NYLL
Module

QuotientRestriction.lean

Nyll.GaloisCohomology.ProP.QuotientRestriction
8 declarations indexed from sourceView source ↗

Module documentation

Quotient inflation followed by subgroup restriction

Defines the continuous quotient projection and subgroup inclusion and identifies their composite cochain and cohomology maps with the constant-one map.

Imports2
Imported by8

Declarations

def

quotientProjection

L28 ↗
ClassFieldTower.Cohomology.quotientProjection
Documentation

The continuous quotient projection, without any openness assumption on the normal subgroup.

Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u v w
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · full declaration
def quotientProjection (N : Subgroup G) [N.Normal] : G →ₜ* G ⧸ N where
  toMonoidHom := QuotientGroup.mk' N
  continuous_toFun := QuotientGroup.continuous_mk
def

subgroupInclusion

L33 ↗
ClassFieldTower.Cohomology.subgroupInclusion
Documentation

The continuous inclusion of a subgroup.

Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u v w
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · full declaration
def subgroupInclusion (N : Subgroup G) : N →ₜ* G where
  toMonoidHom := N.subtype
  continuous_toFun := continuous_subtype_val
def

trivialContinuousHom

L38 ↗
ClassFieldTower.Cohomology.trivialContinuousHom
Documentation

The constant-one continuous homomorphism.

Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u v w
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · full declaration
def trivialContinuousHom
    (H : Type v) (K : Type w) [Group H] [TopologicalSpace H]
    [Group K] [TopologicalSpace K] : H →ₜ* K where
  toMonoidHom := 1
  continuous_toFun := continuous_const
theorem

quotientProjection_comp_subgroupInclusion

L45 ↗
ClassFieldTower.Cohomology.quotientProjection_comp_subgroupInclusion
Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u v w
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem quotientProjection_comp_subgroupInclusion (N : Subgroup G) [N.Normal] :
    (quotientProjection N).comp (subgroupInclusion N) =
      trivialContinuousHom N (G ⧸ N)
theorem

inflation_comp_restriction_eq_trivialMap

L59 ↗
ClassFieldTower.Cohomology.inflation_comp_restriction_eq_trivialMap
Documentation

At the maintained cohomology API level, inflation followed by restriction is the map induced by the constant-one group homomorphism. Proving that this map is zero in positive degree is the first missing source lemma needed even before constructing transgression.

Source context 8 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u v w
variable {G : Type u} [Group G] [TopologicalSpace G]
section Small
variable {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (p : ℕ)
Lean source · statement
theorem inflation_comp_restriction_eq_trivialMap
    (N : Subgroup G) [N.Normal] (n : ℕ) :
    continuousCohomologyZModPMap p (quotientProjection N) n ≫
        continuousCohomologyZModPMap p (subgroupInclusion N) n =
      continuousCohomologyZModPMap p (trivialContinuousHom N (G ⧸ N)) n
theorem

cochains_inflation_comp_restriction_eq_trivialMap

L70 ↗
ClassFieldTower.Cohomology.cochains_inflation_comp_restriction_eq_trivialMap
Documentation

The corresponding source-level factorization on homogeneous cochains.

Source context 8 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u v w
variable {G : Type u} [Group G] [TopologicalSpace G]
section Small
variable {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (p : ℕ)
Lean source · statement
theorem cochains_inflation_comp_restriction_eq_trivialMap
    (N : Subgroup G) [N.Normal] :
    trivialZModPCochainsMap p (quotientProjection N) ≫
        trivialZModPCochainsMap p (subgroupInclusion N) =
      trivialZModPCochainsMap p (trivialContinuousHom N (G ⧸ N))
theorem

inflation_comp_restriction_eq_trivialMap_lifted

L89 ↗
ClassFieldTower.Cohomology.inflation_comp_restriction_eq_trivialMap_lifted
Documentation

Inflation followed by restriction for universe-lifted trivial coefficients is induced by the constant-one group homomorphism.

Source context 8 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u v w
variable {G : Type u} [Group G] [TopologicalSpace G]
section Lifted
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (p : ℕ)
Lean source · statement
theorem inflation_comp_restriction_eq_trivialMap_lifted
    (N : Subgroup G) [N.Normal] (n : ℕ) :
    continuousCohomologyZModPMapLifted p (quotientProjection N) n ≫
        continuousCohomologyZModPMapLifted p (subgroupInclusion N) n =
      continuousCohomologyZModPMapLifted p (trivialContinuousHom N (G ⧸ N)) n
theorem

cochains_inflation_comp_restriction_eq_trivialMap_lifted

L100 ↗
ClassFieldTower.Cohomology.cochains_inflation_comp_restriction_eq_trivialMap_lifted
Documentation

The lifted source-level factorization on homogeneous cochains.

Source context 8 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u v w
variable {G : Type u} [Group G] [TopologicalSpace G]
section Lifted
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (p : ℕ)
Lean source · statement
theorem cochains_inflation_comp_restriction_eq_trivialMap_lifted
    (N : Subgroup G) [N.Normal] :
    trivialZModPCochainsMapLifted p (quotientProjection N) ≫
        trivialZModPCochainsMapLifted p (subgroupInclusion N) =
      trivialZModPCochainsMapLifted p (trivialContinuousHom N (G ⧸ N))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.