Atlas.NumberTheoryI.code.LocalExtensions

source

theorem nakayama_local_ring_generators {R : Type u_1} {M : Type u_2} [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M] {N N' : Submodule R M} (hN' : N'.FG) (hNN : N' ≤ N ⊔ IsLocalRing.maximalIdeal R • N') :

N' ≤ N

source

theorem maximal_ideal_contains_image_of_finite_algebra {A : Type u_1} {B : Type u_2} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] [CommRing B] [Algebra A B] [Module.Finite A B] (𝔪 : Ideal B) [h𝔪 : 𝔪.IsMaximal] :

Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A) ≤ 𝔪

source

theorem Polynomial.comap_mapRingHom_bot_eq_map_C_ker {A : Type u_1} [CommRing A] (I : Ideal A) :

Ideal.comap (mapRingHom (Ideal.Quotient.mk I)) ⊥ = Ideal.map C I

source

noncomputable def AdjoinRoot.quotientIso (A : Type u_1) [CommRing A] [IsLocalRing A] (g : Polynomial A) :

(AdjoinRoot g ⧸ Ideal.map (of g) (IsLocalRing.maximalIdeal A)) ≃ₐ[A] Polynomial (IsLocalRing.ResidueField A) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) g}

Instances For

source

theorem AdjoinRoot.maximal_ideal_form {A : Type u_1} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (g : Polynomial A) [hA : Module.Finite A (AdjoinRoot g)] (𝔪 : Ideal (AdjoinRoot g)) [h𝔪 : 𝔪.IsMaximal] :

∃ (q : Polynomial A), Irreducible (Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) q) ∧ Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) q ∣ Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) g ∧ 𝔪 = Ideal.map (algebraMap A (AdjoinRoot g)) (IsLocalRing.maximalIdeal A) ⊔ Ideal.span {(mk g) q}

source

theorem AdjoinRoot.is_maximal_of_irreducible_factor {A : Type u_1} [CommRing A] [IsLocalRing A] (g q : Polynomial A) (hirr : Irreducible (Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) q)) (hdvd : Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) q ∣ Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) g) :

(Ideal.map (algebraMap A (AdjoinRoot g)) (IsLocalRing.maximalIdeal A) ⊔ Ideal.span {(mk g) q}).IsMaximal

source

theorem AdjoinRoot.maximal_ideal_iff {A : Type u_1} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (g : Polynomial A) [hA : Module.Finite A (AdjoinRoot g)] (𝔪 : Ideal (AdjoinRoot g)) :

𝔪.IsMaximal ↔ ∃ (q : Polynomial A), Irreducible (Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) q) ∧ Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) q ∣ Polynomial.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) g ∧ 𝔪 = Ideal.map (algebraMap A (AdjoinRoot g)) (IsLocalRing.maximalIdeal A) ⊔ Ideal.span {(mk g) q}

source

theorem subalgebra_eq_top_of_mod_maximal {A : Type u_1} {B : Type u_2} [CommRing A] [IsLocalRing A] [CommRing B] [Algebra A B] [Module.Finite A B] (S : Subalgebra A B) (h : ⊤ ≤ Subalgebra.toSubmodule S ⊔ IsLocalRing.maximalIdeal A • ⊤) :

S = ⊤

source

class IsUnramifiedDVRExtension (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] :

Prop

residue_separable : Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)
degree_eq : Module.finrank A B = Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)

Instances

source

structure IsDVRUnramified (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (B : Type u_2) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] :

Prop

ramIdx_eq_one : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal B) = 1
residue_separable : Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)

Instances For

source

theorem isDVRUnramified_isSeparable (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] (hunr : IsDVRUnramified A B) :

Algebra.IsSeparable K L

source

theorem isDVRUnramified_implies_formallyUnramified (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] (hunr : IsDVRUnramified A B) :

Algebra.FormallyUnramified K L

source

theorem cyclotomic_dvr_unramified (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] (m : ℕ) (hm : m.Coprime (ringChar (IsLocalRing.ResidueField A))) (ζ : L) (hζ : IsPrimitiveRoot ζ m) (hgen : K⟮ζ⟯ = ⊤) :

IsDVRUnramified A B

source

theorem mod_maximal_surjection_general (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [FiniteDimensional (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (ᾱ : IsLocalRing.ResidueField B) (hᾱ : (IsLocalRing.ResidueField A)⟮ᾱ⟯ = ⊤) (α : B) (hα : (IsLocalRing.residue B) α = ᾱ) (b : B) :

∃ s ∈ Subalgebra.toSubmodule A[α], b - s ∈ IsLocalRing.maximalIdeal B

source

theorem unit_mul_irreducible_not_sq' (B : Type u_2) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] (u : B) (hu : IsUnit u) (p : B) (hp : Irreducible p) :

u * p ∉ IsLocalRing.maximalIdeal B ^ 2

source

theorem irreducible_of_mem_not_sq' (B : Type u_2) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] (x : B) (hx_in : x ∈ IsLocalRing.maximalIdeal B) (hx_not : x ∉ IsLocalRing.maximalIdeal B ^ 2) :

Irreducible x

source

theorem uniformizer_in_adjoin (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] (hsep : Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)) [FiniteDimensional (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (abar : IsLocalRing.ResidueField B) (_habar : (IsLocalRing.ResidueField A)⟮abar⟯ = ⊤) (α₀ : B) (hα₀ : (IsLocalRing.residue B) α₀ = abar) :

∃ (α : B), (IsLocalRing.residue B) α = abar ∧ ∃ π ∈ Subalgebra.toSubmodule A[α], Irreducible π

source

theorem bootstrap_subalgebra_pow (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] (S : Subalgebra A B) (π : B) (hπ_irr : Irreducible π) (hπ_in : π ∈ Subalgebra.toSubmodule S) (hmod1 : ∀ (b : B), ∃ s ∈ Subalgebra.toSubmodule S, b - s ∈ IsLocalRing.maximalIdeal B) (n : ℕ) (b : B) :

∃ s ∈ Subalgebra.toSubmodule S, b - s ∈ IsLocalRing.maximalIdeal B ^ n

source

theorem exists_maximal_pow_le_map (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [Module.Finite A B] :

∃ (e : ℕ), IsLocalRing.maximalIdeal B ^ e ≤ Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A)

source

theorem adjusted_lift_spans (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] (hsep : Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)) [FiniteDimensional (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (ᾱ : IsLocalRing.ResidueField B) (hᾱ : (IsLocalRing.ResidueField A)⟮ᾱ⟯ = ⊤) (α₀ : B) (hα₀ : (IsLocalRing.residue B) α₀ = ᾱ) :

∃ (α : B), ∀ (b : B), ∃ s ∈ Subalgebra.toSubmodule A[α], b - s ∈ Submodule.restrictScalars A (Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A))

source

theorem exists_spanning_element (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] (hsep : Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)) [FiniteDimensional (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] :

∃ (α : B), ⊤ ≤ Subalgebra.toSubmodule A[α] ⊔ IsLocalRing.maximalIdeal A • ⊤

source

theorem dvr_monogenicity (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] (hsep : Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)) [FiniteDimensional (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] :

∃ (α : B), A[α] = ⊤

source

theorem map_maximalIdeal_eq_of_ramificationIdx_one (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] (hunram : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal B) = 1) :

Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A) = IsLocalRing.maximalIdeal B

source

theorem dvr_monogenicity_unramified_forall (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] (_hsep : Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)) [FiniteDimensional (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] (hunram : (IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal B) = 1) (ᾱ : IsLocalRing.ResidueField B) (hgen : (IsLocalRing.ResidueField A)[ᾱ] = ⊤) (α₀ : B) (hlift : (IsLocalRing.residue B) α₀ = ᾱ) :

A[α₀] = ⊤

source

theorem unramified_iff_norm_surjective_units (A : Type u_1) (B : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [Fintype (IsLocalRing.ResidueField A)] :

Algebra.FormallyUnramified A B ↔ Function.Surjective ⇑(Units.map (Algebra.norm A))

source

def IsFiniteUnramifiedSubext (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] (L : Type u_3) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] (E : IntermediateField K L) :

Prop

Instances For

source

theorem isFiniteUnramifiedSubext_map (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] (E : IntermediateField K L) (hE : IsFiniteUnramifiedSubext A K L E) (σ : Gal(L/K)) :

IsFiniteUnramifiedSubext A K L (IntermediateField.map (↑σ) E)

source

def maximalUnramifiedSubextension (A : Type u_1) [CommRing A] (K : Type u_2) [Field K] [Algebra A K] (L : Type u_3) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] :

IntermediateField K L

Instances For

source

theorem maximalUnramifiedSubextension_map_le (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] (σ : Gal(L/K)) :

IntermediateField.map (↑σ) (maximalUnramifiedSubextension A K L) ≤ maximalUnramifiedSubextension A K L

source

theorem maximalUnramifiedSubextension_map_eq (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] (σ : Gal(L/K)) :

IntermediateField.map (↑σ) (maximalUnramifiedSubextension A K L) = maximalUnramifiedSubextension A K L

source

theorem coprime_pred_of_prime_dvd {p m : ℕ} (hp : Nat.Prime p) (hm : 1 ≤ m) (hdvd : p ∣ m) :

(m - 1).Coprime p

source

theorem finite_field_coprime_pred_pow (F : Type u_1) [Field F] [Fintype F] (n : ℕ) (hn : 0 < n) :

(Fintype.card F ^ n - 1).Coprime (ringChar F)

source

theorem henselian_prim_root (A : Type u_1) [CommRing A] [IsDomain A] [IsLocalRing A] [HenselianLocalRing A] [Fintype (IsLocalRing.ResidueField A)] :

∃ (ζ : A), IsPrimitiveRoot ζ (Fintype.card (IsLocalRing.ResidueField A) - 1)

source

theorem integral_closure_isLocalRing (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] :

IsLocalRing ↥(integralClosure A L)

source

theorem algebraMap_integralClosure_injective (A : Type u_1) [CommRing A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] :

Function.Injective ⇑(algebraMap A ↥(integralClosure A L))

source

theorem isPrecomplete_of_pow_localExt {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] (e : ℕ) (he : 1 ≤ e) [hpc : IsPrecomplete (I ^ e) M] :

IsPrecomplete I M

source

theorem integral_closure_isAdicComplete (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] [Algebra.IsSeparable K L] [IsLocalRing ↥(integralClosure A L)] :

IsAdicComplete (IsLocalRing.maximalIdeal ↥(integralClosure A L)) ↥(integralClosure A L)

source

theorem integral_closure_isHenselian (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] [Algebra.IsSeparable K L] :

HenselianLocalRing ↥(integralClosure A L)

source

theorem integral_closure_isNoetherianRing (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] [Algebra.IsSeparable K L] :

IsNoetherianRing ↥(integralClosure A L)

source

theorem integral_closure_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] [Algebra A L] [IsScalarTower A K L] [Algebra.IsSeparable K L] :

Module.Finite A ↥(integralClosure A L)

source

noncomputable def integral_closure_residueField_fintype (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField 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] [Algebra.IsSeparable K L] [IsLocalRing ↥(integralClosure A L)] :

Fintype (IsLocalRing.ResidueField ↥(integralClosure A L))

Instances For

source

theorem formallyUnramified_integralClosure_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 A L] [IsScalarTower A K L] [Algebra.IsSeparable K L] [IsLocalRing ↥(integralClosure A L)] [IsLocalHom (algebraMap A ↥(integralClosure A L))] :

Algebra.FormallyUnramified A ↥(integralClosure A L)

source

theorem thm_10_13_ramificationIdx_eq_one (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] [Algebra.FormallyUnramified K L] [IsLocalRing ↥(integralClosure A L)] [IsLocalHom (algebraMap A ↥(integralClosure A L))] :

(IsLocalRing.maximalIdeal A).ramificationIdx (IsLocalRing.maximalIdeal ↥(integralClosure A L)) = 1

source

theorem integral_closure_residueField_finrank_eq (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField 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] [Algebra.FormallyUnramified K L] [IsLocalRing ↥(integralClosure A L)] [Fintype (IsLocalRing.ResidueField ↥(integralClosure A L))] [IsLocalHom (algebraMap A ↥(integralClosure A L))] :

Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField ↥(integralClosure A L)) = Module.finrank K L

source

theorem integral_closure_residueField_card (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField 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] [Algebra.FormallyUnramified K L] [IsLocalRing ↥(integralClosure A L)] [Fintype (IsLocalRing.ResidueField ↥(integralClosure A L))] :

Fintype.card (IsLocalRing.ResidueField ↥(integralClosure A L)) = Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L

source

theorem integral_closure_prim_root (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra A L] [IsScalarTower A K L] (hunr : Algebra.FormallyUnramified K L) :

∃ (ζ : ↥(integralClosure A L)), IsPrimitiveRoot ζ (Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L - 1)

source

theorem hensel_lift_prim_root_to_ext (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] (hunr : Algebra.FormallyUnramified K L) :

∃ (ζ : L), IsPrimitiveRoot ζ (Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L - 1)

source

theorem hensel_minpoly_degree_ge_aux (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] (hunr : Algebra.FormallyUnramified K L) (ζ : L) (hζ : IsPrimitiveRoot ζ (Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L - 1)) :

Module.finrank K L ≤ (minpoly K ζ).natDegree

source

theorem hensel_primroot_order_dvd (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] (hunr : Algebra.FormallyUnramified K L) (ζ : L) (hζ : IsPrimitiveRoot ζ (Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L - 1)) :

Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L - 1 ∣ Fintype.card (IsLocalRing.ResidueField A) ^ (minpoly K ζ).natDegree - 1

source

theorem hensel_minpoly_degree_ge (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] (hunr : Algebra.FormallyUnramified K L) (ζ : L) (hζ : IsPrimitiveRoot ζ (Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L - 1)) :

Module.finrank K L ≤ (minpoly K ζ).natDegree

source

theorem teichmuller_order_dvd (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] (hunr : Algebra.FormallyUnramified K L) (ζ : L) (hζ : IsPrimitiveRoot ζ (Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L - 1)) :

Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L - 1 ∣ Fintype.card (IsLocalRing.ResidueField A) ^ (minpoly K ζ).natDegree - 1

source

theorem minpoly_primitiveRoot_degree_ge (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] (hunr : Algebra.FormallyUnramified K L) (ζ : L) (hζ : IsPrimitiveRoot ζ (Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L - 1)) :

Module.finrank K L ≤ (minpoly K ζ).natDegree

source

theorem thm_10_12_adjoin_gen (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] (hunr : Algebra.FormallyUnramified K L) (ζ : L) (hζ : IsPrimitiveRoot ζ (Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L - 1)) :

K⟮ζ⟯ = ⊤

source

theorem thm_10_13_galois (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] (hunr : Algebra.FormallyUnramified K L) :

IsGalois K L

source

theorem galois_group_iso_residue_field (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra A L] [IsScalarTower A K L] [Algebra.IsSeparable K L] [IsLocalRing ↥(integralClosure A L)] [IsLocalHom (algebraMap A ↥(integralClosure A L))] [Fintype (IsLocalRing.ResidueField ↥(integralClosure A L))] :

Nonempty (Gal(L/K) ≃* Gal(IsLocalRing.ResidueField ↥(integralClosure A L)/IsLocalRing.ResidueField A))

source

theorem thm_10_13_cyclic (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] (hunr : Algebra.FormallyUnramified K L) :

IsCyclic Gal(L/K)

source

theorem cor_10_17_iff (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] :

IsDVRUnramified A B ↔ ∃ (ζ : L), IsPrimitiveRoot ζ (Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L - 1) ∧ K⟮ζ⟯ = ⊤

source

theorem root_of_unity_eq_one_of_congr_mod_maximal {B : Type u_1} [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] {m : ℕ} {ζ : B} (hpow : ζ ^ m = 1) (hcong : ζ - 1 ∈ IsLocalRing.maximalIdeal B) (hm_unit : ↑m ∉ IsLocalRing.maximalIdeal B) :

ζ = 1

source

theorem finite_field_adjoin_eq_top_of_isPrimitiveRoot {k : Type u_1} {l : Type u_2} [Field k] [Field l] [Algebra k l] [Fintype l] {ζ : l} (hζ : IsPrimitiveRoot ζ (Fintype.card l - 1)) :

k[ζ] = ⊤

source

theorem dvr_unramified_cyclotomic_monogenic (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] (hunr : IsDVRUnramified A B) (ζ_B : B) (hζ_B : IsPrimitiveRoot ζ_B (Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L - 1)) :

A[ζ_B] = ⊤

source

theorem cor_10_17_integral_closure (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] (hunr : IsDVRUnramified A B) (ζ : L) (hζ : IsPrimitiveRoot ζ (Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L - 1)) (hgen : K⟮ζ⟯ = ⊤) :

A[ζ] = (IsScalarTower.toAlgHom A B L).range

source

theorem cor_10_17_galois_structure (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] (hunr : IsDVRUnramified A B) :

IsGalois K L ∧ Nonempty (Gal(L/K) ≃* Multiplicative (ZMod (Module.finrank K L)))

source

theorem unramified_iff_adjoin_rootOfUnity_and_galois (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Fintype (IsLocalRing.ResidueField A)] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] (L : Type u_4) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] :

(IsDVRUnramified A B ↔ ∃ (ζ : L), IsPrimitiveRoot ζ (Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L - 1) ∧ K⟮ζ⟯ = ⊤) ∧ (IsDVRUnramified A B → ∀ (ζ : L), IsPrimitiveRoot ζ (Fintype.card (IsLocalRing.ResidueField A) ^ Module.finrank K L - 1) → K⟮ζ⟯ = ⊤ → A[ζ] = (IsScalarTower.toAlgHom A B L).range) ∧ (IsDVRUnramified A B → IsGalois K L ∧ Nonempty (Gal(L/K) ≃* Multiplicative (ZMod (Module.finrank K L))))

source

@[reducible, inline]

noncomputable abbrev AKLB_ramIdx (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] :

ℕ

Instances For

source

@[reducible, inline]

noncomputable abbrev AKLB_resDeg (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_3) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] :

ℕ

Instances For

source

theorem thm_9_22_integralClosure_isDVR (A : Type u_5) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_6) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (E : Type u_7) [Field E] [Algebra K E] [FiniteDimensional K E] [Algebra A E] [IsScalarTower A K E] [Algebra.IsSeparable K E] :

IsDiscreteValuationRing ↥(integralClosure A E)

source

theorem AKLB_intClE_isDVR (A : Type u_5) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_6) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (L : Type u_7) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra A L] [IsScalarTower A K L] [Algebra.IsSeparable K L] (E : IntermediateField K L) :

IsDiscreteValuationRing ↥(integralClosure A ↥E)

source

theorem AKLB_degree_eq_ramIdx_mul_resDeg (A : Type u_5) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (K : Type u_6) [Field K] [Algebra A K] [IsFractionRing A K] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] (B : Type u_7) [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Algebra A B] [IsLocalHom (algebraMap A B)] [Module.Finite A B] [NoZeroSMulDivisors A B] (L : Type u_8) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsSeparable (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)] :

Module.finrank K L = AKLB_ramIdx A B * AKLB_resDeg A B