NYLL
Module

TrivialMapH1.lean

Nyll.GaloisCohomology.ProP.TrivialMapH1
6 declarations indexed from sourceView source ↗

Module documentation

Trivial restriction maps in degree-one continuous cohomology

Pullback along the constant-one homomorphism vanishes on cocycles and continuous cohomology with trivial ZMod p coefficients. Consequently, inflation followed by restriction to the kernel vanishes in degree one. The same statements are proved for universe-lifted coefficients.

Imports1
Imported by1

Declarations

theorem

trivialZModPCocyclesMap_trivial_one_eq_zero

L32 ↗
ClassFieldTower.Cohomology.trivialZModPCocyclesMap_trivial_one_eq_zero
Documentation

Pullback along the constant-one group homomorphism is zero on continuous cocycles in degree one with trivial ZMod p coefficients.

Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ)
variable {G H : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem trivialZModPCocyclesMap_trivial_one_eq_zero :
    trivialZModPCocyclesMap p (trivialContinuousHom H G) 1 = 0
theorem

continuousCohomologyZModPMap_trivial_one_eq_zero

L61 ↗
ClassFieldTower.Cohomology.continuousCohomologyZModPMap_trivial_one_eq_zero
Documentation

Pullback along the constant-one group homomorphism is zero on continuous H¹ with trivial ZMod p coefficients.

Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ)
variable {G H : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem continuousCohomologyZModPMap_trivial_one_eq_zero :
    continuousCohomologyZModPMap p (trivialContinuousHom H G) 1 = 0
theorem

inflation_comp_restriction_degree_one_eq_zero

L70 ↗
ClassFieldTower.Cohomology.inflation_comp_restriction_degree_one_eq_zero
Documentation

Inflation followed by restriction is zero on continuous H¹ with trivial ZMod p coefficients.

Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ)
variable {G H : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem inflation_comp_restriction_degree_one_eq_zero
    (N : Subgroup G) [N.Normal] :
    continuousCohomologyZModPMap p (quotientProjection N) 1 ≫
        continuousCohomologyZModPMap p (subgroupInclusion N) 1 = 0
theorem

trivialZModPCocyclesMapLifted_trivial_one_eq_zero

L84 ↗
ClassFieldTower.Cohomology.trivialZModPCocyclesMapLifted_trivial_one_eq_zero
Documentation

Pullback along the constant-one homomorphism is zero on degree-one cocycles with universe-lifted trivial ZMod p coefficients.

Source context 8 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ)
variable {G H : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lifted
variable {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem trivialZModPCocyclesMapLifted_trivial_one_eq_zero :
    trivialZModPCocyclesMapLifted p (trivialContinuousHom H G) 1 = 0
theorem

continuousCohomologyZModPMapLifted_trivial_one_eq_zero

L112 ↗
ClassFieldTower.Cohomology.continuousCohomologyZModPMapLifted_trivial_one_eq_zero
Documentation

Pullback along the constant-one homomorphism is zero on lifted continuous H¹.

Source context 8 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ)
variable {G H : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lifted
variable {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem continuousCohomologyZModPMapLifted_trivial_one_eq_zero :
    continuousCohomologyZModPMapLifted p (trivialContinuousHom H G) 1 = 0
theorem

inflation_comp_restriction_degree_one_eq_zero_lifted

L121 ↗
ClassFieldTower.Cohomology.inflation_comp_restriction_degree_one_eq_zero_lifted
Documentation

Inflation followed by restriction is zero on lifted continuous H¹ with trivial ZMod p coefficients.

Source context 8 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ)
variable {G H : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
section Lifted
variable {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem inflation_comp_restriction_degree_one_eq_zero_lifted
    (N : Subgroup G) [N.Normal] :
    continuousCohomologyZModPMapLifted p (quotientProjection N) 1 ≫
        continuousCohomologyZModPMapLifted p (subgroupInclusion N) 1 = 0

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