Module

QuotientFamily.lean

Nyll.ProCGroups.FoxDifferential.Completed.Comparison.QuotientFamily

16 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — comparison — quotient family

The principal declarations in this module are:

ZCFiniteStageQuotientBundle

A bundled finite-stage quotient family for source-stage comparison theorems. The purpose is to carry the topology and topological-group structure on the quotient target once, instead of repeating these hypotheses at every comparison theorem.

Target

The target quotient carried by a finite-stage quotient bundle.

targetFiniteInstance

The finiteness instance certified by a genuine finite-stage quotient bundle.

targetDiscreteTopology

The genuine finite quotient stage has discrete topology.

Imports1

Nyll.ProCGroups.FoxDifferential.Completed.Comparison.DiscreteCompletion

Imported by2

structure

ZCFiniteStageQuotientBundle

L42 ↗

FoxDifferential.ZCFiniteStageQuotientBundle

Documentation

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]

Lean source · full declaration

structure ZCFiniteStageQuotientBundle where
  /-- Finiteness of the algebraic Fox-stage target quotient. -/
  targetFinite : Finite (foxAlgebraicStageTargetQuotient (X := X) N)

abbrev

Target

L52 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.Target

Documentation

The target quotient carried by a finite-stage quotient bundle.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
namespace ZCFiniteStageQuotientBundle
variable {N}
variable (C : ProCGroups.FiniteGroupClass.{u})

Lean source · statement

abbrev Target (_B : ZCFiniteStageQuotientBundle N) : Type u

theorem

targetFiniteInstance

L57 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.targetFiniteInstance

Documentation

The finiteness instance certified by a genuine finite-stage quotient bundle.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
namespace ZCFiniteStageQuotientBundle
variable {N}
variable (C : ProCGroups.FiniteGroupClass.{u})
omit [DecidableEq X] [N.Normal] in

Lean source · statement

theorem targetFiniteInstance (B : ZCFiniteStageQuotientBundle N) :
    Finite (Target (N := N) B)

def

targetTopology

L66 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.targetTopology

Documentation

The canonical discrete topology on a genuine finite quotient stage.

This keeps the historical projection-style name while removing the former arbitrary-topology field.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
namespace ZCFiniteStageQuotientBundle
variable {N}
variable (C : ProCGroups.FiniteGroupClass.{u})

Lean source · statement

def targetTopology (_B : ZCFiniteStageQuotientBundle N) :
    TopologicalSpace (Target (N := N) _B)

theorem

targetDiscreteTopology

L72 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.targetDiscreteTopology

Documentation

The genuine finite quotient stage has discrete topology.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
namespace ZCFiniteStageQuotientBundle
variable {N}
variable (C : ProCGroups.FiniteGroupClass.{u})
omit [DecidableEq X] [N.Normal] in

Lean source · statement

theorem targetDiscreteTopology (B : ZCFiniteStageQuotientBundle N) :
    @DiscreteTopology (Target (N := N) B) B.targetTopology

theorem

targetIsTopologicalGroup

L82 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.targetIsTopologicalGroup

Documentation

The canonical discrete topology makes the genuine finite quotient stage a topological group.

This keeps the historical projection-style name while deriving the structure rather than accepting it as unrelated input data.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
namespace ZCFiniteStageQuotientBundle
variable {N}
variable (C : ProCGroups.FiniteGroupClass.{u})
omit [DecidableEq X] in

Lean source · statement

theorem targetIsTopologicalGroup (B : ZCFiniteStageQuotientBundle N) :
    @IsTopologicalGroup (Target (N := N) B) B.targetTopology inferInstance

def

quotientMap

L89 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.quotientMap

Documentation

The canonical quotient morphism represented by a genuine finite-stage bundle.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
namespace ZCFiniteStageQuotientBundle
variable {N}
variable (C : ProCGroups.FiniteGroupClass.{u})

Lean source · statement

def quotientMap (_B : ZCFiniteStageQuotientBundle N) :
    FreeGroup X →* Target (N := N) _B

theorem

quotientMap_surjective

L95 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.quotientMap_surjective

Documentation

The canonical quotient morphism of a genuine finite-stage bundle is surjective.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
namespace ZCFiniteStageQuotientBundle
variable {N}
variable (C : ProCGroups.FiniteGroupClass.{u})
omit [DecidableEq X] in

Lean source · statement

theorem quotientMap_surjective (B : ZCFiniteStageQuotientBundle N) :
    Function.Surjective B.quotientMap

theorem

ofFinite

L101 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.ofFinite

Documentation

Bundle an already known finite quotient using its canonical discrete topology.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
namespace ZCFiniteStageQuotientBundle
variable {N}
variable (C : ProCGroups.FiniteGroupClass.{u})
omit [DecidableEq X] in

Lean source · statement

theorem ofFinite
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [Finite (foxAlgebraicStageTargetQuotient (X := X) N)] :
    ZCFiniteStageQuotientBundle N

abbrev

Index

L108 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.Index

Documentation

The completed pro-\(C\) stage indices for the bundled target quotient.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
namespace ZCFiniteStageQuotientBundle
variable {N}
variable (C : ProCGroups.FiniteGroupClass.{u})

Lean source · statement

abbrev Index (B : ZCFiniteStageQuotientBundle N) : Type u

abbrev

CompletedGroupAlgebra

L113 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.CompletedGroupAlgebra

Documentation

The completed group algebra of the bundled target quotient.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
namespace ZCFiniteStageQuotientBundle
variable {N}
variable (C : ProCGroups.FiniteGroupClass.{u})

Lean source · statement

abbrev CompletedGroupAlgebra (B : ZCFiniteStageQuotientBundle N) : Type u

theorem

scalarStage_apply

L122 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.scalarStage_apply

Documentation

The scalar stage attached to the quotient bundle is evaluated at the corresponding finite quotient and coefficient stage.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
namespace ZCFiniteStageQuotientBundle
variable {N}
variable (C : ProCGroups.FiniteGroupClass.{u})

Lean source · full declaration

theorem scalarStage_apply
    (B : ZCFiniteStageQuotientBundle N)
    (j : B.Index C) (w : FreeGroup X) :
    letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
    letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
    zcCompletedGroupAlgebraScalarStage C N j w =
      (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
       modNCompletedGroupAlgebraStageMapInClass j.1.modulus
        (zcFiniteStageTarget X N) C j.2
        (foxAlgebraicStageCoefficient (X := X) N j.1.modulus w)) := by
  let : TopologicalSpace (Target (N := N) B) := B.targetTopology
  let : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
  exact zcCompletedGroupAlgebraScalarStage_apply (C := C) (X := X) N j w

theorem

derivative_finiteStageProjection

L137 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.derivative_finiteStageProjection

Documentation

Completed derivative projection theorem, using the bundled quotient-family hypotheses.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
namespace ZCFiniteStageQuotientBundle
variable {N}
variable (C : ProCGroups.FiniteGroupClass.{u})

Lean source · full declaration

theorem derivative_finiteStageProjection
    (B : ZCFiniteStageQuotientBundle N)
    (j : B.Index C) (i : X) (w : FreeGroup X) :
    letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
    letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
    zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
        (zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w) =
      (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
       modNCompletedGroupAlgebraStageMapInClass j.1.modulus
        (zcFiniteStageTarget X N) C j.2
        (foxAlgebraicStageDerivative (X := X) N j.1.modulus i w)) := by
  let : TopologicalSpace (Target (N := N) B) := B.targetTopology
  let : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
  exact zcFreeGroupFoxDerivative_finiteStageProjection (C := C) (X := X) N j i w

theorem

derivativeVector_finiteStageProjection

L153 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.derivativeVector_finiteStageProjection

Documentation

Completed derivative-vector projection theorem, using the bundled quotient-family hypotheses.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
namespace ZCFiniteStageQuotientBundle
variable {N}
variable (C : ProCGroups.FiniteGroupClass.{u})

Lean source · full declaration

theorem derivativeVector_finiteStageProjection
    (B : ZCFiniteStageQuotientBundle N)
    (j : B.Index C) (w : FreeGroup X) :
    letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
    letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
    (fun i : X =>
      zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
        (zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)) =
      fun i : X =>
        letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
        modNCompletedGroupAlgebraStageMapInClass j.1.modulus
          (zcFiniteStageTarget X N) C j.2
          (foxAlgebraicStageDerivative (X := X) N j.1.modulus i w) := by
  let : TopologicalSpace (Target (N := N) B) := B.targetTopology
  let : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
  exact zcFreeGroupFoxDerivativeVector_finiteStageProjection (C := C) (X := X) N j w

theorem

derivative_finiteStageProjection_discreteReduction

L173 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.derivative_finiteStageProjection_discreteReduction

Documentation

Discrete-reduction derivative projection theorem, using the bundled quotient-family hypotheses.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
namespace ZCFiniteStageQuotientBundle
variable {N}
variable (C : ProCGroups.FiniteGroupClass.{u})

Lean source · full declaration

theorem derivative_finiteStageProjection_discreteReduction
    (B : ZCFiniteStageQuotientBundle N)
    (j : B.Index C) (i : X) (w : FreeGroup X) :
    letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
    letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
    zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
        (zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i w) =
      (letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
       modNCompletedGroupAlgebraStageMapInClass j.1.modulus
        (zcFiniteStageTarget X N) C j.2
        (foxAlgebraicStageGroupRingReduction (X := X) N j.1.modulus
          (FoxCalculus.relativeFreeGroupFoxDerivative
            (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i))) := by
  let : TopologicalSpace (Target (N := N) B) := B.targetTopology
  let : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
  exact zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction
    (C := C) (X := X) N i w j

theorem

derivativeVector_finiteStageProjection_discreteReduction

L195 ↗

FoxDifferential.ZCFiniteStageQuotientBundle.derivativeVector_finiteStageProjection_discreteReduction

Documentation

Discrete-reduction derivative-vector projection theorem, using the bundled quotient-family hypotheses.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
universe u
section FiniteStageQuotientBundle
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
namespace ZCFiniteStageQuotientBundle
variable {N}
variable (C : ProCGroups.FiniteGroupClass.{u})

Lean source · full declaration

theorem derivativeVector_finiteStageProjection_discreteReduction
    (B : ZCFiniteStageQuotientBundle N)
    (j : B.Index C) (w : FreeGroup X) :
    letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
    letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
    (fun i : X =>
      zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
        (zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) w i)) =
      fun i : X =>
        letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
        modNCompletedGroupAlgebraStageMapInClass j.1.modulus
          (zcFiniteStageTarget X N) C j.2
          (foxAlgebraicStageGroupRingReduction (X := X) N j.1.modulus
            (FoxCalculus.relativeFreeGroupFoxDerivative
              (H := zcFiniteStageTarget X N) X (QuotientGroup.mk' N) w i)) := by
  let : TopologicalSpace (Target (N := N) B) := B.targetTopology
  let : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
  exact zcFreeGroupFoxDerivativeVector_finiteStageProjection_discreteReduction
    (C := C) (X := X) N w j

Module documentation

Fox differential: completed — comparison — quotient family

Declarations