Atlas.NumberTheoryI.code.KroneckerWeber

source

class KroneckerWeber.IsAbelianExtension (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] :

Prop

isGalois : IsGalois F E
comm (σ τ : Gal(E/F)) : σ * τ = τ * σ

Instances

source

class KroneckerWeber.IsCyclicExtension (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] :

Prop

isGalois : IsGalois F E
isCyclic : IsCyclic Gal(E/F)

Instances

source

def KroneckerWeber.LiesInCyclotomicExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] :

Prop

Instances For

source

instance KroneckerWeber.IsAbelianExtension.toIsGalois (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [h : IsAbelianExtension F E] :

IsGalois F E

source

theorem KroneckerWeber.cyclotomic_prime_irreducible_padic (p : ℕ) [hp : Fact (Nat.Prime p)] :

Irreducible (Polynomial.cyclotomic p ℚ_[p])

source

theorem KroneckerWeber.hensel_padic_unit_root_p_eq_two (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [IsCyclotomicExtension {p} ℚ_[p] L] (ζ : L) (hζ : IsPrimitiveRoot ζ p) (hp : p = 2) :

∃ (β : L), β ≠ 0 ∧ β ^ (p - 1) = -(ζ - 1) ^ (p - 1) / (algebraMap ℚ_[p] L) ↑p

source

def KroneckerWeber.geom_sum_prod {R : Type u_1} [CommRing R] (ζ : R) (p : ℕ) :

Instances For

source

theorem KroneckerWeber.cyclotomic_product_identity {R : Type u_1} [CommRing R] [IsDomain R] {p : ℕ} (hp : Nat.Prime p) (hodd : p ≠ 2) {ζ : R} (hζ : IsPrimitiveRoot ζ p) :

(ζ - 1) ^ (p - 1) * geom_sum_prod ζ p = ↑p

source

theorem KroneckerWeber.isUnit_geom_sum_prod {L : Type u_1} [Field L] {p : ℕ} {ζ : L} (hζ : IsPrimitiveRoot ζ p) :

IsUnit (geom_sum_prod ζ p)

source

theorem KroneckerWeber.hensel_padic_neg_winv_isUnit (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [IsCyclotomicExtension {p} ℚ_[p] L] (ζ : L) (hζ : IsPrimitiveRoot ζ p) (hp2 : p ≠ 2) :

∃ (u : (↥(integralClosure ℤ_[p] L))ˣ), ↑↑u = -(geom_sum_prod ζ p)⁻¹

source

theorem KroneckerWeber.hensel_padic_neg_winv_cong_one (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [IsCyclotomicExtension {p} ℚ_[p] L] (ζ : L) (hζ : IsPrimitiveRoot ζ p) (hp2 : p ≠ 2) (u : (↥(integralClosure ℤ_[p] L))ˣ) :

↑↑u = -(geom_sum_prod ζ p)⁻¹ → ↑u - 1 ∈ IsLocalRing.maximalIdeal ↥(integralClosure ℤ_[p] L)

source

theorem KroneckerWeber.hensel_padic_tame_condition (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [IsCyclotomicExtension {p} ℚ_[p] L] (hp2 : p ≠ 2) :

¬ringChar (IsLocalRing.ResidueField ↥(integralClosure ℤ_[p] L)) ∣ p - 1

source

theorem KroneckerWeber.hensel_padic_unit_root (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [IsCyclotomicExtension {p} ℚ_[p] L] (ζ : L) (hζ : IsPrimitiveRoot ζ p) :

∃ (β : L), β ≠ 0 ∧ β ^ (p - 1) = -(ζ - 1) ^ (p - 1) / (algebraMap ℚ_[p] L) ↑p

source

theorem KroneckerWeber.eisenstein_element_generates_cyclotomic (p : ℕ) [hp : Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [IsCyclotomicExtension {p} ℚ_[p] L] (α : L) (hα : α ^ (p - 1) + (algebraMap ℚ_[p] L) ↑p = 0) :

ℚ_[p][α] = ⊤

source

theorem KroneckerWeber.exists_root_neg_p_in_cyclotomic (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [IsCyclotomicExtension {p} ℚ_[p] L] :

∃ (α : L), α ^ (p - 1) + (algebraMap ℚ_[p] L) ↑p = 0 ∧ ℚ_[p][α] = ⊤

source

theorem KroneckerWeber.lemma_20_5 (p : ℕ) [Fact (Nat.Prime p)] :

∃ (L : Type) (x : Field L) (x_1 : Algebra ℚ_[p] L), IsCyclotomicExtension {p} ℚ_[p] L ∧ (∃ (α : L), α ^ (p - 1) + (algebraMap ℚ_[p] L) ↑p = 0 ∧ ℚ_[p][α] = ⊤) ∧ Module.finrank ℚ_[p] L = p - 1

source

theorem KroneckerWeber.tame_decomp_chapters_8_11_combined (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [IsCyclicExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hℓp : ℓ ≠ p) (r : ℕ) (hdeg : Module.finrank ℚ_[p] K = ℓ ^ r) :

∃ (e : ℕ) (n : ℕ) (k : ℕ), e ∣ p - 1 ∧ n ≥ 1 ∧ k ≥ 1 ∧ Nonempty (K →ₐ[ℚ_[p]] CyclotomicField (k * n * p) ℚ_[p])

source

theorem KroneckerWeber.tame_cyclic_decomposition_chapters_8_through_11 (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [IsCyclicExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hℓp : ℓ ≠ p) (r : ℕ) (hdeg : Module.finrank ℚ_[p] K = ℓ ^ r) :

∃ (e : ℕ) (k : ℕ), e ∣ p - 1 ∧ k ≥ 1 ∧ Nonempty (K →ₐ[ℚ_[p]] CyclotomicField (k * p) ℚ_[p])

source

theorem KroneckerWeber.tame_cyclic_embeds_in_cyclotomic (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [IsCyclicExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hℓp : ℓ ≠ p) (r : ℕ) (hdeg : Module.finrank ℚ_[p] K = ℓ ^ r) :

∃ (e : ℕ), e ∣ p - 1 ∧ ∃ (m : ℕ) (_ : m ≥ 1), Nonempty (K →ₐ[ℚ_[p]] CyclotomicField m ℚ_[p])

source

theorem KroneckerWeber.tame_decomp_compositum_axiom (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [IsCyclicExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hℓp : ℓ ≠ p) (r : ℕ) (hdeg : Module.finrank ℚ_[p] K = ℓ ^ r) :

∃ (e : ℕ), e ∣ p - 1 ∧ ∀ q ≥ 1, ∀ (M : Type) (x : Field M) (x_1 : Algebra ℚ_[p] M), IsCyclotomicExtension {q} ℚ_[p] M → ∃ (n : ℕ) (_ : n ≥ 1) (N : Type) (x : Field N) (x_2 : Algebra ℚ_[p] N), IsCyclotomicExtension {n} ℚ_[p] N ∧ Nonempty (K →ₐ[ℚ_[p]] N)

source

theorem KroneckerWeber.cor_10_17_tame_decomp_with_input (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [IsCyclicExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (_ℓ : ℕ) (_hℓ : Nat.Prime _ℓ) (_hℓp : _ℓ ≠ p) (_r : ℕ) (_hdeg : Module.finrank ℚ_[p] K = _ℓ ^ _r) (htame_decomp : ∃ (e : ℕ), e ∣ p - 1 ∧ ∀ q ≥ 1, ∀ (M : Type) (x : Field M) (x_1 : Algebra ℚ_[p] M), IsCyclotomicExtension {q} ℚ_[p] M → ∃ (n : ℕ) (_ : n ≥ 1) (N : Type) (x : Field N) (x_2 : Algebra ℚ_[p] N), IsCyclotomicExtension {n} ℚ_[p] N ∧ Nonempty (K →ₐ[ℚ_[p]] N)) (htot_ram_cyc : ∀ (e : ℕ), e ∣ p - 1 → ∃ q ≥ 1, ∃ (M : Type) (x : Field M) (x_1 : Algebra ℚ_[p] M), IsCyclotomicExtension {q} ℚ_[p] M) :

LiesInCyclotomicExtension ℚ_[p] K

source

theorem KroneckerWeber.lemma_20_5_consequence (p : ℕ) [Fact (Nat.Prime p)] (hlem205 : ∃ (L : Type) (x : Field L) (x_1 : Algebra ℚ_[p] L), IsCyclotomicExtension {p} ℚ_[p] L ∧ Module.finrank ℚ_[p] L = p - 1) (_e : ℕ) (_he : _e ∣ p - 1) :

∃ q ≥ 1, ∃ (M : Type) (x : Field M) (x_1 : Algebra ℚ_[p] M), IsCyclotomicExtension {q} ℚ_[p] M

source

theorem KroneckerWeber.prop_20_4_earlier_chapter_decomposition (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [IsCyclicExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hℓp : ℓ ≠ p) (r : ℕ) (hdeg : Module.finrank ℚ_[p] K = ℓ ^ r) (hlem205 : ∃ (L : Type) (x : Field L) (x_1 : Algebra ℚ_[p] L), IsCyclotomicExtension {p} ℚ_[p] L ∧ Module.finrank ℚ_[p] L = p - 1) :

LiesInCyclotomicExtension ℚ_[p] K

source

theorem KroneckerWeber.proposition_20_4 (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [IsCyclicExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hℓp : ℓ ≠ p) (r : ℕ) (hdeg : Module.finrank ℚ_[p] K = ℓ ^ r) :

LiesInCyclotomicExtension ℚ_[p] K

source

theorem KroneckerWeber.proposition_20_7_totally_wild_cyclic (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [FiniteDimensional ℚ_[p] K] [IsGalois ℚ_[p] K] (htot_ram : Module.finrank ℚ_[p] K > 1) (hwild : p ∣ Module.finrank ℚ_[p] K) :

IsCyclic Gal(K/ℚ_[p])

source

noncomputable def KroneckerWeber.projToLastTwo (p : ℕ) :

Multiplicative (ZMod p × ZMod p × ZMod p) →* Multiplicative (ZMod p × ZMod p)

Instances For

source

theorem KroneckerWeber.projToLastTwo_surjective (p : ℕ) :

Function.Surjective ⇑(projToLastTwo p)

source

theorem KroneckerWeber.inertia_decomp_ZpZ3 (p : ℕ) [Fact (Nat.Prime p)] (_hp : p ≠ 2) (K : Type) [Field K] [Algebra ℚ_[p] K] [FiniteDimensional ℚ_[p] K] [IsGalois ℚ_[p] K] (φ : Gal(K/ℚ_[p]) ≃* Multiplicative (ZMod p × ZMod p × ZMod p)) :

∃ (L : Type) (x : Field L) (x_1 : Algebra ℚ_[p] L) (_ : FiniteDimensional ℚ_[p] L) (_ : IsGalois ℚ_[p] L), Module.finrank ℚ_[p] L > 1 ∧ p ∣ Module.finrank ℚ_[p] L ∧ Nonempty (Gal(L/ℚ_[p]) ≃* Multiplicative (ZMod p × ZMod p))

source

theorem KroneckerWeber.ZMod_square_not_cyclic (p : ℕ) [Fact (Nat.Prime p)] :

¬IsCyclic (Multiplicative (ZMod p × ZMod p))

source

theorem KroneckerWeber.proposition_20_7_inertia_argument (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) (K : Type) [Field K] [Algebra ℚ_[p] K] [FiniteDimensional ℚ_[p] K] [IsGalois ℚ_[p] K] (φ : Gal(K/ℚ_[p]) ≃* Multiplicative (ZMod p × ZMod p × ZMod p)) :

False

source

theorem KroneckerWeber.proposition_20_7_no_ZpZ3 (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) :

¬∃ (K : Type) (x : Field K) (x_1 : Algebra ℚ_[p] K) (_ : FiniteDimensional ℚ_[p] K) (_ : IsGalois ℚ_[p] K), Nonempty (Gal(K/ℚ_[p]) ≃* Multiplicative (ZMod p × ZMod p × ZMod p))

source

theorem KroneckerWeber.cor_10_18_autEquivPow_ax (p : ℕ) [Fact (Nat.Prime p)] (r : ℕ) (hr : r ≥ 1) :

Nonempty (Gal(CyclotomicField (p ^ (r + 1)) ℚ_[p]/ℚ_[p]) ≃* (ZMod (p ^ (r + 1)))ˣ)

source

theorem KroneckerWeber.cor_10_18_ramified_cyclotomic_galois_ax (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) (r : ℕ) (hr : r ≥ 1) :

∃ (M : Type) (x : Field M) (x_1 : Algebra ℚ_[p] M) (_ : FiniteDimensional ℚ_[p] M) (_ : IsGalois ℚ_[p] M), Nonempty (Gal(M/ℚ_[p]) ≃* Multiplicative (ZMod (p - 1) × ZMod (p ^ r))) ∧ LiesInCyclotomicExtension ℚ_[p] M

source

theorem KroneckerWeber.cor_10_17_cyclicity_ax (p : ℕ) [Fact (Nat.Prime p)] (r : ℕ) (hr : r ≥ 1) :

IsCyclic Gal(CyclotomicField (p ^ p ^ r - 1) ℚ_[p]/ℚ_[p])

source

theorem KroneckerWeber.cor_10_17_degree_ax (p : ℕ) [Fact (Nat.Prime p)] (r : ℕ) (hr : r ≥ 1) :

Module.finrank ℚ_[p] (CyclotomicField (p ^ p ^ r - 1) ℚ_[p]) = p ^ r

source

theorem KroneckerWeber.cor_10_17_unramified_cyclotomic_galois_ax (p : ℕ) [Fact (Nat.Prime p)] (r : ℕ) (hr : r ≥ 1) :

∃ (N : Type) (x : Field N) (x_1 : Algebra ℚ_[p] N) (_ : FiniteDimensional ℚ_[p] N) (_ : IsGalois ℚ_[p] N), Nonempty (Gal(N/ℚ_[p]) ≃* Multiplicative (ZMod (p ^ r))) ∧ LiesInCyclotomicExtension ℚ_[p] N

source

theorem KroneckerWeber.ch6_galois_product_of_compositum (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [IsCyclicExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (r : ℕ) (hr : r ≥ 1) (hdeg : Module.finrank ℚ_[p] K = p ^ r) (hnotcyc : ¬LiesInCyclotomicExtension ℚ_[p] K) (M : Type u_2) [Field M] [Algebra ℚ_[p] M] [FiniteDimensional ℚ_[p] M] [IsGalois ℚ_[p] M] (hM_cyc : LiesInCyclotomicExtension ℚ_[p] M) (N : Type u_3) [Field N] [Algebra ℚ_[p] N] [FiniteDimensional ℚ_[p] N] [IsGalois ℚ_[p] N] (hN_cyc : LiesInCyclotomicExtension ℚ_[p] N) (GM : Type u_4) (GN : Type u_5) [CommGroup GM] [CommGroup GN] (hM_gal : Nonempty (Gal(M/ℚ_[p]) ≃* GM)) (hN_gal : Nonempty (Gal(N/ℚ_[p]) ≃* GN)) :

∃ (s : ℕ) (_ : s ≥ 1) (L : Type) (x : Field L) (x_1 : Algebra ℚ_[p] L) (_ : FiniteDimensional ℚ_[p] L) (_ : IsGalois ℚ_[p] L), Nonempty (Gal(L/ℚ_[p]) ≃* GM × GN × Multiplicative (ZMod (p ^ s)))

source

theorem KroneckerWeber.ch6_compositum_with_cyclic_contribution_ax (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [IsCyclicExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (r : ℕ) (hr : r ≥ 1) (hdeg : Module.finrank ℚ_[p] K = p ^ r) (hnotcyc : ¬LiesInCyclotomicExtension ℚ_[p] K) (M : Type u_2) [Field M] [Algebra ℚ_[p] M] [FiniteDimensional ℚ_[p] M] [IsGalois ℚ_[p] M] (hM_cyc : LiesInCyclotomicExtension ℚ_[p] M) (N : Type u_3) [Field N] [Algebra ℚ_[p] N] [FiniteDimensional ℚ_[p] N] [IsGalois ℚ_[p] N] (hN_cyc : LiesInCyclotomicExtension ℚ_[p] N) (GM : Type u_4) (GN : Type u_5) [CommGroup GM] [CommGroup GN] (hM_gal : Nonempty (Gal(M/ℚ_[p]) ≃* GM)) (hN_gal : Nonempty (Gal(N/ℚ_[p]) ≃* GN)) :

source

theorem KroneckerWeber.cor_10_17_18_galois_structure_data (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [IsCyclicExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (r : ℕ) (hr : r ≥ 1) (hdeg : Module.finrank ℚ_[p] K = p ^ r) (hnotcyc : ¬LiesInCyclotomicExtension ℚ_[p] K) :

∃ (s : ℕ) (_ : s ≥ 1) (L : Type) (x : Field L) (x_1 : Algebra ℚ_[p] L) (_ : FiniteDimensional ℚ_[p] L) (_ : IsGalois ℚ_[p] L), Nonempty (Gal(L/ℚ_[p]) ≃* Multiplicative (ZMod (p ^ r) × ZMod (p ^ r) × ZMod (p - 1) × ZMod (p ^ s)))

source

theorem KroneckerWeber.cor_10_17_18_compositum_galois_structure_odd (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [IsCyclicExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (r : ℕ) (hdeg : Module.finrank ℚ_[p] K = p ^ r) (hnotcyc : ¬LiesInCyclotomicExtension ℚ_[p] K) :

∃ (s : ℕ) (_ : s ≥ 1) (_ : r ≥ 1) (L : Type) (x : Field L) (x_1 : Algebra ℚ_[p] L) (_ : FiniteDimensional ℚ_[p] L) (_ : IsGalois ℚ_[p] L), Nonempty (Gal(L/ℚ_[p]) ≃* Multiplicative (ZMod (p ^ r) × ZMod (p ^ r) × ZMod (p - 1) × ZMod (p ^ s)))

source

theorem KroneckerWeber.local_kw_p_odd_contradiction (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [IsCyclicExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (r : ℕ) (hdeg : Module.finrank ℚ_[p] K = p ^ r) (hnotcyc : ¬LiesInCyclotomicExtension ℚ_[p] K) :

∃ (E : Type) (x : Field E) (x_1 : Algebra ℚ_[p] E) (_ : FiniteDimensional ℚ_[p] E) (_ : IsGalois ℚ_[p] E), Nonempty (Gal(E/ℚ_[p]) ≃* Multiplicative (ZMod p × ZMod p × ZMod p))

source

theorem KroneckerWeber.theorem_20_6 (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [IsCyclicExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (r : ℕ) (hdeg : Module.finrank ℚ_[p] K = p ^ r) :

LiesInCyclotomicExtension ℚ_[p] K

source

theorem KroneckerWeber.index_map_mulEquiv {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (φ : G ≃* G') (H : Subgroup G) :

(Subgroup.map φ.toMonoidHom H).index = H.index

source

theorem KroneckerWeber.index_subgroups_card_eq_of_mulEquiv {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (φ : G ≃* G') (n : ℕ) :

Nat.card { H : Subgroup G // H.index = n } = Nat.card { H : Subgroup G' // H.index = n }

source

theorem KroneckerWeber.ps4_galois_index2_bound (K : Type) [Field K] [Algebra ℚ_[2] K] [FiniteDimensional ℚ_[2] K] [IsGalois ℚ_[2] K] :

Nat.card { H : Subgroup Gal(K/ℚ_[2]) // H.index = 2 } ≤ 7

source

theorem KroneckerWeber.Z2Z4_index2_count :

Nat.card { H : Subgroup (Multiplicative (ZMod 2 × ZMod 2 × ZMod 2 × ZMod 2)) // H.index = 2 } = 15

source

theorem KroneckerWeber.lemma_20_11_no_Z2Z4 :

¬∃ (K : Type) (x : Field K) (x_1 : Algebra ℚ_[2] K) (_ : FiniteDimensional ℚ_[2] K) (_ : IsGalois ℚ_[2] K), Nonempty (Gal(K/ℚ_[2]) ≃* Multiplicative (ZMod 2 × ZMod 2 × ZMod 2 × ZMod 2))

source

noncomputable def KroneckerWeber.galoisCorrespondenceIndex (F : Type u_1) [Field F] (K : Type u_2) [Field K] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] (n : ℕ) :

{ H : Subgroup Gal(K/F) // H.index = n } ≃ { L : IntermediateField F K // Module.finrank F ↥L = n }

Instances For

source

theorem KroneckerWeber.ps5_galois_cyclic_quartic_bound (K : Type) [Field K] [Algebra ℚ_[2] K] [FiniteDimensional ℚ_[2] K] [IsGalois ℚ_[2] K] :

Nat.card { H : Subgroup Gal(K/ℚ_[2]) // H.index = 4 ∧ ∃ (x : H.Normal), IsCyclic (Gal(K/ℚ_[2]) ⧸ H) } ≤ 12

source

theorem KroneckerWeber.Z4Z3_cyclic_quartic_count :

Nat.card { H : Subgroup (Multiplicative (ZMod 4 × ZMod 4 × ZMod 4)) // H.index = 4 ∧ IsCyclic (Multiplicative (ZMod 4 × ZMod 4 × ZMod 4) ⧸ H) } = 28

source

theorem KroneckerWeber.Z4Z3_cyclic_quartic_count_with_normal :

Nat.card { H : Subgroup (Multiplicative (ZMod 4 × ZMod 4 × ZMod 4)) // H.index = 4 ∧ ∃ (x : H.Normal), IsCyclic (Multiplicative (ZMod 4 × ZMod 4 × ZMod 4) ⧸ H) } = 28

source

theorem KroneckerWeber.cyclic_normal_index_subgroups_card_eq_of_mulEquiv {G G' : Type} [Group G] [Group G'] (φ : G ≃* G') (n : ℕ) :

Nat.card { H : Subgroup G // H.index = n ∧ ∃ (x : H.Normal), IsCyclic (G ⧸ H) } = Nat.card { H : Subgroup G' // H.index = n ∧ ∃ (x : H.Normal), IsCyclic (G' ⧸ H) }

source

theorem KroneckerWeber.lemma_20_11_no_Z4Z3 :

¬∃ (K : Type) (x : Field K) (x_1 : Algebra ℚ_[2] K) (_ : FiniteDimensional ℚ_[2] K) (_ : IsGalois ℚ_[2] K), Nonempty (Gal(K/ℚ_[2]) ≃* Multiplicative (ZMod 4 × ZMod 4 × ZMod 4))

source

theorem KroneckerWeber.lemma_20_11 :

(¬∃ (K : Type) (x : Field K) (x_1 : Algebra ℚ_[2] K) (_ : FiniteDimensional ℚ_[2] K) (_ : IsGalois ℚ_[2] K), Nonempty (Gal(K/ℚ_[2]) ≃* Multiplicative (ZMod 2 × ZMod 2 × ZMod 2 × ZMod 2))) ∧ ¬∃ (K : Type) (x : Field K) (x_1 : Algebra ℚ_[2] K) (_ : FiniteDimensional ℚ_[2] K) (_ : IsGalois ℚ_[2] K), Nonempty (Gal(K/ℚ_[2]) ≃* Multiplicative (ZMod 4 × ZMod 4 × ZMod 4))

source

theorem KroneckerWeber.galois_quotient_extension (F : Type u₁) (L : Type u₂) [Field F] [Field L] [Algebra F L] [FiniteDimensional F L] [IsGalois F L] (Q : Type u₃) [Group Q] [Fintype Q] (φ : Gal(L/F) →* Q) (hφ : Function.Surjective ⇑φ) :

∃ (E : Type u₂) (x : Field E) (x_1 : Algebra F E) (_ : FiniteDimensional F E) (_ : IsGalois F E), Nonempty (Gal(E/F) ≃* Q)

source

theorem KroneckerWeber.compositum_galois_group_structure_exists (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [IsCyclicExtension ℚ_[2] K] [FiniteDimensional ℚ_[2] K] (r : ℕ) (hr : r ≥ 1) (hdeg : Module.finrank ℚ_[2] K = 2 ^ r) (hnotcyc : ¬LiesInCyclotomicExtension ℚ_[2] K) :

(∃ (s : ℕ) (_ : s ≥ 1) (L : Type) (x : Field L) (x_1 : Algebra ℚ_[2] L) (_ : FiniteDimensional ℚ_[2] L) (_ : IsGalois ℚ_[2] L), Nonempty (Gal(L/ℚ_[2]) ≃* Multiplicative (ZMod 2 × ZMod (2 ^ r) × ZMod (2 ^ r) × ZMod (2 ^ s)))) ∨ ∃ (s : ℕ) (_ : s ≥ 2) (_ : r ≥ 2) (L : Type) (x : Field L) (x_1 : Algebra ℚ_[2] L) (_ : FiniteDimensional ℚ_[2] L) (_ : IsGalois ℚ_[2] L), Nonempty (Gal(L/ℚ_[2]) ≃* Multiplicative (ZMod (2 ^ r) × ZMod (2 ^ r) × ZMod (2 ^ s)))

source

theorem KroneckerWeber.liesInCyclotomicExtension_of_finrank_one (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [FiniteDimensional ℚ_[2] K] (h : Module.finrank ℚ_[2] K = 1) :

LiesInCyclotomicExtension ℚ_[2] K

source

theorem KroneckerWeber.cor_10_17_18_compositum_galois_structure (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [IsCyclicExtension ℚ_[2] K] [FiniteDimensional ℚ_[2] K] (r : ℕ) (hdeg : Module.finrank ℚ_[2] K = 2 ^ r) (hnotcyc : ¬LiesInCyclotomicExtension ℚ_[2] K) :

(∃ (s : ℕ) (_ : s ≥ 1) (_ : r ≥ 1) (L : Type) (x : Field L) (x_1 : Algebra ℚ_[2] L) (_ : FiniteDimensional ℚ_[2] L) (_ : IsGalois ℚ_[2] L), Nonempty (Gal(L/ℚ_[2]) ≃* Multiplicative (ZMod 2 × ZMod (2 ^ r) × ZMod (2 ^ r) × ZMod (2 ^ s)))) ∨ ∃ (s : ℕ) (_ : s ≥ 2) (_ : r ≥ 2) (L : Type) (x : Field L) (x_1 : Algebra ℚ_[2] L) (_ : FiniteDimensional ℚ_[2] L) (_ : IsGalois ℚ_[2] L), Nonempty (Gal(L/ℚ_[2]) ≃* Multiplicative (ZMod (2 ^ r) × ZMod (2 ^ r) × ZMod (2 ^ s)))

source

theorem KroneckerWeber.surjective_of_toMultiplicative {A : Type u_1} {B : Type u_2} [AddZeroClass A] [AddZeroClass B] (f : A →+ B) (hf : Function.Surjective ⇑f) :

Function.Surjective ⇑(AddMonoidHom.toMultiplicative f)

source

theorem KroneckerWeber.surjective_prodMap_addMonoidHom {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [AddZeroClass A] [AddZeroClass B] [AddZeroClass C] [AddZeroClass D] (f : A →+ C) (g : B →+ D) (hf : Function.Surjective ⇑f) (hg : Function.Surjective ⇑g) :

Function.Surjective ⇑(f.prodMap g)

source

theorem KroneckerWeber.cor_10_17_18_compositum_galois_surjection (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [IsCyclicExtension ℚ_[2] K] [FiniteDimensional ℚ_[2] K] (r : ℕ) (hdeg : Module.finrank ℚ_[2] K = 2 ^ r) (hnotcyc : ¬LiesInCyclotomicExtension ℚ_[2] K) :

(∃ (L : Type) (x : Field L) (x_1 : Algebra ℚ_[2] L) (_ : FiniteDimensional ℚ_[2] L) (_ : IsGalois ℚ_[2] L) (φ : Gal(L/ℚ_[2]) →* Multiplicative (ZMod 2 × ZMod 2 × ZMod 2 × ZMod 2)), Function.Surjective ⇑φ) ∨ ∃ (L : Type) (x : Field L) (x_1 : Algebra ℚ_[2] L) (_ : FiniteDimensional ℚ_[2] L) (_ : IsGalois ℚ_[2] L) (φ : Gal(L/ℚ_[2]) →* Multiplicative (ZMod 4 × ZMod 4 × ZMod 4)), Function.Surjective ⇑φ

source

theorem KroneckerWeber.theorem_20_10_contradiction_step (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [IsCyclicExtension ℚ_[2] K] [FiniteDimensional ℚ_[2] K] (r : ℕ) (hdeg : Module.finrank ℚ_[2] K = 2 ^ r) (hnotcyc : ¬LiesInCyclotomicExtension ℚ_[2] K) :

(∃ (E : Type) (x : Field E) (x_1 : Algebra ℚ_[2] E) (_ : FiniteDimensional ℚ_[2] E) (_ : IsGalois ℚ_[2] E), Nonempty (Gal(E/ℚ_[2]) ≃* Multiplicative (ZMod 2 × ZMod 2 × ZMod 2 × ZMod 2))) ∨ ∃ (E : Type) (x : Field E) (x_1 : Algebra ℚ_[2] E) (_ : FiniteDimensional ℚ_[2] E) (_ : IsGalois ℚ_[2] E), Nonempty (Gal(E/ℚ_[2]) ≃* Multiplicative (ZMod 4 × ZMod 4 × ZMod 4))

source

theorem KroneckerWeber.theorem_20_10 (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [IsCyclicExtension ℚ_[2] K] [FiniteDimensional ℚ_[2] K] (r : ℕ) (hdeg : Module.finrank ℚ_[2] K = 2 ^ r) :

LiesInCyclotomicExtension ℚ_[2] K

source

theorem KroneckerWeber.abelian_group_complementary_subgroups (G : Type u_1) [CommGroup G] [Finite G] (hord : 1 < Nat.card G) (hncyc : ¬(IsCyclic G ∧ IsPrimePow (Nat.card G))) :

∃ (H₁ : Subgroup G) (H₂ : Subgroup G), H₁ ⊓ H₂ = ⊥ ∧ 1 < Nat.card ↥H₁ ∧ 1 < Nat.card ↥H₂

source

theorem KroneckerWeber.cyclotomic_compositum_embedding (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [Algebra ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (E₁ E₂ : IntermediateField ℚ_[p] K) (hgen : E₁ ⊔ E₂ = ⊤) (h₁ : LiesInCyclotomicExtension ℚ_[p] ↥E₁) (h₂ : LiesInCyclotomicExtension ℚ_[p] ↥E₂) :

LiesInCyclotomicExtension ℚ_[p] K

source

theorem KroneckerWeber.finrank_fixedField_mul_card (F : Type u_1) [Field F] (K : Type u_2) [Field K] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] (H : Subgroup Gal(K/F)) :

Module.finrank F ↥(IntermediateField.fixedField H) * Nat.card ↥H = Module.finrank F K

source

theorem KroneckerWeber.finrank_fixedField_lt (F : Type u_1) [Field F] (K : Type u_2) [Field K] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] (H : Subgroup Gal(K/F)) (hH : 1 < Nat.card ↥H) :

Module.finrank F ↥(IntermediateField.fixedField H) < Module.finrank F K

source

theorem KroneckerWeber.fixedField_isAbelianExtension (F : Type u_1) [Field F] (K : Type u_2) [Field K] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] (hcomm : ∀ (σ τ : Gal(K/F)), σ * τ = τ * σ) (H : Subgroup Gal(K/F)) [H.Normal] :

IsAbelianExtension F ↥(IntermediateField.fixedField H)

source

theorem KroneckerWeber.fixedField_sup_of_inf_bot (F : Type u_1) [Field F] (K : Type u_2) [Field K] [Algebra F K] [FiniteDimensional F K] [IsGalois F K] (H₁ H₂ : Subgroup Gal(K/F)) (h : H₁ ⊓ H₂ = ⊥) :

IntermediateField.fixedField H₁ ⊔ IntermediateField.fixedField H₂ = ⊤

source

theorem KroneckerWeber.abelian_extension_dichotomy (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [Algebra ℚ_[p] K] [hab : IsAbelianExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] :

(∃ (ℓ : ℕ) (_ : Nat.Prime ℓ) (r : ℕ), IsCyclicExtension ℚ_[p] K ∧ Module.finrank ℚ_[p] K = ℓ ^ r) ∨ ∃ (E₁ : Type) (x : Field E₁) (x_1 : Algebra ℚ_[p] E₁) (_ : IsAbelianExtension ℚ_[p] E₁) (_ : FiniteDimensional ℚ_[p] E₁) (E₂ : Type) (x_4 : Field E₂) (x_5 : Algebra ℚ_[p] E₂) (_ : IsAbelianExtension ℚ_[p] E₂) (_ : FiniteDimensional ℚ_[p] E₂), Module.finrank ℚ_[p] E₁ < Module.finrank ℚ_[p] K ∧ Module.finrank ℚ_[p] E₂ < Module.finrank ℚ_[p] K ∧ (LiesInCyclotomicExtension ℚ_[p] E₁ → LiesInCyclotomicExtension ℚ_[p] E₂ → LiesInCyclotomicExtension ℚ_[p] K)

source

theorem KroneckerWeber.local_kw_reduction (p : ℕ) [Fact (Nat.Prime p)] (cyclic_case : ∀ (E : Type) [inst : Field E] [inst_1 : Algebra ℚ_[p] E] [IsCyclicExtension ℚ_[p] E] [FiniteDimensional ℚ_[p] E] (ℓ : ℕ), Nat.Prime ℓ → ∀ (r : ℕ), Module.finrank ℚ_[p] E = ℓ ^ r → LiesInCyclotomicExtension ℚ_[p] E) (K : Type) [Field K] [Algebra ℚ_[p] K] [IsAbelianExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] :

LiesInCyclotomicExtension ℚ_[p] K

source

theorem KroneckerWeber.theorem_20_2 (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type) [Field K] [Algebra ℚ_[p] K] [IsAbelianExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] :

LiesInCyclotomicExtension ℚ_[p] K

source

theorem KroneckerWeber.adicCompletion_valued_isEquiv_comap {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] :

Valued.v.IsEquiv (Valuation.comap (algebraMap (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)) Valued.v)

source

theorem KroneckerWeber.adicCompletion_valued_hasExtension (A : Type u_A₃) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_K₃) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_L₃) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_B₃) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] :

Valued.v.HasExtension Valued.v

source

theorem KroneckerWeber.algebraMap_adicCompletion_mapsTo_integers (A : Type u_A₄) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_K₄) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_L₄) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_B₄) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (hx : x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) :

(algebraMap (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)) x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮

source

@[reducible]

noncomputable def KroneckerWeber.prop_8_11_completion_integers_algebra (A : Type u_A₄) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_K₄) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_L₄) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_B₄) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] :

Algebra ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)

Instances For

source

theorem KroneckerWeber.adicCompletion_finiteDimensional_aux {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] :

FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)

source

noncomputable def KroneckerWeber.adicCompletionTensorLift {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [IsScalarTower K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] :

TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) L →ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭] IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮

Instances For

source

theorem KroneckerWeber.adicCompletion_tensorProduct_surjective {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [IsScalarTower K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] :

Function.Surjective ⇑(adicCompletionTensorLift 𝔭 𝔮)

source

theorem KroneckerWeber.adicCompletion_isSeparable_aux {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [Algebra.IsSeparable K L] [FiniteDimensional K L] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [IsScalarTower K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] :

Algebra.IsSeparable (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)

source

IsIntegralClosure (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)) (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)

source

Module.Finite ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)

source

IsScalarTower (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭)) (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)

source

Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮) = (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭)).ramificationIdx (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)) * (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭)).inertiaDeg (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮))

source

theorem KroneckerWeber.withZero_mul_eq_exp_neg_one_aux {x y : WithZero (Multiplicative ℤ)} (hprod : x * y = WithZero.exp (-1)) (hx : x ≤ 1) (hy : y ≤ 1) :

x = 1 ∨ y = 1

source

theorem KroneckerWeber.prop_8_11_map_asIdeal_eq_maximalIdeal {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) :

Ideal.map (algebraMap A ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭)) 𝔭.asIdeal = IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭)

source

theorem KroneckerWeber.prop_8_11_comap_maximalIdeal_pow {B : Type u_1} [CommRing B] [IsDomain B] [IsDedekindDomain B] {L : Type u_2} [Field L] [Algebra B L] [IsFractionRing B L] (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (n : ℕ) :

Ideal.comap (algebraMap B ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)) (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮) ^ n) = 𝔮.asIdeal ^ n

source

Ideal.map (algebraMap ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)) (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭)) ≤ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮) ^ n ↔ Ideal.map (algebraMap A B) 𝔭.asIdeal ≤ 𝔮.asIdeal ^ n

source

theorem KroneckerWeber.ch8_10_ramificationIdx_eq_aux {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {B : Type u_3} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] {L : Type u_4} [Field L] [Algebra B L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) [Algebra ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)] [Algebra A ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)] [IsScalarTower A ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)] [IsScalarTower A B ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)] :

source

Function.Injective ⇑(algebraMap ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮))

source

source

theorem KroneckerWeber.ch8_10_map_asIdeal_ne_bot {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {B : Type u_3} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] {L : Type u_4} [Field L] [Algebra B L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) [Algebra ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)] (h_inj : Function.Injective ⇑(algebraMap A B)) :

Ideal.map (algebraMap A B) 𝔭.asIdeal ≠ ⊥

source

BddAbove {n : ℕ | Ideal.map (algebraMap ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)) (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭)) ≤ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮) ^ n}

source

theorem KroneckerWeber.ch8_10_bddAbove_original_aux {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {B : Type u_3} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] {L : Type u_4} [Field L] [Algebra B L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) [Algebra ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)] (h_inj : Function.Injective ⇑(algebraMap A B)) :

BddAbove {n : ℕ | Ideal.map (algebraMap A B) 𝔭.asIdeal ≤ 𝔮.asIdeal ^ n}

source

(IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭)).ramificationIdx (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)) = 𝔭.asIdeal.ramificationIdx 𝔮.asIdeal ∧ BddAbove {n : ℕ | Ideal.map (algebraMap ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)) (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭)) ≤ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮) ^ n} ∧ BddAbove {n : ℕ | Ideal.map (algebraMap A B) 𝔭.asIdeal ≤ 𝔮.asIdeal ^ n}

source

source

source

Ideal.comap (algebraMap ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)) (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)) = IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭)

source

noncomputable def KroneckerWeber.completion_residueFieldEquiv (A : Type u_A₈') [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_K₈') [Field K] [Algebra A K] [IsFractionRing A K] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) :

↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ⧸ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ≃+* A ⧸ 𝔭.asIdeal

Instances For

source

(algebraMap (A ⧸ 𝔭.asIdeal) (B ⧸ 𝔮.asIdeal)).comp (completion_residueFieldEquiv A K 𝔭).toRingHom = (completion_residueFieldEquiv B L 𝔮).toRingHom.comp (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ⧸ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭)) (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮) ⧸ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)))

source

Module.finrank (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ⧸ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭)) (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮) ⧸ IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)) = Module.finrank (A ⧸ 𝔭.asIdeal) (B ⧸ 𝔮.asIdeal)

source

(IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭)).inertiaDeg (IsLocalRing.maximalIdeal ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)) = 𝔭.asIdeal.inertiaDeg 𝔮.asIdeal

source

theorem KroneckerWeber.thm_11_23_part4_completion_degree_eq_ef (A : Type u_A) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_K) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_L) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_B) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) [IsFractionRing B L] [𝔮.asIdeal.LiesOver 𝔭.asIdeal] [inst_alg : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] :

Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮) = 𝔭.asIdeal.ramificationIdx 𝔮.asIdeal * 𝔭.asIdeal.inertiaDeg 𝔮.asIdeal

source

theorem KroneckerWeber.isGalois_adicCompletion (A : Type u_A) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_K) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_L) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_B) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) [IsFractionRing B L] [𝔮.asIdeal.LiesOver 𝔭.asIdeal] (hgal : IsGalois K L) :

IsGalois (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)

source

theorem KroneckerWeber.adjoin_range_algebraMap_adicCompletion_eq_top (A : Type u_A) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_K) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_L) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_B) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) [IsFractionRing B L] [𝔮.asIdeal.LiesOver 𝔭.asIdeal] :

Algebra.adjoin (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (Set.range ⇑(algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮))) = ⊤

source

theorem KroneckerWeber.thm_11_23_part6_galois_implication (A : Type u_A) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_K) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_L) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_B) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) [IsFractionRing B L] [𝔮.asIdeal.LiesOver 𝔭.asIdeal] (hgal : IsGalois K L) :

IsGalois (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮) ∧ ∃ (φ : Gal(IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮/IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) →* Gal(L/K)), Function.Injective ⇑φ

source

theorem KroneckerWeber.theorem_11_23_AKLB (A : Type u_A) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_K) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_L) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_B) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) :

∃ (L_𝔮 : Type u_L) (inst_field : Field L_𝔮) (inst_alg : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) L_𝔮), FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) L_𝔮 ∧ Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) L_𝔮 ≤ Module.finrank K L ∧ Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) L_𝔮 = 𝔭.asIdeal.ramificationIdx 𝔮.asIdeal * 𝔭.asIdeal.inertiaDeg 𝔮.asIdeal ∧ (IsGalois K L → IsGalois (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) L_𝔮 ∧ ∃ (φ : Gal(L_𝔮/IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) →* Gal(L/K)), Function.Injective ⇑φ)

source

theorem KroneckerWeber.theorem_11_23_part1_separable (A : Type u_1) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [CharZero K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_4) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [IsScalarTower K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] :

Algebra.IsSeparable (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)

source

theorem KroneckerWeber.theorem_11_23_part2_unique_prime (A : Type u_1) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_4) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) :

IsDiscreteValuationRing ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)

source

theorem KroneckerWeber.theorem_11_23_part3_ramification_preserved (A : Type u_1) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_4) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] :

source

theorem KroneckerWeber.theorem_11_23_part5_iso_from_weak_approx {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (primesOver : Finset (IsDedekindDomain.HeightOneSpectrum B)) (hPrimesOver : ∀ 𝔮 ∈ primesOver, 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) (hPrimesOverImage : Finset.image IsDedekindDomain.HeightOneSpectrum.asIdeal primesOver = primesOverFinset 𝔭.asIdeal B) :

Nonempty (TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) ≃+* ((𝔮 : ↥primesOver) → IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑𝔮))

source

theorem KroneckerWeber.theorem_11_23_part5_tensor_product_decomp (A : Type u_1) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_4) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (primesOver : Finset (IsDedekindDomain.HeightOneSpectrum B)) (hPrimesOver : ∀ 𝔮 ∈ primesOver, 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) (hPrimesOverImage : Finset.image IsDedekindDomain.HeightOneSpectrum.asIdeal primesOver = primesOverFinset 𝔭.asIdeal B) :

Nonempty (TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) ≃+* ((𝔮 : ↥primesOver) → IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑𝔮)) ∧ Module.finrank K L = ∑ 𝔮 ∈ primesOver, 𝔭.asIdeal.ramificationIdx 𝔮.asIdeal * 𝔭.asIdeal.inertiaDeg 𝔮.asIdeal

source

theorem KroneckerWeber.adicCompletion_algebra_unique {A : Type u_1} [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] {B : Type u_4} [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) [𝔮.asIdeal.LiesOver 𝔭.asIdeal] (inst : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)) [IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] :

inst = instAlgebraAdicCompletionOfLiesOver K 𝔭 𝔮 h𝔮_over_𝔭

source

theorem KroneckerWeber.theorem_11_23_part6_inertia_iso (A : Type u_1) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsGalois K L] (B : Type u_4) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [IsGalois (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] :

(∃ (D_𝔮 : Subgroup Gal(L/K)), Nonempty (Gal(IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮/IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) ≃* ↥D_𝔮)) ∧ ∃ (I_𝔮 : Subgroup Gal(L/K)) (I_hat : Subgroup Gal(IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮/IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭)), Nonempty (↥I_hat ≃* ↥I_𝔮)

source

theorem KroneckerWeber.theorem_11_23_AKLB_specialized_Q (K : Type u_1) [Field K] [Algebra ℚ K] [IsGalois ℚ K] [FiniteDimensional ℚ K] (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ℚ)) :

∃ (L_𝔮 : Type) (inst_field : Field L_𝔮) (inst_alg : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ 𝔭) L_𝔮), IsGalois (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ 𝔭) L_𝔮 ∧ FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ 𝔭) L_𝔮 ∧ Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ 𝔭) L_𝔮 ≤ Module.finrank ℚ K ∧ ∃ (φ : Gal(L_𝔮/IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ 𝔭) →* Gal(K/ℚ)), Function.Injective ⇑φ

source

theorem KroneckerWeber.galois_extension_transport {F₁ : Type u_1} [Field F₁] [Algebra ℚ F₁] {F₂ : Type u_2} [Field F₂] [Algebra ℚ F₂] (e : F₁ ≃ₐ[ℚ ] F₂) {L : Type u_3} [Field L] [Algebra ℚ L] {E : Type} {hF_E : Field E} {hA_E : Algebra F₂ E} (hG : IsGalois F₂ E) (hFD : FiniteDimensional F₂ E) (hbound : Module.finrank F₂ E ≤ Module.finrank ℚ L) (φ : Gal(E/F₂) →* Gal(L/ℚ)) (hφ : Function.Injective ⇑φ) :

∃ (hA' : Algebra F₁ E) (_ : IsGalois F₁ E) (_ : FiniteDimensional F₁ E), Module.finrank F₁ E ≤ Module.finrank ℚ L ∧ ∃ (ψ : Gal(E/F₁) →* Gal(L/ℚ)), Function.Injective ⇑ψ

source

theorem KroneckerWeber.theorem_11_23_completion_exists_galois (K : Type u_1) [Field K] [Algebra ℚ K] [IsGalois ℚ K] [FiniteDimensional ℚ K] (p : ℕ) [Fact (Nat.Prime p)] :

∃ (E : Type) (hF : Field E) (hA : Algebra ℚ_[p] E) (_ : IsGalois ℚ_[p] E) (_ : FiniteDimensional ℚ_[p] E), Module.finrank ℚ_[p] E ≤ Module.finrank ℚ K ∧ ∃ (φ : Gal(E/ℚ_[p]) →* Gal(K/ℚ)), Function.Injective ⇑φ

source

theorem KroneckerWeber.theorem_11_23_local_completion_is_abelian (K : Type u_1) [Field K] [Algebra ℚ K] [hab : IsAbelianExtension ℚ K] [FiniteDimensional ℚ K] (p : ℕ) [Fact (Nat.Prime p)] :

∃ (E : Type) (hF : Field E) (hA : Algebra ℚ_[p] E) (_ : IsAbelianExtension ℚ_[p] E) (_ : FiniteDimensional ℚ_[p] E), Module.finrank ℚ_[p] E ≤ Module.finrank ℚ K ∧ ∃ (φ : Gal(E/ℚ_[p]) →* Gal(K/ℚ)), Function.Injective ⇑φ

source

theorem KroneckerWeber.conductor_from_local_cyclotomic_data (K : Type u_1) [Field K] [Algebra ℚ K] [IsAbelianExtension ℚ K] [FiniteDimensional ℚ K] (local_data : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ (E : Type) (x : Field E) (x_1 : Algebra ℚ_[p] E) (_ : IsAbelianExtension ℚ_[p] E) (_ : FiniteDimensional ℚ_[p] E), LiesInCyclotomicExtension ℚ_[p] E) :

∃ (m : ℕ) (_ : m ≥ 1) (L_m : Type) (hFL : Field L_m) (hAL : Algebra ℚ L_m), IsCyclotomicExtension {m} ℚ L_m

source

theorem KroneckerWeber.inertia_minkowski_gives_embedding (K : Type u_1) [Field K] [Algebra ℚ K] [IsAbelianExtension ℚ K] [FiniteDimensional ℚ K] (local_data : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ (E : Type) (x : Field E) (x_1 : Algebra ℚ_[p] E) (_ : IsAbelianExtension ℚ_[p] E) (_ : FiniteDimensional ℚ_[p] E), LiesInCyclotomicExtension ℚ_[p] E) (m : ℕ) (hm : m ≥ 1) (L_m : Type) (hFL : Field L_m) (hAL : Algebra ℚ L_m) (hcyc : IsCyclotomicExtension {m} ℚ L_m) :

Nonempty (K →ₐ[ℚ ] L_m)

source

theorem KroneckerWeber.conductor_inertia_argument (K : Type u_1) [Field K] [Algebra ℚ K] [IsAbelianExtension ℚ K] [FiniteDimensional ℚ K] (local_data : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ (E : Type) (x : Field E) (x_1 : Algebra ℚ_[p] E) (_ : IsAbelianExtension ℚ_[p] E) (_ : FiniteDimensional ℚ_[p] E), LiesInCyclotomicExtension ℚ_[p] E) :

LiesInCyclotomicExtension ℚ K

source

theorem KroneckerWeber.proposition_20_3 (K : Type u_1) [Field K] [Algebra ℚ K] [IsAbelianExtension ℚ K] [FiniteDimensional ℚ K] (localKW : ∀ (p : ℕ) (x : Fact (Nat.Prime p)) (E : Type) [inst : Field E] [inst_1 : Algebra ℚ_[p] E] [IsAbelianExtension ℚ_[p] E] [FiniteDimensional ℚ_[p] E], LiesInCyclotomicExtension ℚ_[p] E) :

LiesInCyclotomicExtension ℚ K

source

theorem KroneckerWeber.theorem_20_1 (K : Type u_1) [Field K] [Algebra ℚ K] [IsAbelianExtension ℚ K] [FiniteDimensional ℚ K] :

LiesInCyclotomicExtension ℚ K

source

theorem KroneckerWeber.no_Z4Z_cube_extension :

¬∃ (K : Type) (x : Field K) (x_1 : Algebra ℚ_[2] K) (_ : FiniteDimensional ℚ_[2] K) (_ : IsGalois ℚ_[2] K), Nonempty (Gal(K/ℚ_[2]) ≃* Multiplicative (ZMod 4 × ZMod 4 × ZMod 4))

Alias of KroneckerWeber.lemma_20_11_no_Z4Z3.

source

def KroneckerWeber.completion_integers_algebra (A : Type u_A₄) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_K₄) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_L₄) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_B₄) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] :

Algebra ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K 𝔭) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)

Alias of KroneckerWeber.prop_8_11_completion_integers_algebra.

Instances For

source

def no_Z4Z_cube_extension :

¬∃ (K : Type) (x : Field K) (x_1 : Algebra ℚ_[2] K) (_ : FiniteDimensional ℚ_[2] K) (_ : IsGalois ℚ_[2] K), Nonempty (Gal(K/ℚ_[2]) ≃* Multiplicative (ZMod 4 × ZMod 4 × ZMod 4))

Instances For

source

def theorem_20_6 (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [KroneckerWeber.IsCyclicExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (r : ℕ) (hdeg : Module.finrank ℚ_[p] K = p ^ r) :

KroneckerWeber.LiesInCyclotomicExtension ℚ_[p] K

Instances For

source

def theorem_20_10 (K : Type u_1) [Field K] [Algebra ℚ_[2] K] [KroneckerWeber.IsCyclicExtension ℚ_[2] K] [FiniteDimensional ℚ_[2] K] (r : ℕ) (hdeg : Module.finrank ℚ_[2] K = 2 ^ r) :

KroneckerWeber.LiesInCyclotomicExtension ℚ_[2] K

Instances For

source

def theorem_20_2 (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type) [Field K] [Algebra ℚ_[p] K] [KroneckerWeber.IsAbelianExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] :

KroneckerWeber.LiesInCyclotomicExtension ℚ_[p] K

Instances For

source

def theorem_20_1 (K : Type u_1) [Field K] [Algebra ℚ K] [KroneckerWeber.IsAbelianExtension ℚ K] [FiniteDimensional ℚ K] :

KroneckerWeber.LiesInCyclotomicExtension ℚ K

Instances For

source

def proposition_20_3 (K : Type u_1) [Field K] [Algebra ℚ K] [KroneckerWeber.IsAbelianExtension ℚ K] [FiniteDimensional ℚ K] (localKW : ∀ (p : ℕ) (x : Fact (Nat.Prime p)) (E : Type) [inst : Field E] [inst_1 : Algebra ℚ_[p] E] [KroneckerWeber.IsAbelianExtension ℚ_[p] E] [FiniteDimensional ℚ_[p] E], KroneckerWeber.LiesInCyclotomicExtension ℚ_[p] E) :

KroneckerWeber.LiesInCyclotomicExtension ℚ K

Instances For

source

def proposition_20_4 (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [Algebra ℚ_[p] K] [KroneckerWeber.IsCyclicExtension ℚ_[p] K] [FiniteDimensional ℚ_[p] K] (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (hℓp : ℓ ≠ p) (r : ℕ) (hdeg : Module.finrank ℚ_[p] K = ℓ ^ r) :

KroneckerWeber.LiesInCyclotomicExtension ℚ_[p] K

Instances For

source

def proposition_20_7_no_ZpZ3 (p : ℕ) [Fact (Nat.Prime p)] (hp : p ≠ 2) :

¬∃ (K : Type) (x : Field K) (x_1 : Algebra ℚ_[p] K) (_ : FiniteDimensional ℚ_[p] K) (_ : IsGalois ℚ_[p] K), Nonempty (Gal(K/ℚ_[p]) ≃* Multiplicative (ZMod p × ZMod p × ZMod p))

Instances For

source

def lemma_20_5 (p : ℕ) [Fact (Nat.Prime p)] :

Instances For

source

def lemma_20_11 :

Instances For

source

def theorem_11_23_AKLB (A : Type u_1) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_4) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) :

∃ (L_𝔮 : Type u_3) (inst_field : Field L_𝔮) (inst_alg : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) L_𝔮), FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) L_𝔮 ∧ Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) L_𝔮 ≤ Module.finrank K L ∧ Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) L_𝔮 = 𝔭.asIdeal.ramificationIdx 𝔮.asIdeal * 𝔭.asIdeal.inertiaDeg 𝔮.asIdeal ∧ (IsGalois K L → IsGalois (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) L_𝔮 ∧ ∃ (φ : Gal(L_𝔮/IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) →* Gal(L/K)), Function.Injective ⇑φ)

Instances For

source

def theorem_11_23_part1_separable (A : Type u_1) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [CharZero K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_4) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [IsScalarTower K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] :

Algebra.IsSeparable (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)

Instances For

source

def theorem_11_23_part2_unique_prime (A : Type u_1) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_4) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) :

IsDiscreteValuationRing ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L 𝔮)

Instances For

source

def theorem_11_23_part3_ramification_preserved (A : Type u_1) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_4) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [IsScalarTower K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K 𝔭) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L 𝔮)] :

Instances For

source

def theorem_11_23_part5_tensor_product_decomp (A : Type u_1) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_4) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] [IsFractionRing B L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (primesOver : Finset (IsDedekindDomain.HeightOneSpectrum B)) (hPrimesOver : ∀ 𝔮 ∈ primesOver, 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) (hPrimesOverImage : Finset.image IsDedekindDomain.HeightOneSpectrum.asIdeal primesOver = primesOverFinset 𝔭.asIdeal B) :

Instances For

source

def thm_11_23_part6_galois_implication (A : Type u_1) [CommRing A] [IsDedekindDomain A] [IsDomain A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_4) [CommRing B] [IsDomain B] [IsDedekindDomain B] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsIntegralClosure B A L] (𝔭 : IsDedekindDomain.HeightOneSpectrum A) (𝔮 : IsDedekindDomain.HeightOneSpectrum B) (h𝔮_over_𝔭 : 𝔭.asIdeal ≤ Ideal.comap (algebraMap A B) 𝔮.asIdeal) [IsFractionRing B L] [𝔮.asIdeal.LiesOver 𝔭.asIdeal] (hgal : IsGalois K L) :

Instances For

source

Instances For