Module

ProCIntegerStageCoeffProjection.lean

Nyll.ProCGroups.FoxDifferential.Completed.FreeProC.ProCIntegerStageCoeffProjection

12 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — free pro-\(C\) — pro c integer stage coeff projection

The principal declarations in this module are:

zcCompletedGroupAlgebraStageToFoxAlgebraicStage

A finite stage of \(\mathbb{Z}_C\llbracket H\rrbracket\) maps to a finite Fox target group algebra once its coefficient modulus dominates \(n\) and its finite quotient maps to \(F/N\).

zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap

The resulting completed-to-finite coefficient map.

zcCompletedGroupAlgebraStageToFoxAlgebraicStage_of

Evaluation on a completed group-algebra stage basis element.

zcCompletedGroupAlgebraStageToFoxAlgebraicStage_single

Evaluation on a single coefficient at a stage quotient element.

Imports2

Imported by2

def

zcCompletedGroupAlgebraStageToFoxAlgebraicStage

L49 ↗

FoxDifferential.zcCompletedGroupAlgebraStageToFoxAlgebraicStage

Documentation

A finite stage of \(\mathbb{Z}_C\llbracket H\rrbracket\) maps to a finite Fox target group algebra once its coefficient modulus dominates \(n\) and its finite quotient maps to \(F/N\).

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v
section OneStageToFiniteFox
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
variable (i : ZCCompletedGroupAlgebraIndex C H)

Lean source · statement

def zcCompletedGroupAlgebraStageToFoxAlgebraicStage
    (hmod : n ∣ i.1.modulus)
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N) :
    ZCCompletedGroupAlgebraStage C H i →+*
      foxAlgebraicStageTargetGroupAlgebra (X := X) N n

theorem

zcCompletedGroupAlgebraStageToFoxAlgebraicStage_of

L70 ↗

FoxDifferential.zcCompletedGroupAlgebraStageToFoxAlgebraicStage_of

Documentation

Evaluation on a completed group-algebra stage basis element.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v
section OneStageToFiniteFox
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
variable (i : ZCCompletedGroupAlgebraIndex C H)
omit [DecidableEq X] [Fact (0 < n)] in

Lean source · statement

theorem zcCompletedGroupAlgebraStageToFoxAlgebraicStage_of
    (hmod : n ∣ i.1.modulus)
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (q : CompletedGroupAlgebraQuotientInClass H C i.2) :
    zcCompletedGroupAlgebraStageToFoxAlgebraicStage
        (C := C) (X := X) (H := H) N n i hmod qmap
        (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
          (CompletedGroupAlgebraQuotientInClass H C i.2) q) =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N) (qmap q)

theorem

zcCompletedGroupAlgebraStageToFoxAlgebraicStage_single

L90 ↗

FoxDifferential.zcCompletedGroupAlgebraStageToFoxAlgebraicStage_single

Documentation

Evaluation on a single coefficient at a stage quotient element.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v
section OneStageToFiniteFox
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
variable (i : ZCCompletedGroupAlgebraIndex C H)
omit [DecidableEq X] [Fact (0 < n)] in

Lean source · statement

theorem zcCompletedGroupAlgebraStageToFoxAlgebraicStage_single
    (hmod : n ∣ i.1.modulus)
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (q : CompletedGroupAlgebraQuotientInClass H C i.2)
    (a : ModNCompletedCoeff i.1.modulus) :
    zcCompletedGroupAlgebraStageToFoxAlgebraicStage
        (C := C) (X := X) (H := H) N n i hmod qmap
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single (qmap q)
        (modNCompletedCoeffMap (n := n) (m := i.1.modulus) hmod a)

theorem

zcCompletedGroupAlgebraStageToFoxAlgebraicStage_self_injective

L132 ↗

FoxDifferential.zcCompletedGroupAlgebraStageToFoxAlgebraicStage_self_injective

Documentation

If no coefficient reduction is taken and the target quotient comparison is injective, then the finite-stage map from the completed group-algebra stage to the finite Fox target group algebra is injective.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v
section OneStageToFiniteFox
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
variable (i : ZCCompletedGroupAlgebraIndex C H)
omit [DecidableEq X] in

Lean source · statement

theorem zcCompletedGroupAlgebraStageToFoxAlgebraicStage_self_injective
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (hqmap : Function.Injective qmap) :
    Function.Injective
      (zcCompletedGroupAlgebraStageToFoxAlgebraicStage
        (C := C) (X := X) (H := H) N i.1.modulus i dvd_rfl qmap)

def

zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap

L166 ↗

FoxDifferential.zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap

Documentation

The resulting completed-to-finite coefficient map.

Source context 13 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v
section OneStageToFiniteFox
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
variable (i : ZCCompletedGroupAlgebraIndex C H)

Lean source · statement

def zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap
    (hmod : n ∣ i.1.modulus)
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N) :
    ZCCompletedGroupAlgebra C H →+*
      foxAlgebraicStageTargetGroupAlgebra (X := X) N n

theorem

zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_apply

L182 ↗

FoxDifferential.zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_apply

Documentation

The Fox algebraic stage coefficient map evaluates a completed element by stage projection followed by the prescribed target quotient and coefficient maps.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v
section OneStageToFiniteFox
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
variable (i : ZCCompletedGroupAlgebraIndex C H)
omit [DecidableEq X] [Fact (0 < n)] in

Lean source · statement

theorem zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_apply
    (hmod : n ∣ i.1.modulus)
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (a : ZCCompletedGroupAlgebra C H) :
    zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap
        (C := C) (X := X) (H := H) N n i hmod qmap a =
      zcCompletedGroupAlgebraStageToFoxAlgebraicStage
        (C := C) (X := X) (H := H) N n i hmod qmap
        (zcCompletedGroupAlgebraProjection C H i a)

theorem

zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_groupLike

L196 ↗

FoxDifferential.zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_groupLike

Documentation

Group-like formula for the completed-to-finite coefficient map.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v
section OneStageToFiniteFox
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
variable (i : ZCCompletedGroupAlgebraIndex C H)
omit [DecidableEq X] [Fact (0 < n)] in

Lean source · statement

theorem zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_groupLike
    (hmod : n ∣ i.1.modulus)
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (h : H) :
    zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap
        (C := C) (X := X) (H := H) N n i hmod qmap
        (zcGroupLike C H h) =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N)
        (qmap (QuotientGroup.mk h))

theorem

zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_groupLike_eq_stageRight

L213 ↗

FoxDifferential.zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_groupLike_eq_stageRight

Documentation

Group-like formula rewritten through a named finite right quotient map.

Source context 14 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v
section OneStageToFiniteFox
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable (N : Subgroup (FreeGroup X)) [N.Normal]
variable (n : ℕ) [Fact (0 < n)]
variable (i : ZCCompletedGroupAlgebraIndex C H)
omit [DecidableEq X] [Fact (0 < n)] in

Lean source · statement

theorem zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_groupLike_eq_stageRight
    (hmod : n ∣ i.1.modulus)
    (qmap : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (stageRight : H →* foxAlgebraicStageTargetQuotient (X := X) N)
    (hqmap : ∀ h : H, qmap (QuotientGroup.mk h) = stageRight h)
    (h : H) :
    zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap
        (C := C) (X := X) (H := H) N n i hmod qmap
        (zcGroupLike C H h) =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N) (stageRight h)

theorem

foxAlgebraicStageTargetGroupAlgebraMap_single_apply

L240 ↗

FoxDifferential.foxAlgebraicStageTargetGroupAlgebraMap_single_apply

Documentation

Target quotient maps send a single group-algebra coefficient to the mapped basis element.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v
section SingleCoefficientTransitions
variable {X : Type u} [DecidableEq X]
variable {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal]
variable (hNM : N ≤ M)
variable {n m : ℕ} [Fact (0 < n)] [Fact (0 < m)]
variable (hnm : n ∣ m)
omit [DecidableEq X] [Fact (0 < n)] in

Lean source · statement

theorem foxAlgebraicStageTargetGroupAlgebraMap_single_apply
    (q : foxAlgebraicStageTargetQuotient (X := X) N)
    (a : ModNCompletedCoeff n) :
    foxAlgebraicStageTargetGroupAlgebraMap (X := X) hNM n
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single (foxAlgebraicStageTargetQuotientMap (X := X) hNM q) a

theorem

foxAlgebraicStageBifilteredTargetGroupAlgebraMap_single_apply

L251 ↗

FoxDifferential.foxAlgebraicStageBifilteredTargetGroupAlgebraMap_single_apply

Documentation

The bifiltered target transition on a single group-algebra coefficient.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v
section SingleCoefficientTransitions
variable {X : Type u} [DecidableEq X]
variable {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal]
variable (hNM : N ≤ M)
variable {n m : ℕ} [Fact (0 < n)] [Fact (0 < m)]
variable (hnm : n ∣ m)
omit [DecidableEq X] [Fact (0 < n)] [Fact (0 < m)] in

Lean source · statement

theorem foxAlgebraicStageBifilteredTargetGroupAlgebraMap_single_apply
    (q : foxAlgebraicStageTargetQuotient (X := X) N)
    (a : ModNCompletedCoeff m) :
    foxAlgebraicStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
        (MonoidAlgebra.single q a) =
      MonoidAlgebra.single (foxAlgebraicStageTargetQuotientMap (X := X) hNM q)
        (modNCompletedCoeffMap (n := n) (m := m) hnm a)

theorem

zcCompletedGroupAlgebraStageToFoxAlgebraicStage_transition

L282 ↗

FoxDifferential.zcCompletedGroupAlgebraStageToFoxAlgebraicStage_transition

Documentation

Stage-to-finite maps commute with completed-group-algebra transitions when the coefficient reductions and quotient maps commute.

Source context 17 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v
section Transition
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal]
variable (hNM : N ≤ M)
variable {n m : ℕ} [Fact (0 < n)] [Fact (0 < m)]
variable (hnm : n ∣ m)
variable {i j : ZCCompletedGroupAlgebraIndex C H}
variable (hij : i ≤ j)
omit [DecidableEq X] [Fact (0 < n)] [Fact (0 < m)] in

Lean source · statement

theorem zcCompletedGroupAlgebraStageToFoxAlgebraicStage_transition
    (hmod_i : n ∣ i.1.modulus)
    (hmod_j : m ∣ j.1.modulus)
    (hcoeff : ∀ a : ModNCompletedCoeff j.1.modulus,
      modNCompletedCoeffMap (n := n) (m := i.1.modulus) hmod_i
          (modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1 a) =
        modNCompletedCoeffMap (n := n) (m := m) hnm
          (modNCompletedCoeffMap (n := m) (m := j.1.modulus) hmod_j a))
    (qmap_i : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) M)
    (qmap_j : CompletedGroupAlgebraQuotientInClass H C j.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (hqmap : ∀ q : CompletedGroupAlgebraQuotientInClass H C j.2,
      qmap_i
          ((OpenNormalSubgroupInClass.map
            (C := C) (G := H)
            (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) =
        foxAlgebraicStageTargetQuotientMap (X := X) hNM (qmap_j q))
    (x : ZCCompletedGroupAlgebraStage C H j) :
    foxAlgebraicStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
        (zcCompletedGroupAlgebraStageToFoxAlgebraicStage
          (C := C) (X := X) (H := H) N m j hmod_j qmap_j x) =
      zcCompletedGroupAlgebraStageToFoxAlgebraicStage
        (C := C) (X := X) (H := H) M n i hmod_i qmap_i
        (zcCompletedGroupAlgebraTransition C H hij x)

theorem

zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_transition

L374 ↗

FoxDifferential.zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_transition

Documentation

The completed coefficient maps built from stage projections are compatible on completed points once the underlying finite-stage maps commute with transitions.

Source context 17 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.ProC
open ProCGroups.InverseSystems
universe u v
section Transition
variable {C : ProCGroups.FiniteGroupClass}
variable {X H : Type u}
variable [DecidableEq X]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal]
variable (hNM : N ≤ M)
variable {n m : ℕ} [Fact (0 < n)] [Fact (0 < m)]
variable (hnm : n ∣ m)
variable {i j : ZCCompletedGroupAlgebraIndex C H}
variable (hij : i ≤ j)
omit [DecidableEq X] [Fact (0 < n)] [Fact (0 < m)] in

Lean source · statement

theorem zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap_transition
    (hmod_i : n ∣ i.1.modulus)
    (hmod_j : m ∣ j.1.modulus)
    (hcoeff : ∀ a : ModNCompletedCoeff j.1.modulus,
      modNCompletedCoeffMap (n := n) (m := i.1.modulus) hmod_i
          (modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1 a) =
        modNCompletedCoeffMap (n := n) (m := m) hnm
          (modNCompletedCoeffMap (n := m) (m := j.1.modulus) hmod_j a))
    (qmap_i : CompletedGroupAlgebraQuotientInClass H C i.2 →*
      foxAlgebraicStageTargetQuotient (X := X) M)
    (qmap_j : CompletedGroupAlgebraQuotientInClass H C j.2 →*
      foxAlgebraicStageTargetQuotient (X := X) N)
    (hqmap : ∀ q : CompletedGroupAlgebraQuotientInClass H C j.2,
      qmap_i
          ((OpenNormalSubgroupInClass.map
            (C := C) (G := H)
            (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) =
        foxAlgebraicStageTargetQuotientMap (X := X) hNM (qmap_j q))
    (a : ZCCompletedGroupAlgebra C H) :
    foxAlgebraicStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
        (zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap
          (C := C) (X := X) (H := H) N m j hmod_j qmap_j a) =
      zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap
        (C := C) (X := X) (H := H) M n i hmod_i qmap_i a

Module documentation

Fox differential: completed — free pro-\(C\) — pro c integer stage coeff projection

Declarations