theorem
dvr_extension_isLocalHom
(A : Type u_1)
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
(B : Type u_2)
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Module.Finite A B]
:
IsLocalHom (algebraMap A B)
theorem
dvr_extension_module_finite
(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]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
[Algebra.IsSeparable K L]
[IsIntegralClosure B A L]
:
Module.Finite A B
theorem
dvr_extension_finite_and_local
(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]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
[Algebra.IsSeparable K L]
[IsIntegralClosure B A L]
:
theorem
cyclotomic_monogenicity_hensel
{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]
{m : ℕ}
(_hm : 0 < m)
{L : Type u_3}
[Field L]
[Algebra K L]
[IsCyclotomicExtension {m} K L]
[FiniteDimensional K L]
{B : Type u_4}
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
[Module.Finite A B]
[IsLocalHom (algebraMap A B)]
(ζ : B)
(_hζ : IsPrimitiveRoot ζ m)
:
theorem
cyclotomic_residue_field_generated
{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]
{m : ℕ}
(_hm : 0 < m)
{L : Type u_3}
[Field L]
[Algebra K L]
[IsCyclotomicExtension {m} K L]
[FiniteDimensional K L]
{B : Type u_4}
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
[Module.Finite A B]
[IsLocalHom (algebraMap A B)]
(ζ : B)
(_hζ : IsPrimitiveRoot ζ m)
:
theorem
cyclotomic_lifting_mod_maxideal_B
{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]
{m : ℕ}
(_hm : 0 < m)
{L : Type u_3}
[Field L]
[Algebra K L]
[IsCyclotomicExtension {m} K L]
[FiniteDimensional K L]
{B : Type u_4}
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
[Module.Finite A B]
(ζ : B)
(_hζ : IsPrimitiveRoot ζ m)
(b : B)
:
∃ s ∈ Subalgebra.toSubmodule A[ζ], b - s ∈ IsLocalRing.maximalIdeal B
theorem
cyclotomic_uniformizer_in_adjoin
{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]
{m : ℕ}
(_hm : 0 < m)
{L : Type u_3}
[Field L]
[Algebra K L]
[IsCyclotomicExtension {m} K L]
[FiniteDimensional K L]
{B : Type u_4}
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
[Module.Finite A B]
(ζ : B)
(_hζ : IsPrimitiveRoot ζ m)
:
∃ π ∈ A[ζ], Irreducible π
theorem
cyclotomic_root_spans_mod_maximal
(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]
(m : ℕ)
(_hm : 0 < m)
(L : Type u_3)
[Field L]
[Algebra K L]
[IsCyclotomicExtension {m} K L]
[FiniteDimensional K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
[Module.Finite A B]
(ζ : B)
(_hζ : IsPrimitiveRoot ζ m)
:
theorem
dvr_cyclotomic_monogenic_adjoin_eq_top
(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]
(m : ℕ)
(hm : 0 < m)
(L : Type u_3)
[Field L]
[Algebra K L]
[IsCyclotomicExtension {m} K L]
[FiniteDimensional K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
[IsIntegralClosure B A L]
(ζ : B)
(hζ : IsPrimitiveRoot ζ m)
:
theorem
dvr_cyclotomic_monogenic_root
(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]
(m : ℕ)
(hm : 0 < m)
(L : Type u_3)
[Field L]
[Algebra K L]
[IsCyclotomicExtension {m} K L]
[FiniteDimensional K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
[IsIntegralClosure B A L]
:
∃ (ζ : B), IsPrimitiveRoot ζ m ∧ A[ζ] = ⊤
theorem
dvr_cyclotomic_unramified_finrank
(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]
(p : ℕ)
[hp : Fact (Nat.Prime p)]
[Fintype (IsLocalRing.ResidueField A)]
[CharP (IsLocalRing.ResidueField A) p]
(m : ℕ)
(hm : 0 < m)
(hcop : ¬p ∣ m)
(L : Type u_3)
[Field L]
[Algebra K L]
[IsCyclotomicExtension {m} K L]
[FiniteDimensional K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
[IsLocalHom (algebraMap A B)]
[IsIntegralClosure B A L]
:
theorem
no_prim_root_in_unramified_ext_of_base
(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]
[Fintype (IsLocalRing.ResidueField A)]
(p : ℕ)
[hp : Fact (Nat.Prime p)]
[CharP (IsLocalRing.ResidueField A) p]
(L : Type u_3)
[Field L]
[Algebra K L]
[FiniteDimensional K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
(habsunram : Ideal.span {↑p} = IsLocalRing.maximalIdeal A)
(he : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal B) = 1)
(hnoroot : ∀ (ω : K), ¬IsPrimitiveRoot ω p)
(ω : L)
:
¬IsPrimitiveRoot ω p
theorem
no_prim_pth_root_in_unramified_ext
(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]
[Fintype (IsLocalRing.ResidueField A)]
(p : ℕ)
[hp : Fact (Nat.Prime p)]
[CharP (IsLocalRing.ResidueField A) p]
(L : Type u_3)
[Field L]
[Algebra K L]
[FiniteDimensional K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
(habsunram : Ideal.span {↑p} = IsLocalRing.maximalIdeal A)
(he : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal B) = 1)
(hnoroot : ∀ (ω : K), ¬IsPrimitiveRoot ω p)
(η : L)
(hη : η ^ p = 1)
:
theorem
unramified_pth_root_in_base
(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]
[Fintype (IsLocalRing.ResidueField A)]
(p : ℕ)
[hp : Fact (Nat.Prime p)]
[CharP (IsLocalRing.ResidueField A) p]
(L : Type u_3)
[Field L]
[Algebra K L]
[FiniteDimensional K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
(habsunram : Ideal.span {↑p} = IsLocalRing.maximalIdeal A)
(he : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal B) = 1)
(η : L)
(hη : η ^ p = 1)
:
∃ (ζ : K), (algebraMap K L) ζ = η
theorem
dvr_pth_root_ramified
(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]
(p : ℕ)
[hp : Fact (Nat.Prime p)]
[Fintype (IsLocalRing.ResidueField A)]
[CharP (IsLocalRing.ResidueField A) p]
(hno_prim : ∀ (ζ : K), ζ ^ p = 1 → ζ = 1)
(m : ℕ)
(hm : 0 < m)
(hdvd : p ∣ m)
(L : Type u_3)
[Field L]
[Algebra K L]
[IsCyclotomicExtension {m} K L]
[FiniteDimensional K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
(habsunram : Ideal.span {↑p} = IsLocalRing.maximalIdeal A)
:
theorem
cyclotomic_unramified_of_coprime
(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]
(p : ℕ)
[hp : Fact (Nat.Prime p)]
[Fintype (IsLocalRing.ResidueField A)]
[CharP (IsLocalRing.ResidueField A) p]
(m : ℕ)
(hm : 0 < m)
(hcop : ¬p ∣ m)
(L : Type u_3)
[Field L]
[Algebra K L]
[IsCyclotomicExtension {m} K L]
[FiniteDimensional K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
[Algebra.IsSeparable K L]
[IsIntegralClosure B A L]
:
theorem
cyclotomic_ramified_of_dvd
(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]
(p : ℕ)
[hp : Fact (Nat.Prime p)]
[Fintype (IsLocalRing.ResidueField A)]
[CharP (IsLocalRing.ResidueField A) p]
(hno_prim : ∀ (ζ : K), ζ ^ p = 1 → ζ = 1)
(m : ℕ)
(hm : 0 < m)
(hdvd : p ∣ m)
(L : Type u_3)
[Field L]
[Algebra K L]
[IsCyclotomicExtension {m} K L]
[FiniteDimensional K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
(habsunram : Ideal.span {↑p} = IsLocalRing.maximalIdeal A)
:
theorem
cyclotomic_ramified_iff_char_dvd
(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]
(p : ℕ)
[hp : Fact (Nat.Prime p)]
[Fintype (IsLocalRing.ResidueField A)]
[CharP (IsLocalRing.ResidueField A) p]
(hno_prim : ∀ (ζ : K), ζ ^ p = 1 → ζ = 1)
(m : ℕ)
(hm : 0 < m)
(L : Type u_3)
[Field L]
[Algebra K L]
[IsCyclotomicExtension {m} K L]
[FiniteDimensional K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
(habsunram : Ideal.span {↑p} = IsLocalRing.maximalIdeal A)
[Algebra.IsSeparable K L]
[IsIntegralClosure B A L]
:
theorem
cor_10_16
(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]
(n : ℕ)
(hn_pos : 0 < n)
(L : Type u_3)
[Field L]
[Algebra K L]
[IsCyclotomicExtension {n} K L]
[FiniteDimensional K L]
(B : Type u_4)
[CommRing B]
[IsDomain B]
[IsDiscreteValuationRing B]
[Algebra A B]
[Algebra B L]
[Algebra A L]
[IsFractionRing B L]
[IsScalarTower A B L]
[IsScalarTower A K L]
[IsIntegralClosure B A L]
[IsLocalHom (algebraMap A B)]
[Module.Finite A B]
[NoZeroSMulDivisors A B]
(ζ : B)
(hprim : IsPrimitiveRoot ζ n)
(hcoprime : n.Coprime (ringChar (IsLocalRing.ResidueField A)))
: