Documentation

Atlas.NumberTheoryI.code.KroneckerWeberLocal2

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

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

Instances

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

Instances For

theorem KroneckerWeberLocal2.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

theorem KroneckerWeberLocal2.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 }

def KroneckerWeberLocal2.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

theorem KroneckerWeberLocal2.ps4_at_most_7_quadratic_extensions (K : Type) [Field K] [Algebra ℚ_[2] K] [FiniteDimensional ℚ_[2] K] :

Nat.card { L : IntermediateField ℚ_[2] K // Module.finrank ℚ_[2] ↥L = 2 } ≤ 7

theorem KroneckerWeberLocal2.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

theorem KroneckerWeberLocal2.Z2Z4_index2_count :

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

theorem KroneckerWeberLocal2.ps5_at_most_12_cyclic_quartic_extensions (K : Type) [Field K] [Algebra ℚ_[2] K] [FiniteDimensional ℚ_[2] K] :

Nat.card { L : IntermediateField ℚ_[2] K // Module.finrank ℚ_[2] ↥L = 4 ∧ IsGalois ℚ_[2] ↥L ∧ IsCyclic Gal(↥L/ℚ_[2]) } ≤ 12

theorem KroneckerWeberLocal2.ps5_galois_cyclic_quartic_bound (K : Type) (x✝ : Field K) (x✝¹ : 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

theorem KroneckerWeberLocal2.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

theorem KroneckerWeberLocal2.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

theorem KroneckerWeberLocal2.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) }

theorem KroneckerWeberLocal2.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))

theorem KroneckerWeberLocal2.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))

theorem KroneckerWeberLocal2.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))

theorem KroneckerWeberLocal2.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)

theorem KroneckerWeberLocal2.cor_10_17_18_galois_group_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) :

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

theorem KroneckerWeberLocal2.surjective_toMultiplicative {A : Type u_1} {B : Type u_2} [AddCommMonoid A] [AddCommMonoid B] (f : A →+ B) (hf : Function.Surjective ⇑f) :

Function.Surjective ⇑(AddMonoidHom.toMultiplicative f)

theorem KroneckerWeberLocal2.addMonoidHom_prodMap_surjective {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') (hf : Function.Surjective ⇑f) (hg : Function.Surjective ⇑g) :

Function.Surjective ⇑(f.prodMap g)

theorem KroneckerWeberLocal2.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 ⇑φ

theorem KroneckerWeberLocal2.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))

theorem KroneckerWeberLocal2.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