English
If the integral basis is used, and certain coefficient matrices are integral over ℤ, then discr computed from those matrices matches the ℚ-discriminant.
Русский
Если использовать интегральную базу и некоторые коэффициентные матрицы целочисленны по ℤ, то дискриминант, получаемый из этих матриц, совпадает с дискриминантом над ℚ.
LaTeX
$$$$\\mathsf{discr}_{\\mathbb{Q}}(\\text{coeff-integral matrices}) = \\mathsf{discr}(K).$$$$
Lean4
/-- If `b` and `b'` are `ℚ`-bases of a number field `K` such that
`∀ i j, IsIntegral ℤ (b.toMatrix b' i j)` and `∀ i j, IsIntegral ℤ (b'.toMatrix b i j)` then
`discr ℚ b = discr ℚ b'`. -/
theorem discr_eq_discr_of_toMatrix_coeff_isIntegral [NumberField K] {b : Basis ι ℚ K} {b' : Basis ι' ℚ K}
(h : ∀ i j, IsIntegral ℤ (b.toMatrix b' i j)) (h' : ∀ i j, IsIntegral ℤ (b'.toMatrix b i j)) :
discr ℚ b = discr ℚ b' :=
by
replace h' : ∀ i j, IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b')) i j) :=
by
intro i j
convert h' i ((b.indexEquiv b').symm j)
simp [Basis.toMatrix_apply]
classical
rw [← (b.reindex (b.indexEquiv b')).toMatrix_map_vecMul b', discr_of_matrix_vecMul, ← one_mul (discr ℚ b),
Basis.coe_reindex, discr_reindex]
congr
have hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix b').det := IsIntegral.det fun i j => h _ _
obtain ⟨r, hr⟩ := IsIntegrallyClosed.isIntegral_iff.1 hint
have hunit : IsUnit r :=
by
have : IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b'))).det := IsIntegral.det fun i j => h' _ _
obtain ⟨r', hr'⟩ := IsIntegrallyClosed.isIntegral_iff.1 this
refine isUnit_iff_exists_inv.2 ⟨r', ?_⟩
suffices algebraMap ℤ ℚ (r * r') = 1
by
rw [← RingHom.map_one (algebraMap ℤ ℚ)] at this
exact (IsFractionRing.injective ℤ ℚ) this
rw [RingHom.map_mul, hr, hr', ← Matrix.det_mul, Basis.toMatrix_mul_toMatrix_flip, Matrix.det_one]
rw [← RingHom.map_one (algebraMap ℤ ℚ), ← hr]
rcases Int.isUnit_iff.1 hunit with hp | hm
· simp [hp]
· simp [hm]
