Module

H2FiniteStageFamily.lean

Nyll.GaloisCohomology.ProP.H2FiniteStageFamily

8 declarations indexed from sourceView source ↗

Module documentation

Common finite-stage realization of degree-two classes

Finite families of lifted degree-two classes of a pro-p group inflate from one common finite p-group quotient. In particular, the ranges of finite-stage inflation cover the ambient degree-two cohomology.

Imports3

Nyll.GaloisCohomology.ProP.H2FiniteStage
Mathlib.LinearAlgebra.Dimension.Free
Mathlib.Data.Fintype.EquivFin

Imported by6

theorem

finiteDimensional_zmod_of_finite

L34 ↗

ClassFieldTower.Cohomology.finiteDimensional_zmod_of_finite

Source context 9 commands

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

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

Lean source · statement

theorem finiteDimensional_zmod_of_finite
    {V : Type v} [AddCommGroup V] [Module (ZMod p) V]
    (hV : Finite V) : FiniteDimensional (ZMod p) V

theorem

finite_resolutionX_trivial

L43 ↗

ClassFieldTower.Cohomology.finite_resolutionX_trivial

Source context 9 commands

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

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

Lean source · statement

theorem finite_resolutionX_trivial
    (Q : Type u) [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    (hQ : Finite Q) (n : ℕ) :
    Finite (TopRep.resolutionX (trivialZModPLifted p Q) n)

theorem

finiteDimensional_degree_two_of_finite

L64 ↗

ClassFieldTower.Cohomology.finiteDimensional_degree_two_of_finite

Documentation

Lifted mod-p degree-two continuous cohomology of a finite group is finite-dimensional.

This is proved from finiteness of the homogeneous cochain space, not assumed as a separate finite-stage input.

Source context 9 commands

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

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

Lean source · statement

theorem finiteDimensional_degree_two_of_finite
    {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
    (hQ : Finite Q) :
    FiniteDimensional (ZMod p) (continuousCohomologyZModPLifted p Q 2)

theorem

inflation_transition_eq

L89 ↗

ClassFieldTower.Cohomology.inflation_transition_eq

Documentation

Inflating after transition to a finer quotient agrees with inflation from the original quotient.

Source context 10 commands

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

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

Lean source · statement

theorem inflation_transition_eq
    {U V : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G}
    (hVU : (V.1 : Subgroup G) ≤ (U.1 : Subgroup G))
    (xU : continuousCohomologyZModPLifted p
      (G ⧸ (U.1 : Subgroup G)) 2) :
    continuousCohomologyZModPMapLifted p
        (OpenNormalSubgroupInClass.quotientProj V) 2
        (continuousCohomologyZModPMapLifted p
          (OpenNormalSubgroupInClass.transition hVU) 2 xU) =
      continuousCohomologyZModPMapLifted p
        (OpenNormalSubgroupInClass.quotientProj U) 2 xU

theorem

exists_common_inflation_finset

L110 ↗

ClassFieldTower.Cohomology.exists_common_inflation_finset

Documentation

A finite set of lifted degree-two classes inflates from one common finite p-group quotient.

Source context 9 commands

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

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

Lean source · statement

theorem exists_common_inflation_finset
    {ι : Type v}
    (hG : HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) G)
    (x : ι → continuousCohomologyZModPLifted p G 2)
    (s : Finset ι) :
    ∃ U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G,
      ∀ i, i ∈ s →
        ∃ xU : continuousCohomologyZModPLifted p
            (G ⧸ (U.1 : Subgroup G)) 2,
          continuousCohomologyZModPMapLifted p
            (OpenNormalSubgroupInClass.quotientProj U) 2 xU = x i

theorem

exists_openNormalSubgroupInClass_inflation_eq_degree_two_family

L149 ↗

ClassFieldTower.Cohomology.exists_openNormalSubgroupInClass_inflation_eq_degree_two_family

Documentation

Every finite family of lifted degree-two classes of a pro-p group inflates from one common finite p-group quotient.

Source context 9 commands

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

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

Lean source · statement

theorem exists_openNormalSubgroupInClass_inflation_eq_degree_two_family
    {ι : Type v} [Finite ι]
    (hG : HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) G)
    (x : ι → continuousCohomologyZModPLifted p G 2) :
    ∃ U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G,
      ∃ xU : ι → continuousCohomologyZModPLifted p
          (G ⧸ (U.1 : Subgroup G)) 2,
        ∀ i,
          continuousCohomologyZModPMapLifted p
            (OpenNormalSubgroupInClass.quotientProj U) 2 (xU i) = x i

abbrev

degreeTwoInflationRange

L167 ↗

ClassFieldTower.Cohomology.degreeTwoInflationRange

Documentation

The subspace of ambient degree-two classes inflated from a fixed finite quotient.

Source context 10 commands

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

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

Lean source · statement

abbrev degreeTwoInflationRange
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    Submodule (ZMod p) (continuousCohomologyZModPLifted p G 2)

theorem

iSup_degreeTwoInflationRange_eq_top

L175 ↗

ClassFieldTower.Cohomology.iSup_degreeTwoInflationRange_eq_top

Documentation

Finite-stage inflation ranges cover all lifted degree-two classes.

Source context 9 commands

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

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

Lean source · statement

theorem iSup_degreeTwoInflationRange_eq_top
    (hG : HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) G) :
    (⨆ U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G,
      degreeTwoInflationRange (p := p) U) = ⊤

Module documentation

Common finite-stage realization of degree-two classes

Declarations