NYLL
Module

PresentationH2Primitive.lean

Nyll.GaloisCohomology.ProP.PresentationH2Primitive
19 declarations indexed from sourceView source ↗

Module documentation

Primitive selection for presentation degree-two classes

This file linearly selects homogeneous cocycle representatives and, after restriction to the finite-basis free pro-p source, linearly selects degree-one primitives. It also records the pointwise boundary and normalization identities used by the presentation five-term argument.

Imports3
Imported by4

Declarations

theorem

homologyπ_surjective

L34 ↗
ClassFieldTower.ProP.PresentationH2Aux.homologyπ_surjective
Source context 8 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
Lean source · statement
theorem homologyπ_surjective
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (A : TopRep.{u} (ZMod p) G) (n : ℕ) :
    Function.Surjective (ContinuousCohomology.π A n)
def

homologyRepresentativeSection

L72 ↗
ClassFieldTower.ProP.PresentationH2Aux.homologyRepresentativeSection
Documentation

A linear choice of a cocycle representative for each continuous cohomology class.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
Lean source · statement
def homologyRepresentativeSection
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (A : TopRep.{u} (ZMod p) G) (n : ℕ) :
    continuousCohomology n A →ₗ[ZMod p]
      ContinuousCohomology.cocycles A n
theorem

homologyRepresentativeSection_rightInverse

L81 ↗
ClassFieldTower.ProP.PresentationH2Aux.homologyRepresentativeSection_rightInverse
Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
Lean source · statement
theorem homologyRepresentativeSection_rightInverse
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (A : TopRep.{u} (ZMod p) G) (n : ℕ) :
    (ContinuousCohomology.π A n).hom.toLinearMap.comp
        (homologyRepresentativeSection A n) = LinearMap.id
theorem

freeBoundary_surjective

L90 ↗
ClassFieldTower.ProP.PresentationH2Aux.freeBoundary_surjective
Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
Lean source · statement
theorem freeBoundary_surjective
    {d : ℕ}
    (sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p))
    (hbasis : Cardinal.mk sourceData.basis = d) :
    Function.Surjective
      ((Cohomology.trivialZModPCochainsLifted p sourceData.carrier).toCycles 1 2).hom
def

freePrimitiveSection

L116 ↗
ClassFieldTower.ProP.PresentationH2Aux.freePrimitiveSection
Documentation

A linear choice of degree-one primitives for degree-two cocycles on the free source.

Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
Lean source · statement
def freePrimitiveSection
    {d : ℕ}
    (sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p))
    (hbasis : Cardinal.mk sourceData.basis = d) :
    Cohomology.trivialZModPCocyclesLifted p sourceData.carrier 2 →ₗ[ZMod p]
      (Cohomology.trivialZModPCochainsLifted p sourceData.carrier).X 1
theorem

freePrimitiveSection_rightInverse

L129 ↗
ClassFieldTower.ProP.PresentationH2Aux.freePrimitiveSection_rightInverse
Source context 9 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
Lean source · statement
theorem freePrimitiveSection_rightInverse
    {d : ℕ}
    (sourceData :
      FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (FiniteGroupClass.pGroup p))
    (hbasis : Cardinal.mk sourceData.basis = d) :
    ((Cohomology.trivialZModPCochainsLifted p sourceData.carrier).toCycles 1 2).hom.toLinearMap.comp
        (freePrimitiveSection sourceData hbasis) = LinearMap.id
def

targetCocycleSection

L150 ↗
ClassFieldTower.ProP.PresentationH2Aux.targetCocycleSection
Documentation

The chosen target degree-two cocycle representative.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
Lean source · statement
def targetCocycleSection :
    Cohomology.continuousCohomologyZModPLifted p G 2 →ₗ[ZMod p]
      Cohomology.trivialZModPCocyclesLifted p G 2
def

presentationPulledCocycle

L156 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationPulledCocycle
Documentation

Pull the chosen target representative back to the free presentation source.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
Lean source · statement
def presentationPulledCocycle
    (P : FiniteProPPresentation p d r sourceData G) :
    Cohomology.continuousCohomologyZModPLifted p G 2 →ₗ[ZMod p]
      Cohomology.trivialZModPCocyclesLifted p sourceData.carrier 2
def

presentationPrimitive

L164 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationPrimitive
Documentation

The chosen free-source primitive of the pulled-back target cocycle.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
Lean source · statement
def presentationPrimitive
    (P : FiniteProPPresentation p d r sourceData G) :
    Cohomology.continuousCohomologyZModPLifted p G 2 →ₗ[ZMod p]
      (Cohomology.trivialZModPCochainsLifted p sourceData.carrier).X 1
theorem

presentationPrimitive_toCycles

L171 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationPrimitive_toCycles
Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
Lean source · statement
theorem presentationPrimitive_toCycles
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2) :
    ((Cohomology.trivialZModPCochainsLifted p sourceData.carrier).toCycles 1 2).hom
        (presentationPrimitive P x) = presentationPulledCocycle P x
theorem

targetCocycleSection_π

L182 ↗
ClassFieldTower.ProP.PresentationH2Aux.targetCocycleSection_π
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem targetCocycleSection_π
    (x : Cohomology.continuousCohomologyZModPLifted p G 2) :
    ContinuousCohomology.π (Cohomology.trivialZModPLifted p G) 2
        (targetCocycleSection x) = x
theorem

presentationPrimitive_boundary

L191 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationPrimitive_boundary
Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
Lean source · statement
theorem presentationPrimitive_boundary
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2) :
    ((Cohomology.trivialZModPCochainsLifted p sourceData.carrier).d 1 2).hom
        (presentationPrimitive P x) =
      ((Cohomology.trivialZModPCochainsLifted p sourceData.carrier).iCycles 2).hom
        (presentationPulledCocycle P x)
theorem

presentationPulledCocycle_apply

L208 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationPulledCocycle_apply
Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
Lean source · statement
theorem presentationPulledCocycle_apply
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2)
    (f₀ f₁ f₂ : sourceData.carrier) :
    (((Cohomology.trivialZModPCochainsLifted p sourceData.carrier).iCycles 2).hom
        (presentationPulledCocycle P x)).1 f₀ f₁ f₂ =
      (((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom
        (targetCocycleSection x)).1 (P.quotient f₀) (P.quotient f₁) (P.quotient f₂)
theorem

homogeneousTwoCocycleEquation

L230 ↗
ClassFieldTower.ProP.PresentationH2Aux.homogeneousTwoCocycleEquation
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
omit [Fact p.Prime] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem homogeneousTwoCocycleEquation
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (x₀ x₁ x₂ x₃ : G) :
    (((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom z).1 x₁ x₂ x₃ -
        (((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom z).1 x₀ x₂ x₃ +
        (((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom z).1 x₀ x₁ x₃ -
      (((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom z).1 x₀ x₁ x₂ = 0
theorem

homogeneousTwoCocycle_leftInvariant

L255 ↗
ClassFieldTower.ProP.PresentationH2Aux.homogeneousTwoCocycle_leftInvariant
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
omit [Fact p.Prime] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem homogeneousTwoCocycle_leftInvariant
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (g x₀ x₁ x₂ : G) :
    (((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom z).1
        (g * x₀) (g * x₁) (g * x₂) =
      (((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom z).1 x₀ x₁ x₂
theorem

homogeneousTwoCocycle_one_one

L271 ↗
ClassFieldTower.ProP.PresentationH2Aux.homogeneousTwoCocycle_one_one
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
omit [Fact p.Prime] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem homogeneousTwoCocycle_one_one
    (z : Cohomology.trivialZModPCocyclesLifted p G 2) (g : G) :
    (((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom z).1 1 1 g =
      (((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom z).1 1 1 1
theorem

homogeneousTwoCocycle_one_diag

L279 ↗
ClassFieldTower.ProP.PresentationH2Aux.homogeneousTwoCocycle_one_diag
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
omit [Fact p.Prime] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem homogeneousTwoCocycle_one_diag
    (z : Cohomology.trivialZModPCocyclesLifted p G 2) (g : G) :
    (((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom z).1 1 g g =
      (((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom z).1 1 1 1
theorem

presentationPrimitive_boundary_apply

L294 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationPrimitive_boundary_apply
Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
Lean source · statement
theorem presentationPrimitive_boundary_apply
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2)
    (f₀ f₁ f₂ : sourceData.carrier) :
    (presentationPrimitive P x).1 f₁ f₂ -
        ((presentationPrimitive P x).1 f₀ f₂ -
          (presentationPrimitive P x).1 f₀ f₁) =
      (((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom
        (targetCocycleSection x)).1 (P.quotient f₀) (P.quotient f₁) (P.quotient f₂)
theorem

presentationPrimitive_leftInvariant

L313 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationPrimitive_leftInvariant
Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory Limits TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
namespace PresentationH2Aux
universe u
variable {p : ℕ}
variable [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
variable {d r : ℕ}
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
Lean source · statement
theorem presentationPrimitive_leftInvariant
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2)
    (a f g : sourceData.carrier) :
    (presentationPrimitive P x).1 (a⁻¹ * f) (a⁻¹ * g) =
      (presentationPrimitive P x).1 f g

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