Module

KummerCyclicOperator.lean

Nyll.GaloisCohomology.Kummer.Abstract.KummerCyclicOperator

3 declarations indexed from sourceView source ↗

Module documentation

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

abstract-operator step

This file isolates the finite cyclic step in the proof of the finite abelian Kummer decomposition. It does not claim the full Kummer correspondence. In additive notation, we use a fixed kernel element xi of an equivariant operator wp, of order n. If the cyclic Galois group is killed by n, the vanishing of H⁻¹ produces one element a such that wp a is fixed and a has trivial stabilizer. This is the abstract analogue of the construction a^σ⁻¹ = ζ and hence the single-radical generation step.

Imports2

Imported by2

def

representationStabilizer

L36 ↗

KummerTheory.representationStabilizer

Documentation

Stabilizer for the action carried by a representation. We keep it explicit because a Representation does not install its action as a global MulAction instance on the underlying module.

Source context 4 commands

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

namespace KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory

Lean source · statement

def representationStabilizer {Q : IntegralRepGroupType} [Group Q]
    (B : Rep ℤ Q) (a : B.V) : Subgroup Q

theorem

cyclic_single_radical_of_tateHMinusOne_isZero

L62 ↗

KummerTheory.cyclic_single_radical_of_tateHMinusOne_isZero

Documentation

The cohomological core of the finite cyclic case of the finite abelian Kummer decomposition.

The two conclusions say that wp a belongs to the base fixed module and that the orbit of a has the full size of Q. No radical element or generation assertion is assumed.

Source context 4 commands

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

namespace KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory

Lean source · statement

theorem cyclic_single_radical_of_tateHMinusOne_isZero
    {Q : IntegralRepGroupType} [Group Q] [Fintype Q]
    (B : Rep ℤ Q) (g : Q) (hg : ∀ q, q ∈ Subgroup.zpowers g)
    (hzero : Limits.IsZero (tateCohomology B (-1)))
    (wp : B ⟶ B) (n : ℕ+) (xi : B.V)
    (hxi_order : addOrderOf xi = (n : ℕ))
    (hxi_kernel : wp.hom xi = 0)
    (hxi_fixed : ∀ q : Q, B.ρ q xi = xi)
    (hexponent : ∀ q : Q, q ^ (n : ℕ) = 1) :
    ∃ a : B.V,
      (∀ q : Q, B.ρ q (wp.hom a) = wp.hom a) ∧
      representationStabilizer B a = ⊥

theorem

cyclicOperator_singleRadical_of_normKernelVanishing

L162 ↗

KummerTheory.cyclicOperator_singleRadical_of_normKernelVanishing

Documentation

Finite-cyclic, single-radical frontier of finite abelian Kummer theory, the finite abelian Kummer decomposition, now obtained from SatisfiesCyclicNormKernelVanishing itself.

Here B is the actual coefficient representation A_L attached to the abstract cyclic extension. The operator is stated on B; constructing it functorially from a global operator on A, and assembling cyclic subextensions into the full abelian Kummer extension, are deliberately not claimed in this theorem.

Source context 4 commands

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

namespace KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory

Lean source · statement

theorem cyclicOperator_singleRadical_of_normKernelVanishing
    {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
    (A : Rep ℤ G) (hAxiom : SatisfiesCyclicNormKernelVanishing A)
    (K L : ClosedSubgroup G) (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup K L hLK).Normal]
    [hfinite : Finite (K.toSubgroup ⧸ extensionSubgroup K L hLK)]
    (g : K.toSubgroup ⧸ extensionSubgroup K L hLK)
    (hg : ∀ q, q ∈ Subgroup.zpowers g)
    (wp : extensionFixedRepresentation A K L hLK hnormal ⟶
      extensionFixedRepresentation A K L hLK hnormal)
    (n : ℕ+) (xi : (extensionFixedRepresentation A K L hLK hnormal).V)
    (hxi_order : addOrderOf xi = (n : ℕ))
    (hxi_kernel : wp.hom xi = 0)
    (hxi_fixed : ∀ q : K.toSubgroup ⧸ extensionSubgroup K L hLK,
      (extensionFixedRepresentation A K L hLK hnormal).ρ q xi = xi)
    (hexponent : ∀ q : K.toSubgroup ⧸ extensionSubgroup K L hLK,
      q ^ (n : ℕ) = 1) :
    ∃ a : (extensionFixedRepresentation A K L hLK hnormal).V,
      (∀ q : K.toSubgroup ⧸ extensionSubgroup K L hLK,
        (extensionFixedRepresentation A K L hLK hnormal).ρ q (wp.hom a) = wp.hom a) ∧
      representationStabilizer (extensionFixedRepresentation A K L hLK hnormal) a = ⊥

Module documentation

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

Declarations

representationStabilizer

cyclic_single_radical_of_tateHMinusOne_isZero

cyclicOperator_singleRadical_of_normKernelVanishing