Module

KummerDelta.lean

Nyll.GaloisCohomology.Kummer.Abstract.KummerDelta

7 declarations indexed from sourceView source ↗

Module documentation

finite abelian Kummer theory, the finite abelian Kummer decomposition: the exact Delta

For an equivariant additive operator wp, the construction defines Delta = wp(A_L) ∩ A_K. Here fixed modules are represented as ambient additive subgroups. The finite abelian assembly supplies finitely many elements in wp⁻¹(Delta) generating L; the reverse fixing inclusion uses the construction datum that the kernel of wp is generated by its distinguished element xi.

Imports3

Imported by5

def

ambientFixedAddSubgroup

L34 ↗

KummerTheory.ambientFixedAddSubgroup

Documentation

Ambient coefficient elements fixed pointwise by a closed abstract field subgroup.

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

def ambientFixedAddSubgroup (A : Rep ℤ G) (H : ClosedSubgroup G) :
    AddSubgroup A.V

theorem

mem_ambientFixedAddSubgroup_iff

L49 ↗

KummerTheory.mem_ambientFixedAddSubgroup_iff

Documentation

Membership in the ambient fixed subgroup is equivalent to invariance under every subgroup element.

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_ambientFixedAddSubgroup_iff
    (A : Rep ℤ G) (H : ClosedSubgroup G) (a : A.V) :
    a ∈ ambientFixedAddSubgroup A H ↔
      ∀ h : H.toSubgroup, A.ρ h.1 a = a

def

kummerDeltaAddSubgroup

L57 ↗

KummerTheory.kummerDeltaAddSubgroup

Documentation

The Delta = wp(A_L) ∩ A_K, as an additive subgroup of the ambient coefficient module.

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

def kummerDeltaAddSubgroup
    (A : Rep ℤ G) (wp : A ⟶ A) (K L : ClosedSubgroup G) :
    AddSubgroup A.V

def

kummerRadicalAddSubgroup

L65 ↗

KummerTheory.kummerRadicalAddSubgroup

Documentation

The radical set wp⁻¹(Delta) in the additive abstract model.

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

def kummerRadicalAddSubgroup
    (A : Rep ℤ G) (wp : A ⟶ A) (K L : ClosedSubgroup G) :
    AddSubgroup A.V

theorem

mem_kummerRadicalAddSubgroup_iff

L73 ↗

KummerTheory.mem_kummerRadicalAddSubgroup_iff

Documentation

The Kummer radical consists of fixed elements annihilated by the Kummer exponent.

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_kummerRadicalAddSubgroup_iff
    (A : Rep ℤ G) (wp : A ⟶ A) (K L : ClosedSubgroup G) (a : A.V) :
    a ∈ kummerRadicalAddSubgroup A wp K L ↔
      wp.hom a ∈ kummerDeltaAddSubgroup A wp K L

theorem

kummerRadical_fixed_of_ker_le_zmultiples

L82 ↗

KummerTheory.kummerRadical_fixed_of_ker_le_zmultiples

Documentation

If ker(wp) is generated by the G_K-fixed element xi, every member of wp⁻¹(wp(A_L) ∩ A_K) is fixed by G_L. Only the inclusion ker(wp) ≤ ℤ xi is needed for this direction.

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 kummerRadical_fixed_of_ker_le_zmultiples
    (A : Rep ℤ G) (wp : A ⟶ A) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (xi : A.V)
    (hxi_fixed : ∀ k : K.toSubgroup, A.ρ k.1 xi = xi)
    (hker : AddMonoidHom.ker (AddMonoidHom.ofClass wp.hom) ≤
      AddSubgroup.zmultiples xi)
    {a : A.V} (ha : a ∈ kummerRadicalAddSubgroup A wp K L)
    (l : L.toSubgroup) :
    A.ρ l.1 a = a

theorem

finiteAbelian_kummerRadical_fixingSubgroup_eq

L122 ↗

KummerTheory.finiteAbelian_kummerRadical_fixingSubgroup_eq

Documentation

Exact finite-abelian Delta endpoint of the finite abelian Kummer decomposition: L = K(wp⁻¹(wp(A_L) ∩ A_K)).

The cyclic factors, their radical generators, and the inclusion of those generators in wp⁻¹(Delta) are constructed in the proof. The only additional operator datum beyond the finite assembly is the kernel generation condition.

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_kummerRadical_fixingSubgroup_eq
    [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)
    (hker : AddMonoidHom.ker (AddMonoidHom.ofClass wp.hom) ≤
      AddSubgroup.zmultiples xi)
    (hexponent :
      ∀ q : K.toSubgroup ⧸ extensionSubgroup (G := G) K L hLK,
        q ^ (n : ℕ) = 1) :
    closedSetFixingSubgroup A hcontinuous K
      (kummerRadicalAddSubgroup A wp K L : Set A.V) = L

Module documentation

finite abelian Kummer theory, the finite abelian Kummer decomposition: the exact Delta

Declarations

ambientFixedAddSubgroup

mem_ambientFixedAddSubgroup_iff

kummerDeltaAddSubgroup

kummerRadicalAddSubgroup

mem_kummerRadicalAddSubgroup_iff

kummerRadical_fixed_of_ker_le_zmultiples

finiteAbelian_kummerRadical_fixingSubgroup_eq