Module

KummerGlobalOperator.lean

Nyll.GaloisCohomology.Kummer.Abstract.KummerGlobalOperator

8 declarations indexed from sourceView source ↗

Module documentation

finite abelian Kummer theory, the finite abelian Kummer decomposition: descending the global

operator

This file constructs, rather than assumes, the endomorphism of A_L induced by a global equivariant endomorphism wp : A ⟶ A. It also embeds a G_K-fixed global kernel element into the invariant subtype defining A_L and supplies these constructions to the finite cyclic single-radical theorem.

The result remains only the finite cyclic step of the finite abelian Kummer decomposition, not the full abelian Kummer correspondence.

Imports1

Nyll.GaloisCohomology.Kummer.Abstract.KummerCyclicOperator

Imported by2

def

extensionFixedEndomorphism

L35 ↗

KummerTheory.extensionFixedEndomorphism

Documentation

The endomorphism of A_L induced functorially by a global equivariant endomorphism wp : A ⟶ A: first restrict to G_K, then pass to the G_L-invariants and the quotient action.

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 extensionFixedEndomorphism
    {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup K L hLK).Normal]
    (wp : A ⟶ A) :
    extensionFixedRepresentation A K L hLK hnormal ⟶
      extensionFixedRepresentation A K L hLK hnormal

def

extensionFixedKernelElement

L48 ↗

KummerTheory.extensionFixedKernelElement

Documentation

A global element fixed by G_K, viewed in the invariant subtype which is the carrier of A_L.

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 extensionFixedKernelElement
    {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup K L hLK).Normal]
    (xi : A.V) (hxi_fixed : ∀ k : K.toSubgroup, A.ρ k.1 xi = xi) :
    (extensionFixedRepresentation A K L hLK hnormal).V

theorem

extensionFixedKernelElement_val

L62 ↗

KummerTheory.extensionFixedKernelElement_val

Documentation

The underlying value of the fixed kernel element is the selected global kernel element.

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 extensionFixedKernelElement_val
    {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup K L hLK).Normal]
    (xi : A.V) (hxi_fixed : ∀ k : K.toSubgroup, A.ρ k.1 xi = xi) :
    (extensionFixedKernelElement A K L hLK xi hxi_fixed).1 = xi

theorem

extensionFixedEndomorphism_apply_val

L72 ↗

KummerTheory.extensionFixedEndomorphism_apply_val

Documentation

The extension-fixed endomorphism acts on underlying values by the global operator.

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 extensionFixedEndomorphism_apply_val
    {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup K L hLK).Normal]
    (wp : A ⟶ A) (x : (extensionFixedRepresentation A K L hLK hnormal).V) :
    ((extensionFixedEndomorphism A K L hLK wp).hom x).1 = wp.hom x.1

theorem

extensionFixedKernelElement_addOrderOf

L82 ↗

KummerTheory.extensionFixedKernelElement_addOrderOf

Documentation

The additive order of the fixed kernel element is inherited from its ambient value.

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 extensionFixedKernelElement_addOrderOf
    {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup K L hLK).Normal]
    (xi : A.V) (hxi_fixed : ∀ k : K.toSubgroup, A.ρ k.1 xi = xi) :
    addOrderOf (extensionFixedKernelElement A K L hLK xi hxi_fixed) = addOrderOf xi

theorem

extensionFixedKernelElement_in_kernel

L101 ↗

KummerTheory.extensionFixedKernelElement_in_kernel

Documentation

The selected fixed element lies in the kernel of the extension-fixed endomorphism.

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 extensionFixedKernelElement_in_kernel
    {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup K L hLK).Normal]
    (wp : A ⟶ A) (xi : A.V)
    (hxi_fixed : ∀ k : K.toSubgroup, A.ρ k.1 xi = xi)
    (hxi_kernel : wp.hom xi = 0) :
    (extensionFixedEndomorphism A K L hLK wp).hom
      (extensionFixedKernelElement A K L hLK xi hxi_fixed) = 0

theorem

extensionFixedKernelElement_fixed

L116 ↗

KummerTheory.extensionFixedKernelElement_fixed

Documentation

Every element of the extension subgroup fixes the selected kernel element.

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 extensionFixedKernelElement_fixed
    {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
    (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    [hnormal : (extensionSubgroup K L hLK).Normal]
    (xi : A.V) (hxi_fixed : ∀ k : K.toSubgroup, A.ρ k.1 xi = xi)
    (q : K.toSubgroup ⧸ extensionSubgroup K L hLK) :
    (extensionFixedRepresentation A K L hLK hnormal).ρ q
        (extensionFixedKernelElement A K L hLK xi hxi_fixed) =
      extensionFixedKernelElement A K L hLK xi hxi_fixed

theorem

cyclicGlobalOperator_singleRadical

L134 ↗

KummerTheory.cyclicGlobalOperator_singleRadical

Documentation

The finite cyclic single-radical step with a genuinely global operator. The endomorphism on A_L and its distinguished kernel element are both constructed in the proof, not supplied as hypotheses.

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 cyclicGlobalOperator_singleRadical
    {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 : 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 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
            ((extensionFixedEndomorphism A K L hLK wp).hom a) =
          (extensionFixedEndomorphism A K L hLK wp).hom a) ∧
      representationStabilizer (extensionFixedRepresentation A K L hLK hnormal) a = ⊥

Module documentation

finite abelian Kummer theory, the finite abelian Kummer decomposition: descending the global

Declarations