English
Let R be integrally closed, K its fraction field, L/K finite separable, and B a power basis with B.gen integral over R. Then for any z ∈ L integral over R, discr_K(B.basis) · z lies in the R-subalgebra generated by B.gen.
Русский
Пусть R целостно замкнуто, K — дробная часть R, L/K конечное разделимое, B — база степеней с B.gen целым над R. Тогда для любого z ∈ L, интеграл над R, дискриминант диск_K(B.basis) умноженный на z лежит в R-алгебре, порожденной B.gen.
LaTeX
$$$$ \\mathrm{discr}\\,K\\,B.basis \\cdot z \\in \\operatorname{adjoin}_R(\\{ B.gen \\}) $$$$
Lean4
/-- Let `K` be the fraction field of an integrally closed domain `R` and let `L` be a finite
separable extension of `K`. Let `B : PowerBasis K L` be such that `IsIntegral R B.gen`.
Then for all, `z : L` that are integral over `R`, we have
`(discr K B.basis) • z ∈ adjoin R ({B.gen} : Set L)`. -/
theorem discr_mul_isIntegral_mem_adjoin [Algebra.IsSeparable K L] [IsIntegrallyClosed R] [IsFractionRing R K]
{B : PowerBasis K L} (hint : IsIntegral R B.gen) {z : L} (hz : IsIntegral R z) :
discr K B.basis • z ∈ adjoin R ({ B.gen } : Set L) :=
by
have hinv : IsUnit (traceMatrix K B.basis).det := by simpa [← discr_def] using discr_isUnit_of_basis _ B.basis
have H :
(traceMatrix K B.basis).det • (traceMatrix K B.basis) *ᵥ (B.basis.equivFun z) =
(traceMatrix K B.basis).det • fun i => trace K L (z * B.basis i) :=
by congr; exact traceMatrix_of_basis_mulVec _ _
have cramer := mulVec_cramer (traceMatrix K B.basis) fun i => trace K L (z * B.basis i)
suffices ∀ i, ((traceMatrix K B.basis).det • B.basis.equivFun z) i ∈ (⊥ : Subalgebra R K)
by
rw [← B.basis.sum_repr z, Finset.smul_sum]
refine Subalgebra.sum_mem _ fun i _ => ?_
replace this := this i
rw [← discr_def, Pi.smul_apply, mem_bot] at this
obtain ⟨r, hr⟩ := this
rw [Basis.equivFun_apply] at hr
rw [← smul_assoc, ← hr, algebraMap_smul]
refine Subalgebra.smul_mem _ ?_ _
rw [B.basis_eq_pow i]
exact Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _
intro i
rw [← H, ← mulVec_smul] at cramer
replace cramer := congr_arg (mulVec (traceMatrix K B.basis)⁻¹) cramer
rw [mulVec_mulVec, nonsing_inv_mul _ hinv, mulVec_mulVec, nonsing_inv_mul _ hinv, one_mulVec, one_mulVec] at cramer
rw [← congr_fun cramer i, cramer_apply, det_apply]
refine Subalgebra.sum_mem _ fun σ _ => Subalgebra.zsmul_mem _ (Subalgebra.prod_mem _ fun j _ => ?_) _
by_cases hji : j = i
· simp only [updateCol_apply, hji, PowerBasis.coe_basis]
exact mem_bot.2 (IsIntegrallyClosed.isIntegral_iff.1 <| isIntegral_trace (hz.mul <| hint.pow _))
· simp only [updateCol_apply, hji, PowerBasis.coe_basis]
exact mem_bot.2 (IsIntegrallyClosed.isIntegral_iff.1 <| isIntegral_trace <| (hint.pow _).mul (hint.pow _))
