NYLL
Module

PresentationH2KernelCharacter.lean

Nyll.GaloisCohomology.ProP.PresentationH2KernelCharacter
10 declarations indexed from sourceView source ↗

Module documentation

Kernel characters extracted from presentation degree-two classes

The normalized free-source primitive restricts to a continuous conjugation-invariant character of the presentation kernel. The construction is linear in the degree-two cohomology class.

Imports4
Imported by2

Declarations

instance

presentationH2KernelCanonicalZModAddCommGroup

L32 ↗
ClassFieldTower.ProP.presentationH2KernelCanonicalZModAddCommGroup
Source context 7 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open PresentationH2Aux
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
Lean source · statement
instance presentationH2KernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p)
instance

presentationContinuousH1Module

L41 ↗
ClassFieldTower.ProP.presentationContinuousH1Module
Source context 12 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open PresentationH2Aux
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance presentationH2KernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
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
instance presentationContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H))
def

presentationNormalizedPrimitiveValue

L49 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationNormalizedPrimitiveValue
Documentation

The normalized inhomogeneous value of the chosen free-source primitive.

Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open PresentationH2Aux
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance presentationH2KernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
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)}
local instance presentationContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · statement
def presentationNormalizedPrimitiveValue
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2)
    (f : sourceData.carrier) : ZMod p
theorem

presentationPrimitive_base

L55 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationPrimitive_base
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open PresentationH2Aux
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance presentationH2KernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
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)}
local instance presentationContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · statement
theorem presentationPrimitive_base
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2) :
    (presentationPrimitive P x).1 1 1 =
      (((Cohomology.trivialZModPCochainsLifted p G).iCycles 2).hom
        (targetCocycleSection x)).1 1 1 1
theorem

presentationNormalizedPrimitive_mul_of_left_kernel

L63 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationNormalizedPrimitive_mul_of_left_kernel
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open PresentationH2Aux
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance presentationH2KernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
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)}
local instance presentationContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · statement
theorem presentationNormalizedPrimitive_mul_of_left_kernel
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2)
    (a b : sourceData.carrier) (ha : P.quotient a = 1) :
    presentationNormalizedPrimitiveValue P x (a * b) =
      presentationNormalizedPrimitiveValue P x a +
        presentationNormalizedPrimitiveValue P x b
theorem

presentationNormalizedPrimitive_mul_of_right_kernel

L123 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationNormalizedPrimitive_mul_of_right_kernel
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open PresentationH2Aux
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance presentationH2KernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
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)}
local instance presentationContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · statement
theorem presentationNormalizedPrimitive_mul_of_right_kernel
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2)
    (a b : sourceData.carrier) (hb : P.quotient b = 1) :
    presentationNormalizedPrimitiveValue P x (a * b) =
      presentationNormalizedPrimitiveValue P x a +
        presentationNormalizedPrimitiveValue P x b
def

presentationKernelH1OfClass

L184 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationKernelH1OfClass
Documentation

The continuous kernel character extracted from a degree-two target class.

Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open PresentationH2Aux
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance presentationH2KernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
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)}
local instance presentationContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · full declaration
def presentationKernelH1OfClass
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2) :
    ContinuousH1ZMod (p := p) (G := P.quotient.toMonoidHom.ker) where
  toFun n := presentationNormalizedPrimitiveValue P x n.toMul
  map_zero' := by
    change presentationNormalizedPrimitiveValue P x 1 = 0
    unfold presentationNormalizedPrimitiveValue
    rw [sub_self]
    rfl
  map_add' := by
    intro n m
    change presentationNormalizedPrimitiveValue P x ((n.toMul : _) * m.toMul) =
      presentationNormalizedPrimitiveValue P x n.toMul +
        presentationNormalizedPrimitiveValue P x m.toMul
    apply presentationNormalizedPrimitive_mul_of_left_kernel P x
    exact n.toMul.2
  continuous_toFun := by
    change Continuous fun n : P.quotient.toMonoidHom.ker ↦
      (((presentationPrimitive P x).1 1 (n : sourceData.carrier)) -
        (presentationPrimitive P x).1 1 1).down
    exact ((ContinuousLinearEquiv.ulift :
      ULift.{u} (ZMod p) ≃L[ZMod p] ZMod p).continuous).comp <|
        (((presentationPrimitive P x).1 1).continuous.comp continuous_subtype_val).sub
          continuous_const
theorem

presentationKernelH1OfClass_invariant

L210 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationKernelH1OfClass_invariant
Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open PresentationH2Aux
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance presentationH2KernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
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)}
local instance presentationContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · statement
theorem presentationKernelH1OfClass_invariant
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2)
    (f : sourceData.carrier) (n : P.quotient.toMonoidHom.ker) :
    presentationKernelH1OfClass P x
        (Additive.ofMul (MulAut.conjNormal f n)) =
      presentationKernelH1OfClass P x (Additive.ofMul n)
def

presentationH2KernelClass

L245 ↗
ClassFieldTower.ProP.PresentationH2Aux.presentationH2KernelClass
Documentation

The extracted character, together with its free-source conjugation invariance.

Source context 14 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open PresentationH2Aux
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance presentationH2KernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
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)}
local instance presentationContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
namespace PresentationH2Aux
Lean source · statement
def presentationH2KernelClass
    (P : FiniteProPPresentation p d r sourceData G)
    (x : Cohomology.continuousCohomologyZModPLifted p G 2) :
    InvariantKernelH1 P
def

presentationH2ToInvariantKernelH1

L254 ↗
ClassFieldTower.ProP.presentationH2ToInvariantKernelH1
Documentation

The linear map from target degree-two cohomology to invariant presentation-kernel classes.

Source context 13 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open PresentationH2Aux
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
local instance presentationH2KernelCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
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)}
local instance presentationContinuousH1Module
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := H)) :=
  continuousH1ZModModule
Lean source · full declaration
def presentationH2ToInvariantKernelH1
    (P : FiniteProPPresentation p d r sourceData G) :
    Cohomology.continuousCohomologyZModPLifted p G 2 →ₗ[ZMod p]
      InvariantKernelH1 P where
  toFun := presentationH2KernelClass P
  map_add' x y := by
    apply Subtype.ext
    ext n
    change presentationNormalizedPrimitiveValue P (x + y) n.toMul =
      presentationNormalizedPrimitiveValue P x n.toMul +
        presentationNormalizedPrimitiveValue P y n.toMul
    unfold presentationNormalizedPrimitiveValue
    rw [map_add]
    change
      (((presentationPrimitive P x).1 1 n.toMul +
          (presentationPrimitive P y).1 1 n.toMul) -
        ((presentationPrimitive P x).1 1 1 +
          (presentationPrimitive P y).1 1 1)).down = _
    have hu :
        ((presentationPrimitive P x).1 1 n.toMul +
            (presentationPrimitive P y).1 1 n.toMul) -
          ((presentationPrimitive P x).1 1 1 +
            (presentationPrimitive P y).1 1 1) =
        ((presentationPrimitive P x).1 1 n.toMul -
            (presentationPrimitive P x).1 1 1) +
          ((presentationPrimitive P y).1 1 n.toMul -
            (presentationPrimitive P y).1 1 1) := by abel
    have hd := congrArg ULift.down hu
    change _ =
      ((presentationPrimitive P x).1 1 n.toMul -
          (presentationPrimitive P x).1 1 1).down +
        ((presentationPrimitive P y).1 1 n.toMul -
          (presentationPrimitive P y).1 1 1).down at hd
    exact hd
  map_smul' a x := by
    apply Subtype.ext
    ext n
    let ev : ContinuousH1ZMod (p := p) (G := P.quotient.toMonoidHom.ker) →+ ZMod p :=
      { toFun := fun χ ↦ χ n
        map_zero' := rfl
        map_add' := fun _ _ ↦ rfl }
    change presentationNormalizedPrimitiveValue P (a • x) n.toMul =
      ev (a • (presentationH2KernelClass P x).1)
    rw [ZMod.map_smul ev]
    change presentationNormalizedPrimitiveValue P (a • x) n.toMul =
      a • presentationNormalizedPrimitiveValue P x n.toMul
    unfold presentationNormalizedPrimitiveValue
    rw [map_smul]
    change
      (a • (presentationPrimitive P x).1 1 n.toMul -
        a • (presentationPrimitive P x).1 1 1).down =
      a • ((presentationPrimitive P x).1 1 n.toMul -
        (presentationPrimitive P x).1 1 1).down
    rw [← smul_sub]
    rfl

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