NYLL
Module

KummerAbelianCyclicFactors.lean

Nyll.GaloisCohomology.Kummer.Abstract.KummerAbelianCyclicFactors
17 declarations indexed from sourceView source ↗

Module documentation

finite abelian Kummer theory, the finite abelian Kummer decomposition: cyclic factors of a finite

abelian extension

The proof of the finite abelian Kummer decomposition reduces a finite abelian extension to cyclic subextensions. This file supplies the group-theoretic source for that step. A finite commutative group is written as a finite product of cyclic ZMod groups. The kernels of its coordinate maps have trivial intersection. Pulling those kernels back along a quotient map produces intermediate subgroups whose quotients are finite cyclic and whose intersection is the original normal subgroup.

No radical generators or field-lattice endpoint are asserted here.

Imports2
Imported by2

Declarations

theorem

finiteCommGroup_exists_jointlyFaithful_cyclic_factors

L37 ↗
KummerTheory.finiteCommGroup_exists_jointlyFaithful_cyclic_factors
Documentation

Coordinate characters obtained from the structure theorem separate the elements of a finite commutative group.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section FiniteAbelianCyclicFactors
Lean source · statement
theorem finiteCommGroup_exists_jointlyFaithful_cyclic_factors
    (Q : Type*) [CommGroup Q] [Finite Q] :
    ∃ (ι : Type 0) (_ : Fintype ι) (m : ι → ℕ),
      (∀ i, 1 < m i) ∧
      ∃ f : ∀ i, Q →* Multiplicative (ZMod (m i)),
        (∀ i, Function.Surjective (f i)) ∧
        (⨅ i, MonoidHom.ker (f i)) = ⊥
def

cyclicFactorSubgroup

L67 ↗
KummerTheory.cyclicFactorSubgroup
Documentation

Pull a quotient-factor kernel back to the original group.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section FiniteAbelianCyclicFactors
section Pullback
variable {P C : Type*} [Group P] [Group C]
  (H : Subgroup P) [H.Normal]
Lean source · statement
def cyclicFactorSubgroup (f : (P ⧸ H) →* C) : Subgroup P
instance

cyclicFactorSubgroup_normal

L71 ↗
KummerTheory.cyclicFactorSubgroup_normal
Documentation

The kernel subgroup attached to a cyclic quotient factor is normal.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section FiniteAbelianCyclicFactors
section Pullback
variable {P C : Type*} [Group P] [Group C]
  (H : Subgroup P) [H.Normal]
Lean source · statement
instance cyclicFactorSubgroup_normal (f : (P ⧸ H) →* C) :
    (cyclicFactorSubgroup H f).Normal
theorem

le_cyclicFactorSubgroup

L76 ↗
KummerTheory.le_cyclicFactorSubgroup
Documentation

The original normal subgroup lies in every pulled-back factor kernel.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section FiniteAbelianCyclicFactors
section Pullback
variable {P C : Type*} [Group P] [Group C]
  (H : Subgroup P) [H.Normal]
Lean source · statement
theorem le_cyclicFactorSubgroup (f : (P ⧸ H) →* C) :
    H ≤ cyclicFactorSubgroup H f
theorem

cyclic_cyclicFactorSubgroup_quotient

L86 ↗
KummerTheory.cyclic_cyclicFactorSubgroup_quotient
Documentation

A surjective cyclic factor gives a cyclic quotient of the original group by its pulled-back kernel.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section FiniteAbelianCyclicFactors
section Pullback
variable {P C : Type*} [Group P] [Group C]
  (H : Subgroup P) [H.Normal]
Lean source · statement
theorem cyclic_cyclicFactorSubgroup_quotient
    [IsCyclic C] (f : (P ⧸ H) →* C) (hf : Function.Surjective f) :
    IsCyclic (P ⧸ cyclicFactorSubgroup H f)
theorem

finite_cyclicFactorSubgroup_quotient

L98 ↗
KummerTheory.finite_cyclicFactorSubgroup_quotient
Documentation

If the cyclic factor is finite, so is the corresponding quotient.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section FiniteAbelianCyclicFactors
section Pullback
variable {P C : Type*} [Group P] [Group C]
  (H : Subgroup P) [H.Normal]
Lean source · statement
theorem finite_cyclicFactorSubgroup_quotient
    [Finite C] (f : (P ⧸ H) →* C) (hf : Function.Surjective f) :
    Finite (P ⧸ cyclicFactorSubgroup H f)
theorem

iInf_cyclicFactorSubgroup_eq

L113 ↗
KummerTheory.iInf_cyclicFactorSubgroup_eq
Documentation

Jointly faithful quotient factors pull back to subgroups whose intersection is exactly the original normal subgroup.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section FiniteAbelianCyclicFactors
section Pullback
variable {P C : Type*} [Group P] [Group C]
  (H : Subgroup P) [H.Normal]
variable {ι : Type*} {Cι : ι → Type*} [∀ i, Group (Cι i)]
Lean source · statement
theorem iInf_cyclicFactorSubgroup_eq
    (f : ∀ i, (P ⧸ H) →* Cι i)
    (hfaithful : (⨅ i, MonoidHom.ker (f i)) = ⊥) :
    (⨅ i, cyclicFactorSubgroup H (f i)) = H
theorem

extensionSubgroup_isClosed

L137 ↗
KummerTheory.extensionSubgroup_isClosed
Documentation

A closed abstract field subgroup G_L remains closed when regarded as a subgroup of the larger abstract field subgroup G_K.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section ClosedCyclicSubextensions
variable {G : Type*} [Group G] [TopologicalSpace G]
Lean source · statement
theorem extensionSubgroup_isClosed
    {G : Type*} [Group G] [TopologicalSpace G]
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup) :
    IsClosed (extensionSubgroup (G := G) K L hLK : Set K.toSubgroup)
theorem

cyclicFactorSubgroup_isClosed

L149 ↗
KummerTheory.cyclicFactorSubgroup_isClosed
Documentation

A pulled-back cyclic factor kernel is closed inside G_K: the finite quotient by G_L is discrete, and the factor kernel is pulled back along the continuous quotient map.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section ClosedCyclicSubextensions
variable {G : Type*} [Group G] [TopologicalSpace G]
variable [IsTopologicalGroup G]
Lean source · statement
theorem cyclicFactorSubgroup_isClosed
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup (G := G) K L hLK).Normal]
    [hfinite : Finite (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK)]
    {C : Type*} [Group C]
    (f : (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK) →* C) :
    IsClosed
      (cyclicFactorSubgroup (extensionSubgroup (G := G) K L hLK) f :
        Set K.toSubgroup)
def

closedCyclicFactorSubgroup

L166 ↗
KummerTheory.closedCyclicFactorSubgroup
Documentation

The closed abstract intermediate field attached to one cyclic coordinate factor of G_K/G_L.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section ClosedCyclicSubextensions
variable {G : Type*} [Group G] [TopologicalSpace G]
variable [IsTopologicalGroup G]
Lean source · full declaration
def closedCyclicFactorSubgroup
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup (G := G) K L hLK).Normal]
    [hfinite : Finite (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK)]
    {C : Type*} [Group C]
    (f : (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK) →* C) :
    ClosedSubgroup G where
  toSubgroup :=
    (cyclicFactorSubgroup (extensionSubgroup (G := G) K L hLK) f).map
      K.toSubgroup.subtype
  isClosed' := by
    change IsClosed
      ((fun x : K.toSubgroup => (x : G)) ''
        (cyclicFactorSubgroup (extensionSubgroup (G := G) K L hLK) f :
          Set K.toSubgroup))
    exact K.isClosed'.isClosedMap_subtype_val _
      (cyclicFactorSubgroup_isClosed K L hLK f)
theorem

closedCyclicFactorSubgroup_le_base

L186 ↗
KummerTheory.closedCyclicFactorSubgroup_le_base
Documentation

The cyclic-factor intermediate subgroup lies below the base subgroup G_K.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section ClosedCyclicSubextensions
variable {G : Type*} [Group G] [TopologicalSpace G]
variable [IsTopologicalGroup G]
Lean source · statement
theorem closedCyclicFactorSubgroup_le_base
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup (G := G) K L hLK).Normal]
    [hfinite : Finite (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK)]
    {C : Type*} [Group C]
    (f : (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK) →* C) :
    (closedCyclicFactorSubgroup K L hLK f).toSubgroup ≤ K.toSubgroup
theorem

le_closedCyclicFactorSubgroup

L199 ↗
KummerTheory.le_closedCyclicFactorSubgroup
Documentation

The original subgroup G_L lies below every cyclic-factor intermediate subgroup. Finiteness is needed by the closed intermediate object itself: it makes the quotient discrete, hence its pulled-back kernel closed.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section ClosedCyclicSubextensions
variable {G : Type*} [Group G] [TopologicalSpace G]
variable [IsTopologicalGroup G]
Lean source · statement
theorem le_closedCyclicFactorSubgroup
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup (G := G) K L hLK).Normal]
    [hfinite : Finite (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK)]
    {C : Type*} [Group C]
    (f : (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK) →* C) :
    L.toSubgroup ≤
      (closedCyclicFactorSubgroup (hfinite := hfinite) K L hLK f).toSubgroup
theorem

extensionSubgroup_closedCyclicFactorSubgroup_eq

L217 ↗
KummerTheory.extensionSubgroup_closedCyclicFactorSubgroup_eq
Documentation

Viewed inside G_K, the closed cyclic-factor subgroup has exactly the pulled-back coordinate kernel as its extension subgroup.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section ClosedCyclicSubextensions
variable {G : Type*} [Group G] [TopologicalSpace G]
variable [IsTopologicalGroup G]
Lean source · statement
theorem extensionSubgroup_closedCyclicFactorSubgroup_eq
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup (G := G) K L hLK).Normal]
    [hfinite : Finite (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK)]
    {C : Type*} [Group C]
    (f : (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK) →* C) :
    extensionSubgroup (G := G) K (closedCyclicFactorSubgroup K L hLK f)
        (closedCyclicFactorSubgroup_le_base K L hLK f) =
      cyclicFactorSubgroup (extensionSubgroup (G := G) K L hLK) f
instance

extensionSubgroup_closedCyclicFactorSubgroup_normal

L237 ↗
KummerTheory.extensionSubgroup_closedCyclicFactorSubgroup_normal
Documentation

The extension subgroup of a closed cyclic factor is normal in G_K.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section ClosedCyclicSubextensions
variable {G : Type*} [Group G] [TopologicalSpace G]
variable [IsTopologicalGroup G]
Lean source · statement
instance extensionSubgroup_closedCyclicFactorSubgroup_normal
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup (G := G) K L hLK).Normal]
    [hfinite : Finite (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK)]
    {C : Type*} [Group C]
    (f : (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK) →* C) :
    (extensionSubgroup (G := G) K (closedCyclicFactorSubgroup K L hLK f)
      (closedCyclicFactorSubgroup_le_base K L hLK f)).Normal
theorem

finite_extensionSubgroup_closedCyclicFactorSubgroup_quotient

L250 ↗
KummerTheory.finite_extensionSubgroup_closedCyclicFactorSubgroup_quotient
Documentation

The quotient attached to a surjective finite cyclic coordinate is finite.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section ClosedCyclicSubextensions
variable {G : Type*} [Group G] [TopologicalSpace G]
variable [IsTopologicalGroup G]
Lean source · statement
theorem finite_extensionSubgroup_closedCyclicFactorSubgroup_quotient
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup (G := G) K L hLK).Normal]
    [hfinite : Finite (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK)]
    {C : Type*} [Group C] [Finite C]
    (f : (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK) →* C)
    (hf : Function.Surjective f) :
    Finite
      (K.toSubgroup ⧸
        extensionSubgroup (G := G) K (closedCyclicFactorSubgroup K L hLK f)
          (closedCyclicFactorSubgroup_le_base K L hLK f))
theorem

cyclic_extensionSubgroup_closedCyclicFactorSubgroup_quotient

L266 ↗
KummerTheory.cyclic_extensionSubgroup_closedCyclicFactorSubgroup_quotient
Documentation

The quotient attached to a surjective cyclic coordinate is cyclic.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section ClosedCyclicSubextensions
variable {G : Type*} [Group G] [TopologicalSpace G]
variable [IsTopologicalGroup G]
Lean source · statement
theorem cyclic_extensionSubgroup_closedCyclicFactorSubgroup_quotient
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup (G := G) K L hLK).Normal]
    [hfinite : Finite (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK)]
    {C : Type*} [Group C] [IsCyclic C]
    (f : (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK) →* C)
    (hf : Function.Surjective f) :
    IsCyclic
      (K.toSubgroup ⧸
        extensionSubgroup (G := G) K (closedCyclicFactorSubgroup K L hLK f)
          (closedCyclicFactorSubgroup_le_base K L hLK f))
theorem

extensionSubgroup_closedCyclicFactorSubgroup_quotient_pow_eq_one

L285 ↗
KummerTheory.extensionSubgroup_closedCyclicFactorSubgroup_quotient_pow_eq_one
Documentation

An exponent bound on G_K/G_L descends to the quotient attached to a closed cyclic coordinate.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open CyclicCohomology
noncomputable section
section ClosedCyclicSubextensions
variable {G : Type*} [Group G] [TopologicalSpace G]
variable [IsTopologicalGroup G]
Lean source · statement
theorem extensionSubgroup_closedCyclicFactorSubgroup_quotient_pow_eq_one
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup (G := G) K L hLK).Normal]
    [hfinite : Finite (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK)]
    {C : Type*} [Group C]
    (f : (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK) →* C)
    {n : ℕ}
    (hexponent : ∀ q : K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK,
      q ^ n = 1) :
    ∀ q : K.toSubgroup ⧸
        extensionSubgroup (G := G) K (closedCyclicFactorSubgroup K L hLK f)
          (closedCyclicFactorSubgroup_le_base K L hLK f),
      q ^ n = 1

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.