NYLL
Module

ContinuousTransgression.lean

Nyll.GaloisCohomology.ProP.ContinuousTransgression
16 declarations indexed from sourceView source ↗

Module documentation

Continuous transgression from an open normal subgroup

The algebraic factor-set construction in FiniteTransgression uses a bottom topology on its finite quotient. Here the same construction is made directly for the canonical quotient topology of an open normal subgroup, so that it composes with the maintained inflation map.

Imports6
Imported by3

Declarations

instance

continuousTransgressionZModAddCommGroup

L38 ↗
ClassFieldTower.Cohomology.continuousTransgressionZModAddCommGroup
Source context 10 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
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
instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p)
instance

continuousTransgressionH1Module

L41 ↗
ClassFieldTower.Cohomology.continuousTransgressionH1Module
Source context 11 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
Lean source · statement
instance continuousTransgressionH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H))
def

InvariantContinuousH1

L47 ↗
ClassFieldTower.Cohomology.InvariantContinuousH1
Documentation

Continuous mod-p characters of an open normal subgroup fixed by ambient conjugation.

Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousTransgressionH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · full declaration
def InvariantContinuousH1
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    Submodule (ZMod p)
      (ContinuousH1ZMod (p := p) (G := (U.1 : Subgroup G))) where
  carrier := {chi | ∀ (g : G) (n : U.1),
    chi (Additive.ofMul (MulAut.conjNormal g n)) = chi (Additive.ofMul n)}
  zero_mem' := by
    intro g n
    rfl
  add_mem' := by
    intro chi psi hchi hpsi g n
    change chi _ + psi _ = chi _ + psi _
    rw [hchi g n, hpsi g n]
  smul_mem' := by
    intro a chi hchi g n
    let evConj : ContinuousH1ZMod (p := p) (G := (U.1 : Subgroup G)) →+ ZMod p :=
      { toFun := fun eta ↦ eta (Additive.ofMul (MulAut.conjNormal g n))
        map_zero' := rfl
        map_add' := fun _ _ ↦ rfl }
    let ev : ContinuousH1ZMod (p := p) (G := (U.1 : Subgroup G)) →+ ZMod p :=
      { toFun := fun eta ↦ eta (Additive.ofMul n)
        map_zero' := rfl
        map_add' := fun _ _ ↦ rfl }
    exact (ZMod.map_smul evConj a chi).trans
      ((congrArg (fun z : ZMod p ↦ a • z) (hchi g n)).trans
        (ZMod.map_smul ev a chi).symm)
def

invariantContinuousH1ToFiniteCharacterAddHom

L75 ↗
ClassFieldTower.Cohomology.invariantContinuousH1ToFiniteCharacterAddHom
Documentation

Forget continuity while retaining ambient conjugation invariance.

Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousTransgressionH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · full declaration
def invariantContinuousH1ToFiniteCharacterAddHom
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    InvariantContinuousH1 U →+
      InvariantFiniteCharacter (p := p) (U.1 : Subgroup G) where
  toFun chi := ⟨Additive.ofMul (characterOfH1 chi.1).toMonoidHom, by
    intro g n
    exact congrArg Multiplicative.ofAdd (chi.2 g n)⟩
  map_zero' := by apply Subtype.ext; rfl
  map_add' := by intros; apply Subtype.ext; rfl
def

continuousTransgressionHomogeneousCochain

L86 ↗
ClassFieldTower.Cohomology.continuousTransgressionHomogeneousCochain
Documentation

The canonical-topology homogeneous factor-set cochain.

Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousTransgressionH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def continuousTransgressionHomogeneousCochain
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : InvariantContinuousH1 U) :
    (trivialZModPCochainsLifted p (G ⧸ (U.1 : Subgroup G))).X 2
theorem

continuousTransgressionHomogeneousCochain_mem_cycles

L112 ↗
ClassFieldTower.Cohomology.continuousTransgressionHomogeneousCochain_mem_cycles
Source context 13 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousTransgressionH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem continuousTransgressionHomogeneousCochain_mem_cycles
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : InvariantContinuousH1 U) :
    ((trivialZModPCochainsLifted p (G ⧸ (U.1 : Subgroup G))).d 2 3).hom
      (continuousTransgressionHomogeneousCochain U chi) = 0
def

continuousTransgressionHomogeneousCocycle

L148 ↗
ClassFieldTower.Cohomology.continuousTransgressionHomogeneousCocycle
Documentation

The canonical-topology factor-set cocycle.

Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousTransgressionH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def continuousTransgressionHomogeneousCocycle
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : InvariantContinuousH1 U) :
    trivialZModPCocyclesLifted p (G ⧸ (U.1 : Subgroup G)) 2
theorem

iCycles_continuousTransgressionHomogeneousCocycle

L159 ↗
ClassFieldTower.Cohomology.iCycles_continuousTransgressionHomogeneousCocycle
Source context 13 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousTransgressionH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem iCycles_continuousTransgressionHomogeneousCocycle
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : InvariantContinuousH1 U) :
    (trivialZModPCochainsLifted p (G ⧸ (U.1 : Subgroup G))).iCycles 2
      (continuousTransgressionHomogeneousCocycle U chi) =
        continuousTransgressionHomogeneousCochain U chi
def

continuousTransgressionClass

L168 ↗
ClassFieldTower.Cohomology.continuousTransgressionClass
Documentation

Continuous transgression as a degree-two cohomology class.

Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousTransgressionH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def continuousTransgressionClass
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : InvariantContinuousH1 U) :
    continuousCohomologyZModPLifted p (G ⧸ (U.1 : Subgroup G)) 2
theorem

continuousTransgressionHomogeneousCochain_zero

L178 ↗
ClassFieldTower.Cohomology.continuousTransgressionHomogeneousCochain_zero
Source context 13 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousTransgressionH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem continuousTransgressionHomogeneousCochain_zero
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    continuousTransgressionHomogeneousCochain U 0 = 0
theorem

continuousTransgressionHomogeneousCochain_add

L190 ↗
ClassFieldTower.Cohomology.continuousTransgressionHomogeneousCochain_add
Source context 13 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousTransgressionH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem continuousTransgressionHomogeneousCochain_add
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi psi : InvariantContinuousH1 U) :
    continuousTransgressionHomogeneousCochain U (chi + psi) =
      continuousTransgressionHomogeneousCochain U chi +
        continuousTransgressionHomogeneousCochain U psi
theorem

continuousTransgressionHomogeneousCocycle_zero

L208 ↗
ClassFieldTower.Cohomology.continuousTransgressionHomogeneousCocycle_zero
Source context 13 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousTransgressionH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem continuousTransgressionHomogeneousCocycle_zero
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    continuousTransgressionHomogeneousCocycle U 0 = 0
theorem

continuousTransgressionHomogeneousCocycle_add

L218 ↗
ClassFieldTower.Cohomology.continuousTransgressionHomogeneousCocycle_add
Source context 13 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousTransgressionH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem continuousTransgressionHomogeneousCocycle_add
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi psi : InvariantContinuousH1 U) :
    continuousTransgressionHomogeneousCocycle U (chi + psi) =
      continuousTransgressionHomogeneousCocycle U chi +
        continuousTransgressionHomogeneousCocycle U psi
def

continuousTransgressionAddHom

L232 ↗
ClassFieldTower.Cohomology.continuousTransgressionAddHom
Documentation

Continuous transgression is additive.

Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousTransgressionH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · full declaration
def continuousTransgressionAddHom
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    InvariantContinuousH1 U →+
      continuousCohomologyZModPLifted p (G ⧸ (U.1 : Subgroup G)) 2 where
  toFun := continuousTransgressionClass U
  map_zero' := by
    unfold continuousTransgressionClass
    rw [continuousTransgressionHomogeneousCocycle_zero, map_zero]
  map_add' := by
    intro chi psi
    unfold continuousTransgressionClass
    rw [continuousTransgressionHomogeneousCocycle_add, map_add]
def

continuousTransgressionLinearMap

L246 ↗
ClassFieldTower.Cohomology.continuousTransgressionLinearMap
Documentation

Continuous transgression as a ZMod p-linear map.

Source context 12 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousTransgressionH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def continuousTransgressionLinearMap
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    InvariantContinuousH1 U →ₗ[ZMod p]
      continuousCohomologyZModPLifted p (G ⧸ (U.1 : Subgroup G)) 2
theorem

continuousTransgressionLinearMap_apply

L254 ↗
ClassFieldTower.Cohomology.continuousTransgressionLinearMap_apply
Source context 13 commands

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

open CategoryTheory TopRep ContRepresentation
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC
open ClassFieldTower.ProP
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
local instance continuousTransgressionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance continuousTransgressionH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem continuousTransgressionLinearMap_apply
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (chi : InvariantContinuousH1 U) :
    continuousTransgressionLinearMap U chi = continuousTransgressionClass U chi

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