theorem
hensel_lemma_III
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
(f : Polynomial A)
(g_bar h_bar : Polynomial (A ⧸ IsLocalRing.maximalIdeal A))
(hfact : Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) f = g_bar * h_bar)
(hcoprime : IsCoprime g_bar h_bar)
:
∃ (g : Polynomial A) (h : Polynomial A),
f = g * h ∧ Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) g = g_bar ∧ Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) h = h_bar ∧ g.natDegree = g_bar.natDegree
theorem
irreducible_no_coprime_factor_mod
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
{f : Polynomial A}
(hirr : Irreducible f)
(g_bar h_bar : Polynomial (A ⧸ IsLocalRing.maximalIdeal A))
(hfact : Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) f = g_bar * h_bar)
(hcoprime : IsCoprime g_bar h_bar)
:
theorem
hensel_kurschak_scaling_step
{A : Type u_3}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
{K : Type u_4}
[Field K]
[Algebra A K]
[IsFractionRing A K]
(f : Polynomial K)
(hirr : Irreducible f)
(hlead : ∃ (a : A), (algebraMap A K) a = f.leadingCoeff)
(hconst : ∃ (a : A), (algebraMap A K) a = f.coeff 0)
(hnotinA : ¬∃ (g : Polynomial A), f = Polynomial.map (algebraMap A K) g)
:
∃ (g : Polynomial A),
Irreducible g ∧ g.coeff 0 ∈ IsLocalRing.maximalIdeal A ∧ g.coeff g.natDegree ∈ IsLocalRing.maximalIdeal A ∧ ∃ (i : ℕ), g.coeff i ∉ IsLocalRing.maximalIdeal A
theorem
hensel_kurschak
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
{K : Type u_2}
[Field K]
[Algebra A K]
[IsFractionRing A K]
(f : Polynomial K)
(hirr : Irreducible f)
(hlead : ∃ (a : A), (algebraMap A K) a = f.leadingCoeff)
(hconst : ∃ (a : A), (algebraMap A K) a = f.coeff 0)
:
∃ (g : Polynomial A), f = Polynomial.map (algebraMap A K) g
theorem
norm_eq_minpoly_const_power
{K : Type u_2}
[Field K]
{L : Type u_3}
[Field L]
[Algebra K L]
[FiniteDimensional K L]
(α : L)
:
∃ (e : ℕ), 0 < e ∧ (Algebra.norm K) α = (-1) ^ Module.finrank K L * Polynomial.eval 0 (minpoly K α) ^ e
theorem
norm_integral_of_integral
{A : Type u_4}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
{K : Type u_5}
[Field K]
[Algebra A K]
[IsFractionRing A K]
{L : Type u_6}
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[Algebra A L]
[IsScalarTower A K L]
(α : L)
(hα : IsIntegral A α)
:
∃ (a : A), (algebraMap A K) a = (Algebra.norm K) α
theorem
integral_of_norm_integral
{A : Type u_4}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
{K : Type u_5}
[Field K]
[Algebra A K]
[IsFractionRing A K]
{L : Type u_6}
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[Algebra A L]
[IsScalarTower A K L]
(α : L)
(hα_norm : ∃ (a : A), (algebraMap A K) a = (Algebra.norm K) α)
:
IsIntegral A α
theorem
integral_iff_norm_integral
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
{K : Type u_2}
[Field K]
[Algebra A K]
[IsFractionRing A K]
{L : Type u_3}
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[Algebra A L]
[IsScalarTower A K L]
(α : L)
:
theorem
isDVR_of_local_dedekind
(R : Type u_1)
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
[IsLocalRing R]
(hnotfield : ¬IsField R)
:
theorem
maximal_lies_over_in_AKLB
(A : Type u_1)
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
(K : Type u_2)
[Field K]
[Algebra A K]
[IsFractionRing A K]
(L : Type u_3)
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[Algebra.IsSeparable K L]
[Algebra A L]
[IsScalarTower A K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[Algebra A B]
[Algebra B L]
[IsScalarTower A B L]
[IsIntegralClosure B A L]
(𝔮 : Ideal B)
(h𝔮 : 𝔮.IsMaximal)
:
theorem
two_maximal_ideals_give_coprime_factorization
{A : Type u_1}
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
{K : Type u_2}
[Field K]
[Algebra A K]
[IsFractionRing A K]
{L : Type u_3}
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[Algebra.IsSeparable K L]
[Algebra A L]
[IsScalarTower A K L]
{B : Type u_4}
[CommRing B]
[IsDomain B]
[Algebra A B]
[Algebra B L]
[IsScalarTower A B L]
[IsIntegralClosure B A L]
(𝔮₁ 𝔮₂ : Ideal B)
(h₁ : 𝔮₁.IsMaximal)
(h₂ : 𝔮₂.IsMaximal)
(_hne : 𝔮₁ ≠ 𝔮₂)
(b : B)
(hb₁ : b ∈ 𝔮₁)
(hb₂ : b ∉ 𝔮₂)
(hbint : IsIntegral A b)
(_hirr : Irreducible (minpoly A b))
:
∃ (g_bar : Polynomial (A ⧸ IsLocalRing.maximalIdeal A)) (h_bar : Polynomial (A ⧸ IsLocalRing.maximalIdeal A)),
Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) (minpoly A b) = g_bar * h_bar ∧ IsCoprime g_bar h_bar ∧ ¬IsUnit g_bar ∧ ¬IsUnit h_bar
theorem
unique_maximal_ideal_of_complete_DVR
(A : Type u_1)
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
(K : Type u_2)
[Field K]
[Algebra A K]
[IsFractionRing A K]
(L : Type u_3)
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[Algebra.IsSeparable K L]
[Algebra A L]
[IsScalarTower A K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[Algebra A B]
[Algebra B L]
[IsScalarTower A B L]
[IsIntegralClosure B A L]
(𝔮₁ 𝔮₂ : Ideal B)
(h₁ : 𝔮₁.IsMaximal)
(h₂ : 𝔮₂.IsMaximal)
:
theorem
integral_closure_complete_DVR_is_DVR
(A : Type u_1)
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
(K : Type u_2)
[Field K]
[Algebra A K]
[IsFractionRing A K]
(L : Type u_3)
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[Algebra.IsSeparable K L]
[Algebra A L]
[IsScalarTower A K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[Algebra A B]
[Algebra B L]
[IsScalarTower A B L]
[IsIntegralClosure B A L]
: