NYLL
Module

SmallLiftedComparison.lean

Nyll.GaloisCohomology.ProP.SmallLiftedComparison
9 declarations indexed from sourceView source ↗

Module documentation

Comparison of small and lifted trivial coefficients

For a group in the base universe, the universe-lifted trivial ZMod p coefficient and the benchmark's small coefficient are isomorphic. Functoriality of homogeneous cochains transports this coefficient isomorphism to every continuous-cohomology degree.

Imports2
Imported by2

Declarations

instance

continuousSMulULiftZModSmall

L28 ↗
ClassFieldTower.Cohomology.continuousSMulULiftZModSmall
Source context 5 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (p : ℕ) (G : Type)
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
instance continuousSMulULiftZModSmall :
    ContinuousSMul (ZMod p) (ULift.{0} (ZMod p))
def

trivialZModPLiftedToSmall

L33 ↗
ClassFieldTower.Cohomology.trivialZModPLiftedToSmall
Documentation

Forget the universe lift on the trivial coefficient representation.

Source context 6 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (p : ℕ) (G : Type)
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZModSmall :
    ContinuousSMul (ZMod p) (ULift.{0} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
Lean source · statement
def trivialZModPLiftedToSmall :
    trivialZModPLifted p G ⟶ trivialZModP p G
def

trivialZModPSmallToLifted

L47 ↗
ClassFieldTower.Cohomology.trivialZModPSmallToLifted
Documentation

Lift the benchmark's small trivial coefficient representation.

Source context 6 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (p : ℕ) (G : Type)
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZModSmall :
    ContinuousSMul (ZMod p) (ULift.{0} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
Lean source · statement
def trivialZModPSmallToLifted :
    trivialZModP p G ⟶ trivialZModPLifted p G
def

trivialZModPLiftedSmallIso

L59 ↗
ClassFieldTower.Cohomology.trivialZModPLiftedSmallIso
Documentation

The small and lifted trivial coefficient representations are isomorphic.

Source context 6 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (p : ℕ) (G : Type)
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZModSmall :
    ContinuousSMul (ZMod p) (ULift.{0} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
Lean source · full declaration
def trivialZModPLiftedSmallIso :
    trivialZModPLifted p G ≅ trivialZModP p G where
  hom := trivialZModPLiftedToSmall p G
  inv := trivialZModPSmallToLifted p G
  hom_inv_id := rfl
  inv_hom_id := rfl
def

trivialZModPCochainsLiftedSmallIso

L67 ↗
ClassFieldTower.Cohomology.trivialZModPCochainsLiftedSmallIso
Documentation

The induced isomorphism between the homogeneous cochain complexes.

Source context 6 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (p : ℕ) (G : Type)
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZModSmall :
    ContinuousSMul (ZMod p) (ULift.{0} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
Lean source · full declaration
def trivialZModPCochainsLiftedSmallIso :
    TopRep.homogeneousCochains (trivialZModPLifted p G) ≅
      TopRep.homogeneousCochains (trivialZModP p G) where
  hom := ContinuousCohomology.cochainsMap (ContinuousMonoidHom.id G)
    (trivialZModPLiftedSmallIso p G).hom
  inv := ContinuousCohomology.cochainsMap (ContinuousMonoidHom.id G)
    (trivialZModPLiftedSmallIso p G).inv
  hom_inv_id := by
    exact (ContinuousCohomology.cochainsMap_comp
      (X := trivialZModPLifted p G) (Y := trivialZModP p G)
      (Z := trivialZModPLifted p G)
      (ContinuousMonoidHom.id G) (ContinuousMonoidHom.id G)
      (trivialZModPLiftedSmallIso p G).hom
      (trivialZModPLiftedSmallIso p G).inv).symm.trans
      (ContinuousCohomology.cochainsMap_id _)
  inv_hom_id := by
    exact (ContinuousCohomology.cochainsMap_comp
      (X := trivialZModP p G) (Y := trivialZModPLifted p G)
      (Z := trivialZModP p G)
      (ContinuousMonoidHom.id G) (ContinuousMonoidHom.id G)
      (trivialZModPLiftedSmallIso p G).inv
      (trivialZModPLiftedSmallIso p G).hom).symm.trans
      (ContinuousCohomology.cochainsMap_id _)
def

continuousCohomologyZModPLiftedSmallIso

L92 ↗
ClassFieldTower.Cohomology.continuousCohomologyZModPLiftedSmallIso
Documentation

The categorical continuous-cohomology comparison in every degree.

Source context 6 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (p : ℕ) (G : Type)
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZModSmall :
    ContinuousSMul (ZMod p) (ULift.{0} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
Lean source · statement
def continuousCohomologyZModPLiftedSmallIso (n : ℕ) :
    continuousCohomologyZModPLifted p G n ≅
      continuousCohomologyZModP p G n
def

continuousCohomologyZModPLiftedSmallLinearEquiv

L99 ↗
ClassFieldTower.Cohomology.continuousCohomologyZModPLiftedSmallLinearEquiv
Documentation

The ZMod p-linear continuous-cohomology comparison in every degree.

Source context 6 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (p : ℕ) (G : Type)
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZModSmall :
    ContinuousSMul (ZMod p) (ULift.{0} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
Lean source · statement
def continuousCohomologyZModPLiftedSmallLinearEquiv (n : ℕ) :
    continuousCohomologyZModPLifted p G n ≃ₗ[ZMod p]
      continuousCohomologyZModP p G n
theorem

continuousCohomologyZModPLiftedSmall_finrank_eq

L105 ↗
ClassFieldTower.Cohomology.continuousCohomologyZModPLiftedSmall_finrank_eq
Documentation

Small and lifted trivial coefficients give the same cohomological dimension.

Source context 6 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (p : ℕ) (G : Type)
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZModSmall :
    ContinuousSMul (ZMod p) (ULift.{0} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
Lean source · statement
theorem continuousCohomologyZModPLiftedSmall_finrank_eq (n : ℕ) :
    Module.finrank (ZMod p) (continuousCohomologyZModPLifted p G n) =
      Module.finrank (ZMod p) (continuousCohomologyZModP p G n)
theorem

continuousCohomologyZModP_finiteDimensional_iff_lifted

L111 ↗
ClassFieldTower.Cohomology.continuousCohomologyZModP_finiteDimensional_iff_lifted
Documentation

Finite dimensionality can be checked using either coefficient model.

Source context 6 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
noncomputable section
variable (p : ℕ) (G : Type)
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance continuousSMulULiftZModSmall :
    ContinuousSMul (ZMod p) (ULift.{0} (ZMod p)) :=
  ContinuousSMul.induced ULift.moduleEquiv.toLinearMap
Lean source · statement
theorem continuousCohomologyZModP_finiteDimensional_iff_lifted
    [Fact p.Prime] (n : ℕ) :
    FiniteDimensional (ZMod p) (continuousCohomologyZModP p G n) ↔
      FiniteDimensional (ZMod p) (continuousCohomologyZModPLifted p G n)

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