ProCGroups.FoxDifferential.Completed.Comparison.QuotientFamily

10 Theorems | 2 Definitions | 3 Abbreviations | 1 Structure

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.

import

ProCGroups.FoxDifferential.Completed.Comparison.DiscreteCompletion

Imported by

Structure FoxDifferential.ZCFiniteStageQuotientBundle

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

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.

Abbreviation FoxDifferential.ZCFiniteStageQuotientBundle.Target

abbrev Target (_B : ZCFiniteStageQuotientBundle N) : Type u :=
  foxAlgebraicStageTargetQuotient (X := X) N

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

Theorem FoxDifferential.ZCFiniteStageQuotientBundle.targetFiniteInstance

omit [DecidableEq X] [N.Normal] in
theorem targetFiniteInstance (B : ZCFiniteStageQuotientBundle N) :
    Finite (Target (N := N) B)

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

Show Lean proof

Definition FoxDifferential.ZCFiniteStageQuotientBundle.targetTopology

@[reducible]
def targetTopology (_B : ZCFiniteStageQuotientBundle N) :
    TopologicalSpace (Target (N := N) _B) :=
  ⊥

The canonical discrete topology on a genuine finite quotient stage.

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

Theorem FoxDifferential.ZCFiniteStageQuotientBundle.targetDiscreteTopology

omit [DecidableEq X] [N.Normal] in
theorem targetDiscreteTopology (B : ZCFiniteStageQuotientBundle N) :
    @DiscreteTopology (Target (N := N) B) B.targetTopology

The genuine finite quotient stage has discrete topology.

Show Lean proof

Theorem FoxDifferential.ZCFiniteStageQuotientBundle.targetIsTopologicalGroup

omit [DecidableEq X] in
theorem targetIsTopologicalGroup (B : ZCFiniteStageQuotientBundle N) :
    @IsTopologicalGroup (Target (N := N) B) B.targetTopology inferInstance

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.

Show Lean proof

Definition FoxDifferential.ZCFiniteStageQuotientBundle.quotientMap

def quotientMap (_B : ZCFiniteStageQuotientBundle N) :
    FreeGroup X →* Target (N := N) _B :=
  QuotientGroup.mk' N

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

Theorem FoxDifferential.ZCFiniteStageQuotientBundle.quotientMap_surjective

omit [DecidableEq X] in
theorem quotientMap_surjective (B : ZCFiniteStageQuotientBundle N) :
    Function.Surjective B.quotientMap

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

Show Lean proof

Theorem FoxDifferential.ZCFiniteStageQuotientBundle.ofFinite

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

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

Show Lean proof

Abbreviation FoxDifferential.ZCFiniteStageQuotientBundle.Index

abbrev Index (B : ZCFiniteStageQuotientBundle N) : Type u :=
  letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
  ZCCompletedGroupAlgebraIndex C (Target (N := N) B)

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

Abbreviation FoxDifferential.ZCFiniteStageQuotientBundle.CompletedGroupAlgebra

abbrev CompletedGroupAlgebra (B : ZCFiniteStageQuotientBundle N) : Type u :=
  letI : TopologicalSpace (Target (N := N) B) := B.targetTopology
  letI : IsTopologicalGroup (Target (N := N) B) := B.targetIsTopologicalGroup
  ZCCompletedGroupAlgebra C (Target (N := N) B)

The completed group algebra of the bundled target quotient.

Theorem FoxDifferential.ZCFiniteStageQuotientBundle.scalarStage_apply

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))

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

Show Lean proof

Theorem FoxDifferential.ZCFiniteStageQuotientBundle.derivative_finiteStageProjection

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))

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

Show Lean proof

Theorem FoxDifferential.ZCFiniteStageQuotientBundle.derivativeVector_finiteStageProjection

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)

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

Show Lean proof

Theorem FoxDifferential.ZCFiniteStageQuotientBundle.derivative_finiteStageProjection_discreteReduction

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)))

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

Show Lean proof

Theorem FoxDifferential.ZCFiniteStageQuotientBundle.derivativeVector_finiteStageProjection_discreteReduction

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))

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

Show Lean proof

ProCGroups.FoxDifferential.Completed.Comparison.QuotientFamily

Declarations