Module

Derivative.lean

Nyll.ProCGroups.ProP.Fox.Derivative

6 declarations indexed from sourceView source ↗

Module documentation

Completed Fox derivatives of finite pro-p presentations

This leaf specializes the existing continuous completed Fox differential to the concrete quotient map carried by a finite pro-p presentation. The formation and closed-target hypotheses are derived from the presentation; they are not additional assumptions.

Imports2

Imported by3

theorem

pGroupFullFormation

L40 ↗

ClassFieldTower.ProP.pGroupFullFormation

Documentation

Finite p-groups form the full formation required by completed Fox calculus.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open CrowellExactSequence
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 pGroupFullFormation :
    FiniteGroupClass.FullFormation (FiniteGroupClass.pGroup p) where
  melnikovFormation :=
    { formation := FiniteGroupClass.pGroup_formation p
      normalSubgroupClosed := fun N _ hN =>
        FiniteGroupClass.pGroup_subgroupClosed p N hN
      extensionClosed := FiniteGroupClass.pGroup_extensionClosed p }
  subgroupClosed := FiniteGroupClass.pGroup_subgroupClosed p

theorem

presentationFoxClosedTargetBasis

L51 ↗

ClassFieldTower.ProP.presentationFoxClosedTargetBasis

Documentation

Surjectivity of the presentation quotient supplies the closed pro-p target used by the completed Fox derivative.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open CrowellExactSequence
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 presentationFoxClosedTargetBasis
    (P : FiniteProPPresentation p d r sourceData G) :
    ProC.HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p)
      (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
        (C := FiniteGroupClass.pGroup p)
        (fun i : ULift.{u} (Fin d) =>
          P.quotient
            (freeProCChosenULiftFamilyOfBasisCard
              sourceData P.basisCard i)) : Subgroup
        (ZCCompletedFoxSemidirect
          (FiniteGroupClass.pGroup p) (ULift.{u} (Fin d)) G)) :=
  freeProCClosedGeneratedTarget_proC_of_surjective
    (C := FiniteGroupClass.pGroup p)
    (hC := pGroupFullFormation (p := p))
    sourceData P.basisCard P.quotient P.quotient_surjective

abbrev

PresentationFoxCoordinates

L68 ↗

ClassFieldTower.ProP.PresentationFoxCoordinates

Documentation

Completed pro-p integral Fox coordinates for the chosen finite basis.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open CrowellExactSequence
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

abbrev PresentationFoxCoordinates

abbrev

PresentationFoxCoefficientRing

L73 ↗

ClassFieldTower.ProP.PresentationFoxCoefficientRing

Documentation

The completed coefficient ring acting on presentation Fox rows.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open CrowellExactSequence
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

abbrev PresentationFoxCoefficientRing

def

presentationFoxDerivative

L77 ↗

ClassFieldTower.ProP.presentationFoxDerivative

Documentation

The existing completed Fox derivative attached to the presentation.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open CrowellExactSequence
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

def presentationFoxDerivative
    (P : FiniteProPPresentation p d r sourceData G) :
    ScalarCrossedHom
      (zcCompletedGroupAlgebraScalar
        (FiniteGroupClass.pGroup p) P.quotient.toMonoidHom)
      (PresentationFoxCoordinates (p := p) (d := d) (G := G))

theorem

continuous_presentationFoxDerivative

L91 ↗

ClassFieldTower.ProP.continuous_presentationFoxDerivative

Documentation

The presentation Fox derivative is continuous.

Source context 11 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
open CrowellExactSequence
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 continuous_presentationFoxDerivative
    (P : FiniteProPPresentation p d r sourceData G) :
    Continuous (presentationFoxDerivative P)

Module documentation

Completed Fox derivatives of finite pro-p presentations

Declarations

pGroupFullFormation

presentationFoxClosedTargetBasis

PresentationFoxCoordinates

PresentationFoxCoefficientRing

presentationFoxDerivative

continuous_presentationFoxDerivative