NYLL
Module

H2FiniteStageCochain.lean

Nyll.GaloisCohomology.ProP.H2FiniteStageCochain
20 declarations indexed from sourceView source ↗

Module documentation

Finite-stage realization of continuous degree-two classes

Imports4
Imported by2

Declarations

abbrev

Coordinate

L34 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.Coordinate
Documentation

A universe-compatible three-element coordinate type.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
abbrev Coordinate
abbrev

Triple

L37 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.Triple
Documentation

The threefold product used to factor a homogeneous two-cocycle.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
abbrev Triple (G : Type u)
def

coordinateIndex

L40 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.coordinateIndex
Documentation

Include a small coordinate into the universe-lifted coordinate type.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
def coordinateIndex (i : Fin 3) : Coordinate
def

triple

L43 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.triple
Documentation

Assemble three entries as an element of the threefold product.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
def triple (a b c : G) : Triple G
def

coordinateHom

L47 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.coordinateHom
Documentation

The continuous homomorphism supported at one coordinate.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · full declaration
def coordinateHom (i : Coordinate) : G →ₜ* Triple G where
  toMonoidHom := MonoidHom.mulSingle (fun _ : Coordinate => G) i
  continuous_toFun := by
    change Continuous fun g : G => (Pi.mulSingle i g : Triple G)
    exact continuous_mulSingle (A := fun _ : Coordinate => G) i
def

coordinateSubgroup

L54 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.coordinateSubgroup
Documentation

Pull an in-class open normal subgroup back along one coordinate inclusion.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
def coordinateSubgroup
    (W : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) (Triple G))
    (i : Coordinate) :
    OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G
def

commonCoordinateSubgroup

L62 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.commonCoordinateSubgroup
Documentation

A common in-class open normal subgroup for all three coordinates.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
def commonCoordinateSubgroup
    (W : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) (Triple G)) :
    OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G
theorem

commonCoordinateSubgroup_le

L73 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.commonCoordinateSubgroup_le
Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
  [TotallyDisconnectedSpace G] in
Lean source · statement
theorem commonCoordinateSubgroup_le
    (W : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) (Triple G))
    (i : Fin 3) :
    ((commonCoordinateSubgroup W).1 : Subgroup G) ≤
      ((coordinateSubgroup W (coordinateIndex i)).1 : Subgroup G)
theorem

mulSingle_mem_of_mem_common

L85 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.mulSingle_mem_of_mem_common
Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
  [TotallyDisconnectedSpace G] in
Lean source · statement
theorem mulSingle_mem_of_mem_common
    (W : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) (Triple G))
    (i : Fin 3) {g : G}
    (hg : g ∈ ((commonCoordinateSubgroup W).1 : Subgroup G)) :
    Pi.mulSingle (coordinateIndex i) g ∈ (W.1 : Subgroup (Triple G))
theorem

map_eq_of_coordinate_quotients

L96 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.map_eq_of_coordinate_quotients
Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
  [TotallyDisconnectedSpace G] in
Lean source · statement
theorem map_eq_of_coordinate_quotients
    (W : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) (Triple G))
    (rho : Triple G → ULift.{u} (ZMod p))
    (rhoW : (Triple G ⧸ (W.1 : Subgroup (Triple G))) → ULift.{u} (ZMod p))
    (hfac : rho = rhoW ∘ OpenNormalSubgroupInClass.quotientProj W)
    (a b : Triple G)
    (hab : ∀ i : Fin 3, OpenNormalSubgroupInClass.quotientProj
        (commonCoordinateSubgroup W) (a (coordinateIndex i)) =
      OpenNormalSubgroupInClass.quotientProj
        (commonCoordinateSubgroup W) (b (coordinateIndex i))) :
    rho a = rho b
def

cocycleValue

L124 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.cocycleValue
Documentation

Evaluate a homogeneous two-cocycle on three elements.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
def cocycleValue
    (z : trivialZModPCocyclesLifted p G 2) (a b c : G) :
    ULift.{u} (ZMod p)
def

cocycleTupleMap

L130 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.cocycleTupleMap
Documentation

Regard a homogeneous two-cocycle as a finite-valued map on a threefold product.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
def cocycleTupleMap
    (z : trivialZModPCocyclesLifted p G 2) (a : Triple G) :
    ULift.{u} (ZMod p)
theorem

cocycleTupleMap_continuous

L137 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.cocycleTupleMap_continuous
Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [Fact p.Prime] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem cocycleTupleMap_continuous
    (z : trivialZModPCocyclesLifted p G 2) :
    Continuous (cocycleTupleMap z)
theorem

cocycleTupleMap_leftInvariant

L149 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.cocycleTupleMap_leftInvariant
Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [Fact p.Prime] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem cocycleTupleMap_leftInvariant
    (z : trivialZModPCocyclesLifted p G 2) (g a b c : G) :
    cocycleTupleMap z (triple (g⁻¹ * a) (g⁻¹ * b) (g⁻¹ * c)) =
      cocycleTupleMap z (triple a b c)
def

quotientSection

L163 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.quotientSection
Documentation

A chosen set-theoretic section of an open-normal quotient projection.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
def quotientSection
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) :
    (G ⧸ (U.1 : Subgroup G)) → G
theorem

quotientProj_quotientSection

L171 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.quotientProj_quotientSection
Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
  [TotallyDisconnectedSpace G] in
Lean source · statement
theorem quotientProj_quotientSection
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (q : G ⧸ (U.1 : Subgroup G)) :
    OpenNormalSubgroupInClass.quotientProj U (quotientSection U q) = q
theorem

quotientProj_quotientSection_inv_mul

L180 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.quotientProj_quotientSection_inv_mul
Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
  [TotallyDisconnectedSpace G] in
Lean source · statement
theorem quotientProj_quotientSection_inv_mul
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G)
    (q r : G ⧸ (U.1 : Subgroup G)) :
    OpenNormalSubgroupInClass.quotientProj U (quotientSection U (q⁻¹ * r)) =
      OpenNormalSubgroupInClass.quotientProj U
        ((quotientSection U q)⁻¹ * quotientSection U r)
theorem

quotientProj_quotientSection_proj

L191 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.quotientProj_quotientSection_proj
Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
  [TotallyDisconnectedSpace G] in
Lean source · statement
theorem quotientProj_quotientSection_proj
    (U : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) G) (g : G) :
    OpenNormalSubgroupInClass.quotientProj U
        (quotientSection U (OpenNormalSubgroupInClass.quotientProj U g)) =
      OpenNormalSubgroupInClass.quotientProj U g
def

descendedHomogeneousCochain

L199 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.descendedHomogeneousCochain
Documentation

Descend a homogeneous cocycle cochain through a common coordinate quotient.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
def descendedHomogeneousCochain
    (W : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) (Triple G))
    (z : trivialZModPCocyclesLifted p G 2)
    (heq : ∀ a b : Triple G,
      (∀ i : Fin 3, OpenNormalSubgroupInClass.quotientProj
          (commonCoordinateSubgroup W) (a (coordinateIndex i)) =
        OpenNormalSubgroupInClass.quotientProj
          (commonCoordinateSubgroup W) (b (coordinateIndex i))) →
      cocycleTupleMap z a = cocycleTupleMap z b) :
    (trivialZModPCochainsLifted p
      (G ⧸ ((commonCoordinateSubgroup W).1 : Subgroup G))).X 2
theorem

descendedHomogeneousCochain_mem_cycles

L248 ↗
ClassFieldTower.Cohomology.H2FiniteStageAux.descendedHomogeneousCochain_mem_cycles
Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.Cohomology
namespace H2FiniteStageAux
open CategoryTheory TopRep ContRepresentation
open ProCGroups ProCGroups.ProC
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in
Lean source · statement
theorem descendedHomogeneousCochain_mem_cycles
    (W : OpenNormalSubgroupInClass (FiniteGroupClass.pGroup p) (Triple G))
    (z : trivialZModPCocyclesLifted p G 2)
    (heq : ∀ a b : Triple G,
      (∀ i : Fin 3, OpenNormalSubgroupInClass.quotientProj
          (commonCoordinateSubgroup W) (a (coordinateIndex i)) =
        OpenNormalSubgroupInClass.quotientProj
          (commonCoordinateSubgroup W) (b (coordinateIndex i))) →
      cocycleTupleMap z a = cocycleTupleMap z b) :
    ((trivialZModPCochainsLifted p
      (G ⧸ ((commonCoordinateSubgroup W).1 : Subgroup G))).d 2 3).hom
        (descendedHomogeneousCochain W z heq) = 0

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