NYLL
Module

DiscreteH2CochainComparison.lean

Nyll.GaloisCohomology.ProP.DiscreteH2CochainComparison
15 declarations indexed from sourceView source ↗

Module documentation

Homogeneous and inhomogeneous cochains for a discrete group

For a discrete group in the base universe, continuous homogeneous cochains with lifted trivial mod-p coefficients are additively equivalent to the usual inhomogeneous function cochains. This file records the equivalences in degrees one through three.

Imports2
Imported by4

Declarations

theorem

homogeneousOneCochainLifted_leftInvariant

L30 ↗
ClassFieldTower.Cohomology.homogeneousOneCochainLifted_leftInvariant
Source context 7 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
omit [DiscreteTopology Q] in
Lean source · statement
theorem homogeneousOneCochainLifted_leftInvariant
    (c : (trivialZModPCochainsLifted p Q).X 1)
    (a x₀ x₁ : Q) :
    c.1 (a * x₀) (a * x₁) = c.1 x₀ x₁
theorem

homogeneousTwoCochainLifted_leftInvariant

L46 ↗
ClassFieldTower.Cohomology.homogeneousTwoCochainLifted_leftInvariant
Source context 7 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
omit [DiscreteTopology Q] in
Lean source · statement
theorem homogeneousTwoCochainLifted_leftInvariant
    (c : (trivialZModPCochainsLifted p Q).X 2)
    (a x₀ x₁ x₂ : Q) :
    c.1 (a * x₀) (a * x₁) (a * x₂) = c.1 x₀ x₁ x₂
theorem

homogeneousThreeCochainLifted_leftInvariant

L62 ↗
ClassFieldTower.Cohomology.homogeneousThreeCochainLifted_leftInvariant
Source context 7 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
omit [DiscreteTopology Q] in
Lean source · statement
theorem homogeneousThreeCochainLifted_leftInvariant
    (c : (trivialZModPCochainsLifted p Q).X 3)
    (a x₀ x₁ x₂ x₃ : Q) :
    c.1 (a * x₀) (a * x₁) (a * x₂) (a * x₃) =
      c.1 x₀ x₁ x₂ x₃
def

dehomogenizeOne

L82 ↗
ClassFieldTower.Cohomology.dehomogenizeOne
Documentation

Dehomogenize a homogeneous degree-one cochain.

Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
Lean source · statement
def dehomogenizeOne
    (c : (trivialZModPCochainsLifted p Q).X 1) (g : Q) : ULift (ZMod p)
def

homogenizeOne

L87 ↗
ClassFieldTower.Cohomology.homogenizeOne
Documentation

Homogenize an inhomogeneous degree-one cochain.

Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
Lean source · statement
def homogenizeOne (f : Q → ULift (ZMod p)) :
    (trivialZModPCochainsLifted p Q).X 1
theorem

homogenizeOne_apply

L104 ↗
ClassFieldTower.Cohomology.homogenizeOne_apply
Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
Lean source · statement
theorem homogenizeOne_apply (f : Q → ULift (ZMod p)) (g h : Q) :
    (homogenizeOne f).1 g h = f (g⁻¹ * h)
def

homogeneousOneCochainAddEquiv

L110 ↗
ClassFieldTower.Cohomology.homogeneousOneCochainAddEquiv
Documentation

Additive equivalence between homogeneous and inhomogeneous degree-one cochains.

Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
Lean source · full declaration
def homogeneousOneCochainAddEquiv :
    (trivialZModPCochainsLifted p Q).X 1 ≃+ (Q → ULift (ZMod p)) where
  toFun := dehomogenizeOne
  invFun := homogenizeOne
  left_inv := by
    intro c
    apply Subtype.ext
    ext g h
    change c.1 1 (g⁻¹ * h) = c.1 g h
    have hinv := homogeneousOneCochainLifted_leftInvariant c g⁻¹ g h
    simp only [inv_mul_cancel] at hinv
    change c.1 1 (g⁻¹ * h) = c.1 g h at hinv
    exact hinv
  right_inv := by
    intro f
    funext g
    change f (1⁻¹ * g) = f g
    simp
  map_add' := by
    intro c d
    funext g
    rfl
def

dehomogenizeTwo

L134 ↗
ClassFieldTower.Cohomology.dehomogenizeTwo
Documentation

Dehomogenize a homogeneous degree-two cochain.

Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
Lean source · statement
def dehomogenizeTwo
    (c : (trivialZModPCochainsLifted p Q).X 2)
    (gh : Q × Q) : ULift (ZMod p)
def

homogenizeTwo

L140 ↗
ClassFieldTower.Cohomology.homogenizeTwo
Documentation

Homogenize an inhomogeneous degree-two cochain.

Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
Lean source · statement
def homogenizeTwo (f : Q × Q → ULift (ZMod p)) :
    (trivialZModPCochainsLifted p Q).X 2
theorem

homogenizeTwo_apply

L164 ↗
ClassFieldTower.Cohomology.homogenizeTwo_apply
Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
Lean source · statement
theorem homogenizeTwo_apply
    (f : Q × Q → ULift (ZMod p)) (g h k : Q) :
    (homogenizeTwo f).1 g h k = f (g⁻¹ * h, h⁻¹ * k)
def

homogeneousTwoCochainAddEquiv

L171 ↗
ClassFieldTower.Cohomology.homogeneousTwoCochainAddEquiv
Documentation

Additive equivalence between homogeneous and inhomogeneous degree-two cochains.

Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
Lean source · full declaration
def homogeneousTwoCochainAddEquiv :
    (trivialZModPCochainsLifted p Q).X 2 ≃+ (Q × Q → ULift (ZMod p)) where
  toFun := dehomogenizeTwo
  invFun := homogenizeTwo
  left_inv := by
    intro c
    apply Subtype.ext
    ext g h k
    change
      c.1 1 (g⁻¹ * h)
            ((g⁻¹ * h) * (h⁻¹ * k)) =
        c.1 g h k
    rw [show (g⁻¹ * h) * (h⁻¹ * k) = g⁻¹ * k by group]
    have hinv := homogeneousTwoCochainLifted_leftInvariant c g⁻¹ g h k
    simp only [inv_mul_cancel] at hinv
    change c.1 1 (g⁻¹ * h) (g⁻¹ * k) = c.1 g h k at hinv
    exact hinv
  right_inv := by
    intro f
    funext gh
    change
      f (1⁻¹ * gh.1, gh.1⁻¹ * (gh.1 * gh.2)) = f gh
    simp
  map_add' := by
    intro c d
    funext gh
    rfl
def

dehomogenizeThree

L200 ↗
ClassFieldTower.Cohomology.dehomogenizeThree
Documentation

Dehomogenize a homogeneous degree-three cochain.

Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
Lean source · statement
def dehomogenizeThree
    (c : (trivialZModPCochainsLifted p Q).X 3)
    (ghk : Q × Q × Q) : ULift (ZMod p)
def

homogenizeThree

L207 ↗
ClassFieldTower.Cohomology.homogenizeThree
Documentation

Homogenize an inhomogeneous degree-three cochain.

Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
Lean source · statement
def homogenizeThree (f : Q × Q × Q → ULift (ZMod p)) :
    (trivialZModPCochainsLifted p Q).X 3
theorem

homogenizeThree_apply

L240 ↗
ClassFieldTower.Cohomology.homogenizeThree_apply
Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
Lean source · statement
theorem homogenizeThree_apply
    (f : Q × Q × Q → ULift (ZMod p)) (g h k l : Q) :
    (homogenizeThree f).1 g h k l =
      f (g⁻¹ * h, h⁻¹ * k, k⁻¹ * l)
def

homogeneousThreeCochainAddEquiv

L248 ↗
ClassFieldTower.Cohomology.homogeneousThreeCochainAddEquiv
Documentation

Additive equivalence between homogeneous and inhomogeneous degree-three cochains.

Source context 6 commands

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

open CategoryTheory TopRep ContRepresentation
namespace ClassFieldTower.Cohomology
noncomputable section
variable {p : ℕ}
variable {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
variable [DiscreteTopology Q]
Lean source · full declaration
def homogeneousThreeCochainAddEquiv :
    (trivialZModPCochainsLifted p Q).X 3 ≃+
      (Q × Q × Q → ULift (ZMod p)) where
  toFun := dehomogenizeThree
  invFun := homogenizeThree
  left_inv := by
    intro c
    apply Subtype.ext
    ext g h k l
    change
      c.1 1 (g⁻¹ * h)
            ((g⁻¹ * h) * (h⁻¹ * k))
            ((g⁻¹ * h) * (h⁻¹ * k) * (k⁻¹ * l)) =
        c.1 g h k l
    rw [show (g⁻¹ * h) * (h⁻¹ * k) = g⁻¹ * k by group]
    rw [show g⁻¹ * k * (k⁻¹ * l) = g⁻¹ * l by group]
    have hinv := homogeneousThreeCochainLifted_leftInvariant c g⁻¹ g h k l
    simp only [inv_mul_cancel] at hinv
    change
      c.1 1 (g⁻¹ * h) (g⁻¹ * k) (g⁻¹ * l) =
        c.1 g h k l at hinv
    exact hinv
  right_inv := by
    intro f
    funext ghk
    change
      f (1⁻¹ * ghk.1,
          ghk.1⁻¹ * (ghk.1 * ghk.2.1),
          (ghk.1 * ghk.2.1)⁻¹ *
            (ghk.1 * ghk.2.1 * ghk.2.2)) = f ghk
    apply congrArg f
    apply Prod.ext
    · simp
    · apply Prod.ext
      · simp
      · group
  map_add' := by
    intro c d
    funext ghk
    rfl

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