Module

KummerAbelianAssembly.lean

Nyll.GaloisCohomology.Kummer.Abstract.KummerAbelianAssembly

6 declarations indexed from sourceView source ↗

Module documentation

finite abelian Kummer theory, the finite abelian Kummer decomposition: assembling cyclic radicals

This file connects elements produced in the invariant subtype A_M to the ambient representation A. A cyclic radical with trivial stabilizer in G_K / G_M is fixed in the ambient module by exactly G_M. Consequently, a family of such radicals whose subgroups intersect in G_L generates the abstract field L over K.

Imports2

Imported by2

theorem

mem_extensionSubgroup_iff

L33 ↗

KummerTheory.mem_extensionSubgroup_iff

Documentation

Membership in G_L, regarded as a subgroup of G_K, is the same as ambient membership in the closed subgroup G_L.

Source context 4 commands

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

namespace KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]

Lean source · statement

theorem mem_extensionSubgroup_iff
    {G : Type*} [Group G] [TopologicalSpace G]
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    (k : K.toSubgroup) :
    k ∈ extensionSubgroup (G := G) K L hLK ↔ (k : G) ∈ L

theorem

extensionFixedRepresentation_quotient_mk_apply_val

L43 ↗

KummerTheory.extensionFixedRepresentation_quotient_mk_apply_val

Documentation

The quotient action on an invariant subtype is the original ambient action after choosing a representative in G_K.

Source context 4 commands

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

namespace KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]

Lean source · statement

theorem extensionFixedRepresentation_quotient_mk_apply_val
    (A : Rep ℤ G) (K M : ClosedSubgroup G)
    (hMK : M.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup (G := G) K M hMK).Normal]
    (a : (extensionFixedRepresentation A K M hMK hnormal).V)
    (k : K.toSubgroup) :
    ((extensionFixedRepresentation A K M hMK hnormal).ρ
      ((QuotientGroup.mk' (extensionSubgroup (G := G) K M hMK)) k) a).1 =
      A.ρ k.1 a.1

theorem

extensionFixedRepresentation_val_fixed_iff_mem

L55 ↗

KummerTheory.extensionFixedRepresentation_val_fixed_iff_mem

Documentation

If an element of A_M has trivial stabilizer under G_K/G_M, its ambient value is fixed by k : G_K exactly when k belongs to G_M.

Source context 4 commands

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

namespace KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]

Lean source · statement

theorem extensionFixedRepresentation_val_fixed_iff_mem
    (A : Rep ℤ G) (K M : ClosedSubgroup G)
    (hMK : M.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup (G := G) K M hMK).Normal]
    (a : (extensionFixedRepresentation A K M hMK hnormal).V)
    (hstabilizer :
      representationStabilizer (extensionFixedRepresentation A K M hMK hnormal) a = ⊥)
    (k : K.toSubgroup) :
    A.ρ k.1 a.1 = a.1 ↔
      k ∈ extensionSubgroup (G := G) K M hMK

theorem

extensionFixedEndomorphism_fixed_val

L86 ↗

KummerTheory.extensionFixedEndomorphism_fixed_val

Documentation

Quotient-fixedness of the descended global operator says precisely that the ambient value wp(a) is fixed by G_K.

Source context 4 commands

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

namespace KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]

Lean source · statement

theorem extensionFixedEndomorphism_fixed_val
    (A : Rep ℤ G) (K M : ClosedSubgroup G)
    (hMK : M.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup (G := G) K M hMK).Normal]
    (wp : A ⟶ A)
    (a : (extensionFixedRepresentation A K M hMK hnormal).V)
    (hfixed : ∀ q : K.toSubgroup ⧸ extensionSubgroup (G := G) K M hMK,
      (extensionFixedRepresentation A K M hMK hnormal).ρ q
          ((extensionFixedEndomorphism A K M hMK wp).hom a) =
        (extensionFixedEndomorphism A K M hMK wp).hom a)
    (k : K.toSubgroup) :
    A.ρ k.1 (wp.hom a.1) = wp.hom a.1

theorem

closedSetFixingSubgroup_range_extensionFixed_eq

L106 ↗

KummerTheory.closedSetFixingSubgroup_range_extensionFixed_eq

Documentation

A family of faithful cyclic radicals generates L once the associated subgroups intersect in G_L. The generation conclusion is derived from the radicals' stabilizers; it is not an input.

Source context 4 commands

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

namespace KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]

Lean source · full declaration

theorem closedSetFixingSubgroup_range_extensionFixed_eq
    [IsTopologicalGroup G]
    (A : Rep ℤ G) (hcontinuous : IsContinuousDiscreteRepresentation A)
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    {iota : Type*}
    (M : iota → ClosedSubgroup G)
    (hMK : ∀ i, (M i).toSubgroup ≤ K.toSubgroup)
    (hnormalM : ∀ i, (extensionSubgroup (G := G) K (M i) (hMK i)).Normal)
    (a : ∀ i,
      (extensionFixedRepresentation A K (M i) (hMK i) (hnormalM i)).V)
    (hstabilizer : ∀ i,
      representationStabilizer
        (extensionFixedRepresentation A K (M i) (hMK i) (hnormalM i)) (a i) = ⊥)
    (hintersect :
      (⨅ i, extensionSubgroup (G := G) K (M i) (hMK i)) =
        extensionSubgroup (G := G) K L hLK) :
    closedSetFixingSubgroup A hcontinuous K (Set.range fun i => (a i).1) = L := by
  ext sigma
  change sigma ∈
      closedSetFixingSubgroup A hcontinuous K (Set.range fun i => (a i).1) ↔
    sigma ∈ L
  rw [mem_closedSetFixingSubgroup_iff]
  constructor
  · rintro ⟨hsigmaK, hfix⟩
    let k : K.toSubgroup := ⟨sigma, hsigmaK⟩
    have hk_all : k ∈ ⨅ i, extensionSubgroup (G := G) K (M i) (hMK i) := by
      rw [Subgroup.mem_iInf]
      intro i
      apply (extensionFixedRepresentation_val_fixed_iff_mem
        A K (M i) (hMK i) (a i) (hstabilizer i) k).1
      exact hfix (a i).1 ⟨i, rfl⟩
    have hkL : k ∈ extensionSubgroup (G := G) K L hLK := by
      rw [← hintersect]
      exact hk_all
    exact (mem_extensionSubgroup_iff K L hLK k).1 hkL
  · intro hsigmaL
    have hsigmaK : sigma ∈ K := hLK hsigmaL
    refine ⟨hsigmaK, ?_⟩
    rintro _ ⟨i, rfl⟩
    let k : K.toSubgroup := ⟨sigma, hsigmaK⟩
    apply (extensionFixedRepresentation_val_fixed_iff_mem
      A K (M i) (hMK i) (a i) (hstabilizer i) k).2
    have hkL : k ∈ extensionSubgroup (G := G) K L hLK :=
      (mem_extensionSubgroup_iff K L hLK k).2 hsigmaL
    have hk_all : k ∈ ⨅ j, extensionSubgroup (G := G) K (M j) (hMK j) := by
      rw [hintersect]
      exact hkL
    exact (Subgroup.mem_iInf.mp hk_all) i

theorem

finiteAbelian_globalOperator_generators

L163 ↗

KummerTheory.finiteAbelian_globalOperator_generators

Documentation

Finite abelian endpoint of the forward direction of the finite abelian Kummer decomposition.

The finite abelian quotient is decomposed into cyclic coordinates. The global cyclic-operator theorem produces one radical for each coordinate; their ambient values form a finite set S. The conclusions say that wp(S) is fixed by G_K (the abstract Delta inclusion) and that the pointwise fixing subgroup of S is exactly G_L (the generation L = K(S)).

Source context 4 commands

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

namespace KummerTheory
open CyclicCohomology
noncomputable section
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]

Lean source · statement

theorem finiteAbelian_globalOperator_generators
    [IsTopologicalGroup G]
    (A : Rep ℤ G) (hAxiom : SatisfiesCyclicNormKernelVanishing A)
    (hcontinuous : IsContinuousDiscreteRepresentation A)
    (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)]
    [IsMulCommutative
      (K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK)]
    (wp : A ⟶ A) (n : ℕ+) (xi : A.V)
    (hxi_order : addOrderOf xi = (n : ℕ))
    (hxi_kernel : wp.hom xi = 0)
    (hxi_fixed : ∀ k : K.toSubgroup, A.ρ k.1 xi = xi)
    (hexponent :
      ∀ q : K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK,
        q ^ (n : ℕ) = 1) :
    ∃ S : Set A.V,
      S.Finite ∧
      (∀ a, a ∈ S → ∀ k : K.toSubgroup,
        A.ρ k.1 (wp.hom a) = wp.hom a) ∧
      closedSetFixingSubgroup A hcontinuous K S = L

Module documentation

finite abelian Kummer theory, the finite abelian Kummer decomposition: assembling cyclic radicals

Declarations

mem_extensionSubgroup_iff

extensionFixedRepresentation_quotient_mk_apply_val

extensionFixedRepresentation_val_fixed_iff_mem

extensionFixedEndomorphism_fixed_val

closedSetFixingSubgroup_range_extensionFixed_eq

finiteAbelian_globalOperator_generators