Module

InvariantCharacterFiniteStage.lean

Nyll.ProCGroups.Cohomology.InvariantCharacterFiniteStage

5 declarations indexed from sourceView source ↗

Module documentation

Finite-stage descent of invariant characters

Every ambient-conjugation-invariant continuous mod-p character on a closed normal subgroup of a pro-p group descends to the subgroup's image in one finite p-group quotient. This isolates the finite-stage input needed to construct transgression without assuming that the closed subgroup is open.

Imports3

Nyll.ProCGroups.Cohomology.FiniteInvariantCharacter
Mathlib.Topology.Instances.ZMod
Nyll.ProCGroups.ProC.Quotients.ClosedSubgroupNeighborhoods

Imported by4

def

finiteStageImage

L35 ↗

ClassFieldTower.ProP.finiteStageImage

Documentation

The image of a closed subgroup in an ambient finite quotient.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]

Lean source · statement

def finiteStageImage (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    Subgroup (F ⧸ (U.1 : Subgroup F))

instance

finiteStageImage_normal

L40 ↗

ClassFieldTower.ProP.finiteStageImage_normal

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]

Lean source · statement

instance finiteStageImage_normal (R : ClosedSubgroup F) [R.Normal]
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    (finiteStageImage R U).Normal

def

finiteStageImageMap

L46 ↗

ClassFieldTower.ProP.finiteStageImageMap

Documentation

The canonical surjection from a closed subgroup to its image at a finite stage.

Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]

Lean source · full declaration

def finiteStageImageMap (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    MonoidHom R (finiteStageImage R U) where
  toFun r :=
    ⟨OpenNormalSubgroup.quotientProj U.1 r.1, ⟨r.1, r.2, rfl⟩⟩
  map_one' := Subtype.ext (map_one (OpenNormalSubgroup.quotientProj U.1))
  map_mul' a b := Subtype.ext (map_mul (OpenNormalSubgroup.quotientProj U.1) a.1 b.1)

theorem

finiteStageImageMap_surjective

L57 ↗

ClassFieldTower.ProP.finiteStageImageMap_surjective

Documentation

The finite-stage image map is surjective.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
omit [IsTopologicalGroup F] [CompactSpace F] [T2Space F]
  [TotallyDisconnectedSpace F] in

Lean source · statement

theorem finiteStageImageMap_surjective (R : ClosedSubgroup F)
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F) :
    Function.Surjective (finiteStageImageMap R U)

theorem

exists_finiteStage_invariant_character

L68 ↗

ClassFieldTower.ProP.exists_finiteStage_invariant_character

Documentation

An ambient-conjugation-invariant continuous mod-p character of a closed normal subgroup descends to an invariant character on the subgroup's image in one finite p-group quotient.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
omit [IsTopologicalGroup F] [CompactSpace F] [T2Space F]
  [TotallyDisconnectedSpace F] in

Lean source · statement

theorem exists_finiteStage_invariant_character
    (hF : HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) F)
    (R : ClosedSubgroup F) [R.Normal]
    (χ : R →ₜ* Multiplicative (ZMod p)) (hχne : χ ≠ 1)
    (hχinv : ∀ (f : F) (r : R), χ (MulAut.conjNormal f r) = χ r) :
    ∃ U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) F,
      ∃ χbar : MonoidHom (finiteStageImage R U) (Multiplicative (ZMod p)),
        χbar.comp (finiteStageImageMap R U) = χ.toMonoidHom ∧
          χbar ≠ 1 ∧
          ∀ (g : F ⧸ (U.1 : Subgroup F)) (n : finiteStageImage R U),
            χbar (MulAut.conjNormal g n) = χbar n

Module documentation

Finite-stage descent of invariant characters

Declarations

finiteStageImage

finiteStageImage_normal

finiteStageImageMap

finiteStageImageMap_surjective

exists_finiteStage_invariant_character