NYLL
Module

ClosedSpan.lean

Nyll.ProCGroups.ProP.Fox.ClosedSpan
5 declarations indexed from sourceView source ↗

Module documentation

Closed generation of completed kernel Fox rows

Continuity and crossed-product identities turn the inverse image of the displayed-row span into a closed normal subgroup. Since the displayed relators closed-normally generate the kernel, every kernel row lies in their closed coefficient span.

Imports1
Imported by2

Declarations

def

kernelRowsInDisplayedClosedSpan

L38 ↗
ClassFieldTower.ProP.kernelRowsInDisplayedClosedSpan
Documentation

Kernel elements whose completed Fox rows lie in the displayed closed span.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FoxDifferential
noncomputable section
universe u
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · full declaration
def kernelRowsInDisplayedClosedSpan
    (P : FiniteProPPresentation p d r sourceData G) :
    Subgroup sourceData.carrier where
  carrier := {x |
    x ∈ P.quotient.toMonoidHom.ker ∧
      presentationFoxDerivative P x ∈ displayedRelatorFoxRowClosedSpan P}
  one_mem' := by
    constructor
    · simp
    · rw [ScalarCrossedHom.map_one]
      exact (displayedRelatorFoxRowClosedSpan P).zero_mem
  mul_mem' := by
    intro x y hx hy
    constructor
    · exact P.quotient.toMonoidHom.ker.mul_mem hx.1 hy.1
    · rw [ScalarCrossedHom.map_mul]
      exact (displayedRelatorFoxRowClosedSpan P).add_mem hx.2
        ((displayedRelatorFoxRowClosedSpan P).smul_mem _ hy.2)
  inv_mem' := by
    intro x hx
    constructor
    · exact P.quotient.toMonoidHom.ker.inv_mem hx.1
    · rw [ScalarCrossedHom.map_inv]
      exact (displayedRelatorFoxRowClosedSpan P).neg_mem
        ((displayedRelatorFoxRowClosedSpan P).smul_mem _ hx.2)
theorem

kernelRowsInDisplayedClosedSpan_normal

L65 ↗
ClassFieldTower.ProP.kernelRowsInDisplayedClosedSpan_normal
Documentation

The row-controlled kernel subgroup is normal in the free source.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FoxDifferential
noncomputable section
universe u
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · full declaration
theorem kernelRowsInDisplayedClosedSpan_normal
    (P : FiniteProPPresentation p d r sourceData G) :
    (kernelRowsInDisplayedClosedSpan P).Normal where
  conj_mem n hn g := by
    rcases hn with ⟨hnker, hnrow⟩
    constructor
    · change P.quotient (g * n * g⁻¹) = 1
      change P.quotient n = 1 at hnker
      simp [hnker]
    · rw [ScalarCrossedHom.map_conj]
      change P.quotient n = 1 at hnker
      have hcoeff :
          zcCompletedGroupAlgebraScalar
              (FiniteGroupClass.pGroup p) P.quotient.toMonoidHom
              (g * n * g⁻¹) = 1 := by
        simp [hnker]
      rw [hcoeff, one_smul]
      simpa only [add_sub_cancel_left] using
        (displayedRelatorFoxRowClosedSpan P).smul_mem
          (zcCompletedGroupAlgebraScalar
            (FiniteGroupClass.pGroup p) P.quotient.toMonoidHom g)
          hnrow
theorem

isClosed_kernelRowsInDisplayedClosedSpan

L89 ↗
ClassFieldTower.ProP.isClosed_kernelRowsInDisplayedClosedSpan
Documentation

The row-controlled kernel subgroup is topologically closed.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FoxDifferential
noncomputable section
universe u
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem isClosed_kernelRowsInDisplayedClosedSpan
    (P : FiniteProPPresentation p d r sourceData G) :
    IsClosed ((kernelRowsInDisplayedClosedSpan P : Subgroup sourceData.carrier) :
      Set sourceData.carrier)
theorem

displayedRelators_subset_kernelRowsInDisplayedClosedSpan

L119 ↗
ClassFieldTower.ProP.displayedRelators_subset_kernelRowsInDisplayedClosedSpan
Documentation

Every displayed relator belongs to the row-controlled kernel subgroup.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FoxDifferential
noncomputable section
universe u
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem displayedRelators_subset_kernelRowsInDisplayedClosedSpan
    (P : FiniteProPPresentation p d r sourceData G) :
    Set.range P.relator ⊆ kernelRowsInDisplayedClosedSpan P
theorem

kernelFoxRow_mem_displayedRelatorFoxRowClosedSpan

L130 ↗
ClassFieldTower.ProP.kernelFoxRow_mem_displayedRelatorFoxRowClosedSpan
Documentation

Every completed kernel row belongs to the closed coefficient span of the displayed finite row family.

Source context 10 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open FoxDifferential
noncomputable section
universe u
variable {p d r : ℕ} [Fact p.Prime]
variable {sourceData :
  FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
    (FiniteGroupClass.pGroup p)}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
Lean source · statement
theorem kernelFoxRow_mem_displayedRelatorFoxRowClosedSpan
    (P : FiniteProPPresentation p d r sourceData G)
    (x : P.quotient.toMonoidHom.ker) :
    kernelFoxRow P x ∈ displayedRelatorFoxRowClosedSpan P

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