ZMod p coefficientsThis is the coefficient object used by the relation-rank benchmark, together with its canonical restriction maps on homogeneous cochains, cocycles, and continuous cohomology.
The trivial continuous ZMod p-representation of a group.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]def trivialZModP : TopRep (ZMod p) GSurrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]theorem trivialZModP_action (g : G) (x : ZMod p) :
(trivialZModP p G).ρ g x = xThe canonical coefficient morphism used to restrict trivial coefficients along a continuous group homomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Restriction
variable {G : Type} [Group G] [TopologicalSpace G]
variable {H : Type} [Group H] [TopologicalSpace H]def trivialZModPRestrictionHom (f : H →ₜ* G) :
TopRep.res f (trivialZModP p G) ⟶ trivialZModP p HSurrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Restriction
variable {G : Type} [Group G] [TopologicalSpace G]
variable {H : Type} [Group H] [TopologicalSpace H]theorem trivialZModPRestrictionHom_id :
trivialZModPRestrictionHom p (ContinuousMonoidHom.id G) = 𝟙 (trivialZModP p G)Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Restriction
variable {G : Type} [Group G] [TopologicalSpace G]
variable {H : Type} [Group H] [TopologicalSpace H]theorem trivialZModPRestrictionHom_comp
{K : Type} [Group K] [TopologicalSpace K]
(f : H →ₜ* G) (g : K →ₜ* H) :
(TopRep.resFunctor (g : K →* H)).map (trivialZModPRestrictionHom p f) ≫
trivialZModPRestrictionHom p g =
trivialZModPRestrictionHom p (f.comp g)Homogeneous continuous cochains with trivial ZMod p coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Cohomology
variable (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]abbrev trivialZModPCochainsContinuous cocycles with trivial ZMod p coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Cohomology
variable (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]abbrev trivialZModPCocycles (n : ℕ)Continuous cohomology with trivial ZMod p coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Cohomology
variable (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]abbrev continuousCohomologyZModP (n : ℕ)Restriction of homogeneous cochains with trivial ZMod p coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Cohomology
variable (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G}
variable {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]def trivialZModPCochainsMap (f : H →ₜ* G) :
trivialZModPCochains p G ⟶ trivialZModPCochains p HRestriction of continuous cocycles with trivial ZMod p coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Cohomology
variable (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G}
variable {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]abbrev trivialZModPCocyclesMap (f : H →ₜ* G) (n : ℕ) :
trivialZModPCocycles p G n ⟶ trivialZModPCocycles p H nRestriction on continuous cohomology with trivial ZMod p coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Cohomology
variable (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G}
variable {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]abbrev continuousCohomologyZModPMap (f : H →ₜ* G) (n : ℕ) :
continuousCohomologyZModP p G n ⟶ continuousCohomologyZModP p H nSurrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Cohomology
variable (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G}
variable {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]theorem trivialZModPCochainsMap_id :
trivialZModPCochainsMap p (ContinuousMonoidHom.id G) =
𝟙 (trivialZModPCochains p G)Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Cohomology
variable (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G}
variable {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]theorem trivialZModPCochainsMap_comp
{K : Type} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(f : H →ₜ* G) (g : K →ₜ* H) :
trivialZModPCochainsMap p (f.comp g) =
trivialZModPCochainsMap p f ≫ trivialZModPCochainsMap p gSurrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Cohomology
variable (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G}
variable {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]theorem continuousCohomologyZModPMap_id (n : ℕ) :
continuousCohomologyZModPMap p (ContinuousMonoidHom.id G) n =
𝟙 (continuousCohomologyZModP p G n)Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Cohomology
variable (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G}
variable {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]theorem continuousCohomologyZModPMap_comp
{K : Type} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(f : H →ₜ* G) (g : K →ₜ* H) (n : ℕ) :
continuousCohomologyZModPMap p (f.comp g) n =
continuousCohomologyZModPMap p f n ≫ continuousCohomologyZModPMap p g nThe cocycle quotient map commutes with restriction.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Cohomology
variable (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G}
variable {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]theorem trivialZModP_π_naturality (f : H →ₜ* G) (n : ℕ) :
ContinuousCohomology.π (trivialZModP p G) n ≫ continuousCohomologyZModPMap p f n =
trivialZModPCocyclesMap p f n ≫ ContinuousCohomology.π (trivialZModP p H) nThe trivial ZMod p-representation with its carrier lifted to the universe of G.
Mathlib's homogeneous continuous-cochain resolution places its representation carrier in at least the universe of the acting group. This lift therefore supplies the universe-polymorphic cohomology coefficient object; trivialZModP retains its original small-universe API.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]def trivialZModPLifted : TopRep.{u} (ZMod p) GSurrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]theorem trivialZModPLifted_action (g : G) (x : ULift.{u} (ZMod p)) :
(trivialZModPLifted p G).ρ g x = xRestriction of the universe-lifted trivial coefficient representation.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]
variable {G H : Type u} [Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]def trivialZModPRestrictionHomLifted (f : H →ₜ* G) :
TopRep.res f (trivialZModPLifted p G) ⟶ trivialZModPLifted p HSurrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]
variable {G H : Type u} [Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]theorem trivialZModPRestrictionHomLifted_id :
trivialZModPRestrictionHomLifted p (ContinuousMonoidHom.id G) =
𝟙 (trivialZModPLifted p G)Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]
variable {G H : Type u} [Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]theorem trivialZModPRestrictionHomLifted_comp
{K : Type u} [Group K] [TopologicalSpace K]
(f : H →ₜ* G) (g : K →ₜ* H) :
(TopRep.resFunctor (g : K →* H)).map (trivialZModPRestrictionHomLifted p f) ≫
trivialZModPRestrictionHomLifted p g =
trivialZModPRestrictionHomLifted p (f.comp g)Homogeneous continuous cochains with universe-lifted trivial ZMod p coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]
variable {G H : Type u} [Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]
section LiftedCohomology
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]abbrev trivialZModPCochainsLiftedContinuous cocycles with universe-lifted trivial ZMod p coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]
variable {G H : Type u} [Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]
section LiftedCohomology
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]abbrev trivialZModPCocyclesLifted (n : ℕ)Continuous cohomology with universe-lifted trivial ZMod p coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]
variable {G H : Type u} [Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]
section LiftedCohomology
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]abbrev continuousCohomologyZModPLifted (n : ℕ)Restriction of lifted homogeneous cochains with trivial ZMod p coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]
variable {G H : Type u} [Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]
section LiftedCohomology
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]def trivialZModPCochainsMapLifted (f : H →ₜ* G) :
trivialZModPCochainsLifted p G ⟶ trivialZModPCochainsLifted p HRestriction of lifted continuous cocycles with trivial ZMod p coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]
variable {G H : Type u} [Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]
section LiftedCohomology
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]abbrev trivialZModPCocyclesMapLifted (f : H →ₜ* G) (n : ℕ) :
trivialZModPCocyclesLifted p G n ⟶ trivialZModPCocyclesLifted p H nRestriction on lifted continuous cohomology with trivial ZMod p coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]
variable {G H : Type u} [Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]
section LiftedCohomology
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]abbrev continuousCohomologyZModPMapLifted (f : H →ₜ* G) (n : ℕ) :
continuousCohomologyZModPLifted p G n ⟶ continuousCohomologyZModPLifted p H nSurrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]
variable {G H : Type u} [Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]
section LiftedCohomology
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]theorem trivialZModPCochainsMapLifted_id :
trivialZModPCochainsMapLifted p (ContinuousMonoidHom.id G) =
𝟙 (trivialZModPCochainsLifted p G)Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]
variable {G H : Type u} [Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]
section LiftedCohomology
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]theorem trivialZModPCochainsMapLifted_comp
{K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(f : H →ₜ* G) (g : K →ₜ* H) :
trivialZModPCochainsMapLifted p (f.comp g) =
trivialZModPCochainsMapLifted p f ≫ trivialZModPCochainsMapLifted p gSurrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]
variable {G H : Type u} [Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]
section LiftedCohomology
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]theorem continuousCohomologyZModPMapLifted_id (n : ℕ) :
continuousCohomologyZModPMapLifted p (ContinuousMonoidHom.id G) n =
𝟙 (continuousCohomologyZModPLifted p G n)Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]
variable {G H : Type u} [Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]
section LiftedCohomology
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]theorem continuousCohomologyZModPMapLifted_comp
{K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
(f : H →ₜ* G) (g : K →ₜ* H) (n : ℕ) :
continuousCohomologyZModPMapLifted p (f.comp g) n =
continuousCohomologyZModPMapLifted p f n ≫
continuousCohomologyZModPMapLifted p g nThe lifted cocycle quotient map commutes with restriction.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
universe u
variable (p : ℕ) (G : Type) [Group G]
section Lifted
variable (p : ℕ) (G : Type u) [Group G]
variable {G H : Type u} [Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]
section LiftedCohomology
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]theorem trivialZModPLifted_π_naturality (f : H →ₜ* G) (n : ℕ) :
ContinuousCohomology.π (trivialZModPLifted p G) n ≫
continuousCohomologyZModPMapLifted p f n =
trivialZModPCocyclesMapLifted p f n ≫
ContinuousCohomology.π (trivialZModPLifted p H) n