Module

DiscreteCompletion.lean

Nyll.ProCGroups.FoxDifferential.Completed.Comparison.DiscreteCompletion

30 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — comparison — discrete completion

The principal declarations in this module are:

foxAlgebraicStageGroupRingReduction

Coefficient reduction from the integral group ring \(\mathbb{Z}[F/N]\) to the finite-stage target group algebra \((\mathbb{Z}/n\mathbb{Z})[F/N]\).

foxAlgebraicStageGroupRingReduction_of

The finite-stage group-ring reduction sends a group-like basis element to the same quotient basis element with reduced coefficient.

foxAlgebraicStageGroupRingReduction_apply

Coefficients of the finite-stage group-ring reduction are ordinary reduction modulo \(n\).

int_eq_zero_of_forall_zmod_cast_eq_zero

An integer whose image in every positive residue ring is zero is zero.

Imports3

Imported by3

def

foxAlgebraicStageGroupRingReduction

L45 ↗

FoxDifferential.foxAlgebraicStageGroupRingReduction

Documentation

Coefficient reduction from the integral group ring \(\mathbb{Z}[F/N]\) to the finite-stage target group algebra \((\mathbb{Z}/n\mathbb{Z})[F/N]\).

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

def foxAlgebraicStageGroupRingReduction :
    GroupRing (foxAlgebraicStageTargetQuotient (X := X) N) →+*
      foxAlgebraicStageTargetGroupAlgebra (X := X) N n

theorem

foxAlgebraicStageGroupRingReduction_of

L58 ↗

FoxDifferential.foxAlgebraicStageGroupRingReduction_of

Documentation

The finite-stage group-ring reduction sends a group-like basis element to the same quotient basis element with reduced coefficient.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStageGroupRingReduction_of
    (q : foxAlgebraicStageTargetQuotient (X := X) N) :
    foxAlgebraicStageGroupRingReduction (X := X) N n
        (MonoidAlgebra.of ℤ (foxAlgebraicStageTargetQuotient (X := X) N) q) =
      MonoidAlgebra.of (ModNCompletedCoeff n)
        (foxAlgebraicStageTargetQuotient (X := X) N) q

theorem

foxAlgebraicStageGroupRingReduction_apply

L70 ↗

FoxDifferential.foxAlgebraicStageGroupRingReduction_apply

Documentation

Coefficients of the finite-stage group-ring reduction are ordinary reduction modulo \(n\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem foxAlgebraicStageGroupRingReduction_apply
    (x : GroupRing (foxAlgebraicStageTargetQuotient (X := X) N))
    (q : foxAlgebraicStageTargetQuotient (X := X) N) :
    (foxAlgebraicStageGroupRingReduction (X := X) N n x).coeff q =
      (x.coeff q : ModNCompletedCoeff n)

theorem

int_eq_zero_of_forall_zmod_cast_eq_zero

L80 ↗

FoxDifferential.int_eq_zero_of_forall_zmod_cast_eq_zero

Documentation

An integer whose image in every positive residue ring is zero is zero.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem int_eq_zero_of_forall_zmod_cast_eq_zero
    (z : ℤ) (hz : ∀ n : ℕ, 0 < n → (z : ZMod n) = 0) :
    z = 0

theorem

int_eq_zero_of_forall_zmod_prime_pow_cast_eq_zero

L95 ↗

FoxDifferential.int_eq_zero_of_forall_zmod_prime_pow_cast_eq_zero

Documentation

An integer whose image in every \(p^k\) residue ring is zero is zero.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem int_eq_zero_of_forall_zmod_prime_pow_cast_eq_zero
    (p : ℕ) [Fact (Nat.Prime p)] (z : ℤ)
    (hz : ∀ k : ℕ, (z : ZMod (p ^ k)) = 0) :
    z = 0

theorem

groupRing_eq_zero_of_nsmul_eq_zero

L115 ↗

FoxDifferential.groupRing_eq_zero_of_nsmul_eq_zero

Documentation

Integral group rings are torsion-free for positive natural scalar multiplication.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem groupRing_eq_zero_of_nsmul_eq_zero
    {M : Type*} [Monoid M] {n : ℕ} (hn : 0 < n) (x : GroupRing M)
    (hx : n • x = 0) :
    x = 0

theorem

groupRing_eq_zero_of_forall_foxAlgebraicStageGroupRingReduction_eq_zero

L132 ↗

FoxDifferential.groupRing_eq_zero_of_forall_foxAlgebraicStageGroupRingReduction_eq_zero

Documentation

A finite-support integral group-ring element is zero if all of its positive residue reductions are zero.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem groupRing_eq_zero_of_forall_foxAlgebraicStageGroupRingReduction_eq_zero
    (x : GroupRing (foxAlgebraicStageTargetQuotient (X := X) N))
    (hx : ∀ n : ℕ, 0 < n →
      foxAlgebraicStageGroupRingReduction (X := X) N n x = 0) :
    x = 0

theorem

groupRing_eq_zero_of_forall_foxAlgebraicStageGroupRingReduction_primePow_eq_zero

L148 ↗

FoxDifferential.groupRing_eq_zero_of_forall_foxAlgebraicStageGroupRingReduction_primePow_eq_zero

Documentation

A finite-support integral group-ring element is zero if all of its \(p^k\) residue reductions are zero.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem groupRing_eq_zero_of_forall_foxAlgebraicStageGroupRingReduction_primePow_eq_zero
    (p : ℕ) [Fact (Nat.Prime p)]
    (x : GroupRing (foxAlgebraicStageTargetQuotient (X := X) N))
    (hx : ∀ k : ℕ,
      foxAlgebraicStageGroupRingReduction (X := X) N (p ^ k) x = 0) :
    x = 0

theorem

exists_eq_nsmul_of_foxAlgebraicStageGroupRingReduction_eq_zero

L165 ↗

FoxDifferential.exists_eq_nsmul_of_foxAlgebraicStageGroupRingReduction_eq_zero

Documentation

A finite-stage residue-zero integral group-ring element is divisible by the chosen coefficient modulus.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
omit [DecidableEq X] in

Lean source · statement

theorem exists_eq_nsmul_of_foxAlgebraicStageGroupRingReduction_eq_zero
    {n : ℕ}
    (x : GroupRing (foxAlgebraicStageTargetQuotient (X := X) N))
    (hx : foxAlgebraicStageGroupRingReduction (X := X) N n x = 0) :
    ∃ y : GroupRing (foxAlgebraicStageTargetQuotient (X := X) N), x = n • y

theorem

foxAlgebraicStageDerivativeVector_eq_discreteReduction

L205 ↗

FoxDifferential.foxAlgebraicStageDerivativeVector_eq_discreteReduction

Documentation

The finite-stage derivative vector is the image of the ordinary relative Fox derivative under coefficient reduction from \(\mathbb{Z}[F/N]\) to \((\mathbb{Z}/n\mathbb{Z})[F/N]\).

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · full declaration

theorem foxAlgebraicStageDerivativeVector_eq_discreteReduction
    (w : FreeGroup X) :
    foxAlgebraicStageDerivativeVector (X := X) N n w =
      fun i : X =>
        foxAlgebraicStageGroupRingReduction (X := X) N n
          (FoxCalculus.relativeFreeGroupFoxDerivative
            (H := foxAlgebraicStageTargetQuotient (X := X) N)
            X (QuotientGroup.mk' N) w i) := by
  let delta : ScalarCrossedHom
      (foxAlgebraicStageCoefficient (X := X) N n)
      (foxAlgebraicStageCoordinateVector (X := X) N n) :=
    { toFun := fun w i =>
        foxAlgebraicStageGroupRingReduction (X := X) N n
          (FoxCalculus.relativeFreeGroupFoxDerivative
            (H := foxAlgebraicStageTargetQuotient (X := X) N)
            X (QuotientGroup.mk' N) w i)
      map_mul' := by
        intro u v
        rw [scalarCrossedAction_apply]
        funext i
        change foxAlgebraicStageGroupRingReduction (X := X) N n
            (FoxCalculus.relativeFreeGroupFoxDerivative
              (H := foxAlgebraicStageTargetQuotient (X := X) N)
              X (QuotientGroup.mk' N) (u * v) i) =
          foxAlgebraicStageGroupRingReduction (X := X) N n
            (FoxCalculus.relativeFreeGroupFoxDerivative
              (H := foxAlgebraicStageTargetQuotient (X := X) N)
              X (QuotientGroup.mk' N) u i) +
            foxAlgebraicStageCoefficient (X := X) N n u *
              foxAlgebraicStageGroupRingReduction (X := X) N n
                (FoxCalculus.relativeFreeGroupFoxDerivative
                  (H := foxAlgebraicStageTargetQuotient (X := X) N)
                  X (QuotientGroup.mk' N) v i)
        rw [show
          FoxCalculus.relativeFreeGroupFoxDerivative
              (H := foxAlgebraicStageTargetQuotient (X := X) N)
              X (QuotientGroup.mk' N) (u * v) i =
            FoxCalculus.relativeFreeGroupFoxDerivative
              (H := foxAlgebraicStageTargetQuotient (X := X) N)
              X (QuotientGroup.mk' N) u i +
            (MonoidAlgebra.of ℤ (foxAlgebraicStageTargetQuotient (X := X) N)
                (QuotientGroup.mk' N u) :
                FoxDifferential.GroupRing (foxAlgebraicStageTargetQuotient (X := X) N)) *
              FoxCalculus.relativeFreeGroupFoxDerivative
                (H := foxAlgebraicStageTargetQuotient (X := X) N)
                X (QuotientGroup.mk' N) v i by
          simpa [Pi.add_apply, Pi.smul_apply, smul_eq_mul] using
            congrFun
              (FoxCalculus.relativeFreeGroupFoxDerivative_mul
                (H := foxAlgebraicStageTargetQuotient (X := X) N)
                X (QuotientGroup.mk' N) u v) i]
        rw [map_add, map_mul, foxAlgebraicStageGroupRingReduction_of]
        rfl }
  have hbasis :
      ∀ x : X, delta (FreeGroup.of x) =
        Pi.single x (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N n) := by
    intro x
    change (fun i : X =>
      foxAlgebraicStageGroupRingReduction (X := X) N n
        (FoxCalculus.relativeFreeGroupFoxDerivative
          (H := foxAlgebraicStageTargetQuotient (X := X) N)
          X (QuotientGroup.mk' N) (FreeGroup.of x) i)) =
      Pi.single x (1 : foxAlgebraicStageTargetGroupAlgebra (X := X) N n)
    funext i
    by_cases hix : i = x
    · subst i
      simp only [FoxCalculus.relativeFreeGroupFoxDerivative_of,
        Pi.single_eq_same, map_one]
    · simp only [FoxCalculus.relativeFreeGroupFoxDerivative_of,
        Pi.single_eq_of_ne hix, map_zero]
  have hdelta_eq :
      delta = foxAlgebraicStageDerivativeVectorCrossedHom (X := X) N n :=
    foxAlgebraicStageDerivativeVector_unique (X := X) N n delta hbasis
  have hw := congrArg (fun d => d w) hdelta_eq
  change
    foxAlgebraicStageDerivativeVectorCrossedHom (X := X) N n w = delta w
  exact hw.symm

theorem

foxAlgebraicStageDerivative_eq_discreteReduction

L287 ↗

FoxDifferential.foxAlgebraicStageDerivative_eq_discreteReduction

Documentation

The comparison between the finite-stage derivative and the ordinary relative Fox derivative holds componentwise.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem foxAlgebraicStageDerivative_eq_discreteReduction
    (i : X) (w : FreeGroup X) :
    foxAlgebraicStageDerivative (X := X) N n i w =
      foxAlgebraicStageGroupRingReduction (X := X) N n
        (FoxCalculus.relativeFreeGroupFoxDerivative
          (H := foxAlgebraicStageTargetQuotient (X := X) N)
          X (QuotientGroup.mk' N) w i)

theorem

exists_eq_nsmul_relFreeFoxDeriv_of_foxAlgebraicStageDerivativeVector_eq_zero

L302 ↗

FoxDifferential.exists_eq_nsmul_relFreeFoxDeriv_of_foxAlgebraicStageDerivativeVector_eq_zero

Documentation

One finite-stage derivative-vector vanishing says that the ordinary integral relative Fox derivative vector is divisible by the coefficient modulus.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem exists_eq_nsmul_relFreeFoxDeriv_of_foxAlgebraicStageDerivativeVector_eq_zero
    {n : ℕ} (w : FreeGroup X)
    (hder : foxAlgebraicStageDerivativeVector (X := X) N n w = 0) :
    ∃ y : X → GroupRing (foxAlgebraicStageTargetQuotient (X := X) N),
      FoxCalculus.relativeFreeGroupFoxDerivative
        (H := foxAlgebraicStageTargetQuotient (X := X) N)
        X (QuotientGroup.mk' N) w = n • y

theorem

exists_eq_nsmul_relFreeFoxDeriv_of_residueUnivDiff_eq_zero

L335 ↗

FoxDifferential.exists_eq_nsmul_relFreeFoxDeriv_of_residueUnivDiff_eq_zero

Documentation

Residue-universal version of one-modulus divisibility for the ordinary integral relative Fox derivative vector.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem exists_eq_nsmul_relFreeFoxDeriv_of_residueUnivDiff_eq_zero
    [Finite X]
    {n : ℕ} (w : FreeGroup X)
    (hres : residueUniversalDifferential n (QuotientGroup.mk' N) w = 0) :
    ∃ y : X → GroupRing (foxAlgebraicStageTargetQuotient (X := X) N),
      FoxCalculus.relativeFreeGroupFoxDerivative
        (H := foxAlgebraicStageTargetQuotient (X := X) N)
        X (QuotientGroup.mk' N) w = n • y

theorem

relFreeFoxDeriv_eq_zero_of_forall_foxAlgebraicStageDerivative_eq_zero

L355 ↗

FoxDifferential.relFreeFoxDeriv_eq_zero_of_forall_foxAlgebraicStageDerivative_eq_zero

Documentation

If every positive finite-stage derivative vanishes, then the ordinary integral relative Fox derivative vanishes.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem relFreeFoxDeriv_eq_zero_of_forall_foxAlgebraicStageDerivative_eq_zero
    (w : FreeGroup X)
    (hder :
      ∀ n : ℕ, 0 < n →
        ∀ i : X, foxAlgebraicStageDerivative (X := X) N n i w = 0) :
    FoxCalculus.relativeFreeGroupFoxDerivative
      (H := foxAlgebraicStageTargetQuotient (X := X) N)
      X (QuotientGroup.mk' N) w = 0

theorem

relFreeFoxDeriv_eq_zero_of_forall_foxAlgebraicStageDerivative_primePow_eq_zero

L375 ↗

FoxDifferential.relFreeFoxDeriv_eq_zero_of_forall_foxAlgebraicStageDerivative_primePow_eq_zero

Documentation

If every \(p^k\) finite-stage derivative vanishes, then the ordinary integral relative Fox derivative vanishes.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

Lean source · statement

theorem relFreeFoxDeriv_eq_zero_of_forall_foxAlgebraicStageDerivative_primePow_eq_zero
    (p : ℕ) [Fact (Nat.Prime p)] (w : FreeGroup X)
    (hder :
      ∀ k : ℕ,
        ∀ i : X, foxAlgebraicStageDerivative (X := X) N (p ^ k) i w = 0) :
    FoxCalculus.relativeFreeGroupFoxDerivative
      (H := foxAlgebraicStageTargetQuotient (X := X) N)
      X (QuotientGroup.mk' N) w = 0

theorem

zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction

L401 ↗

FoxDifferential.zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction

Documentation

Projecting the completed \(\mathbb{Z}_C\) derivative to a finite pro-\(C\) target stage gives the stage map applied to the reduced ordinary relative Fox derivative.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
section CompletedProjection
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
variable [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]

Lean source · full declaration

theorem zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction
    (i : X) (w : FreeGroup X)
    (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)) :
    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 : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
  rw [zcFreeGroupFoxDerivative_finiteStageProjection C N j i w]
  rw [foxAlgebraicStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]

theorem

zcFreeGroupFoxDerivativeVector_finiteStageProjection_discreteReduction

L417 ↗

FoxDifferential.zcFreeGroupFoxDerivativeVector_finiteStageProjection_discreteReduction

Documentation

Vector-valued form of the discrete-to-completed projection comparison.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
section CompletedProjection
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
variable [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]

Lean source · full declaration

theorem zcFreeGroupFoxDerivativeVector_finiteStageProjection_discreteReduction
    (w : FreeGroup X)
    (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)) :
    (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
  funext i
  exact zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction
    (C := C) (X := X) N i w j

theorem

zcFreeGroupFoxDerivative_unique_finiteStageProjection_discreteReduction

L438 ↗

FoxDifferential.zcFreeGroupFoxDerivative_unique_finiteStageProjection_discreteReduction

Documentation

The completed \(\mathbb{Z}_C\) component derivative is uniquely determined by the finite-stage projections of the ordinary relative Fox derivative after coefficient reduction.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
section CompletedProjection
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
variable [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]

Lean source · full declaration

theorem zcFreeGroupFoxDerivative_unique_finiteStageProjection_discreteReduction
    (i : X)
    (delta : FreeGroup X →
      ZCCompletedGroupAlgebra C (zcFiniteStageTarget X N))
    (hprojection : ∀ w
      (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
      zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j (delta 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)))) :
    delta = zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i := by
  refine zcFreeGroupFoxDerivative_unique_finiteStageProjection
    (C := C) (X := X) N i delta ?_
  intro w j
  let : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
  rw [hprojection w j]
  rw [← foxAlgebraicStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]

theorem

existsUnique_zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction

L463 ↗

FoxDifferential.existsUnique_zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction

Documentation

Existence and uniqueness of the completed \(\mathbb{Z}_C\) component derivative characterized by the finite-stage projections of the reduced ordinary relative Fox derivative.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
section CompletedProjection
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
variable [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]

Lean source · full declaration

theorem existsUnique_zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction
    (i : X) :
    ∃! delta : FreeGroup X →
      ZCCompletedGroupAlgebra C (zcFiniteStageTarget X N),
      ∀ w
        (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
        zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j (delta 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
  refine ⟨zcFreeGroupFoxDerivative C (QuotientGroup.mk' N) i, ?_, ?_⟩
  · intro w j
    exact zcFreeGroupFoxDerivative_finiteStageProjection_discreteReduction
      (C := C) (X := X) N i w j
  · intro delta hprojection
    exact zcFreeGroupFoxDerivative_unique_finiteStageProjection_discreteReduction
      (C := C) (X := X) N i delta hprojection

theorem

zcFreeGroupFoxDerivativeVector_unique_finiteStageProjection_discreteReduction

L488 ↗

FoxDifferential.zcFreeGroupFoxDerivativeVector_unique_finiteStageProjection_discreteReduction

Documentation

The completed \(\mathbb{Z}_C\) derivative vector is uniquely determined by the finite-stage projections of the ordinary relative Fox derivative after coefficient reduction.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
section CompletedProjection
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
variable [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]

Lean source · full declaration

theorem zcFreeGroupFoxDerivativeVector_unique_finiteStageProjection_discreteReduction
    (delta : FreeGroup X →
      ZCFreeFoxCoordinates C (X := X) (H := zcFiniteStageTarget X N))
    (hprojection : ∀ w
      (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
      (fun i : X =>
        zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j (delta 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))) :
    delta = zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N) := by
  refine zcFreeGroupFoxDerivativeVector_unique_finiteStageProjection
    (C := C) (X := X) N delta ?_
  intro w j
  funext i
  let : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
  have hcoord := congrFun (hprojection w j) i
  rw [hcoord]
  rw [← foxAlgebraicStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]

theorem

existsUnique_zcFreeFoxDerivVec_finiteStageProj_discreteReduction

L516 ↗

FoxDifferential.existsUnique_zcFreeFoxDerivVec_finiteStageProj_discreteReduction

Documentation

Existence and uniqueness of the completed \(\mathbb{Z}_C\) derivative vector characterized by the finite-stage projections of the reduced ordinary relative Fox derivative.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
section CompletedProjection
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
variable [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]

Lean source · full declaration

theorem existsUnique_zcFreeFoxDerivVec_finiteStageProj_discreteReduction :
    ∃! delta : FreeGroup X →
      ZCFreeFoxCoordinates C (X := X) (H := zcFiniteStageTarget X N),
      ∀ w
        (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)),
        (fun i : X =>
          zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
            (delta 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
  refine ⟨zcFreeGroupFoxDerivativeVector C (QuotientGroup.mk' N), ?_, ?_⟩
  · intro w j
    exact zcFreeGroupFoxDerivativeVector_finiteStageProjection_discreteReduction
      (C := C) (X := X) N w j
  · intro delta hprojection
    exact zcFreeGroupFoxDerivativeVector_unique_finiteStageProjection_discreteReduction
      (C := C) (X := X) N delta hprojection

theorem

zcFreeGroupFoxDerivative_fundFormula_finiteStageProj_discreteReduction

L543 ↗

FoxDifferential.zcFreeGroupFoxDerivative_fundFormula_finiteStageProj_discreteReduction

Documentation

Projecting the completed Fox-Euler formula and reducing the coefficients identifies the derivative coordinates with the ordinary relative Fox derivative.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
section CompletedProjection
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
variable [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]

Lean source · full declaration

theorem zcFreeGroupFoxDerivative_fundFormula_finiteStageProj_discreteReduction
    [Fintype X]
    (w : FreeGroup X)
    (j : ZCCompletedGroupAlgebraIndex C (zcFiniteStageTarget X N)) :
    zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
        (zcCompletedGroupAlgebraBoundary C (QuotientGroup.mk' N) w) =
      ∑ 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))) *
        zcCompletedGroupAlgebraProjection C (zcFiniteStageTarget X N) j
          (zcGroupLike C (zcFiniteStageTarget X N)
            (QuotientGroup.mk' N (FreeGroup.of i)) - 1) := by
  rw [zcFreeGroupFoxDerivative_fundamental_formula_finiteStageProjection_stageMap
    (C := C) (X := X) N w j]
  apply Finset.sum_congr rfl
  intro i hi
  let : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
  rw [foxAlgebraicStageDerivative_eq_discreteReduction (X := X) N j.1.modulus i w]

theorem

relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite

L570 ↗

FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite

Documentation

Over the all-finite coefficient class, a zero completed derivative vector on the finite quotient map already forces the ordinary integral relative Fox derivative to vanish.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
section CompletedProjection
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
variable [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]

Lean source · statement

theorem relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite
    [DiscreteTopology (foxAlgebraicStageTargetQuotient (X := X) N)]
    [Finite (foxAlgebraicStageTargetQuotient (X := X) N)]
    (w : FreeGroup X)
    (hw :
      zcFreeGroupFoxDerivativeVector
        (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
        (QuotientGroup.mk' N) w = 0) :
    FoxCalculus.relativeFreeGroupFoxDerivative
      (H := foxAlgebraicStageTargetQuotient (X := X) N)
      X (QuotientGroup.mk' N) w = 0

theorem

relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_allFinite

L617 ↗

FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_allFinite

Documentation

Over the all-finite coefficient class, a zero completed universal differential on the finite quotient map already forces the ordinary integral relative Fox derivative to vanish.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
section CompletedProjection
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
variable [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]

Lean source · statement

theorem relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_allFinite
    [DiscreteTopology (foxAlgebraicStageTargetQuotient (X := X) N)]
    [Finite (foxAlgebraicStageTargetQuotient (X := X) N)]
    (w : FreeGroup X)
    (hw :
      zcUniversalDifferential
        (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
        (QuotientGroup.mk' N) w = 0) :
    FoxCalculus.relativeFreeGroupFoxDerivative
      (H := foxAlgebraicStageTargetQuotient (X := X) N)
      X (QuotientGroup.mk' N) w = 0

theorem

relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup

L640 ↗

FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup

Documentation

Over the finite \(p\)-group coefficient class, a zero completed derivative vector on the finite quotient map forces the ordinary integral relative Fox derivative to vanish, using only the prime-power coefficient stages.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
section CompletedProjection
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
variable [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]

Lean source · statement

theorem relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup
    (p : ℕ) [Fact (Nat.Prime p)]
    [DiscreteTopology (foxAlgebraicStageTargetQuotient (X := X) N)]
    (hCtarget :
      ProCGroups.FiniteGroupClass.pGroup p
        (foxAlgebraicStageTargetQuotient (X := X) N))
    (w : FreeGroup X)
    (hw :
      zcFreeGroupFoxDerivativeVector
        (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
        (QuotientGroup.mk' N) w = 0) :
    FoxCalculus.relativeFreeGroupFoxDerivative
      (H := foxAlgebraicStageTargetQuotient (X := X) N)
      X (QuotientGroup.mk' N) w = 0

theorem

relativeFreeGroupFoxDerivative_eq_zero_of_zcUniversalDifferential_eq_zero_pGroup

L686 ↗

FoxDifferential.relativeFreeGroupFoxDerivative_eq_zero_of_zcUniversalDifferential_eq_zero_pGroup

Documentation

Over the finite \(p\)-group coefficient class, a zero completed universal differential on the finite quotient map already forces the ordinary integral relative Fox derivative to vanish, using only the prime-power coefficient stages.

Source context 11 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section DiscreteCompletion
variable {X : Type u} [DecidableEq X]
variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
section CompletedProjection
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
variable [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]

Lean source · statement

theorem relativeFreeGroupFoxDerivative_eq_zero_of_zcUniversalDifferential_eq_zero_pGroup
    (p : ℕ) [Fact (Nat.Prime p)]
    [DiscreteTopology (foxAlgebraicStageTargetQuotient (X := X) N)]
    (hCtarget :
      ProCGroups.FiniteGroupClass.pGroup p
        (foxAlgebraicStageTargetQuotient (X := X) N))
    (w : FreeGroup X)
    (hw :
      zcUniversalDifferential
        (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
        (QuotientGroup.mk' N) w = 0) :
    FoxCalculus.relativeFreeGroupFoxDerivative
      (H := foxAlgebraicStageTargetQuotient (X := X) N)
      X (QuotientGroup.mk' N) w = 0

theorem

relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj

L721 ↗

FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj

Documentation

All-finite coefficient separation holds for an arbitrary finite discrete target map. The quotient-map version is applied after identifying the target with \(\mathrm{FreeGroup}(X)/\ker \psi\), and completed derivative vectors are transported by target naturality.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section FiniteTarget
variable {X : Type u} [DecidableEq X]
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj
    [DiscreteTopology H] [Finite H]
    (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
    (w : FreeGroup X)
    (hw :
      zcFreeGroupFoxDerivativeVector
        (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
        ψ w = 0) :
    FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0

theorem

relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_allFinite_of_surj

L782 ↗

FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_allFinite_of_surj

Documentation

Over the all-finite coefficient class, a zero completed universal differential on an arbitrary finite discrete target map already forces the ordinary integral relative Fox derivative to vanish.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section FiniteTarget
variable {X : Type u} [DecidableEq X]
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_allFinite_of_surj
    [DiscreteTopology H] [Finite H]
    (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
    (w : FreeGroup X)
    (hw :
      zcUniversalDifferential
        (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{u})
        ψ w = 0) :
    FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0

theorem

relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj

L802 ↗

FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj

Documentation

Prime-power coefficient separation for an arbitrary finite discrete \(p\)-group target map. The quotient-map version is applied after identifying the target with \(\mathrm{FreeGroup}(X)/\ker \psi\); completed derivative vectors are transported by target naturality.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section FiniteTarget
variable {X : Type u} [DecidableEq X]
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj
    (p : ℕ) [Fact (Nat.Prime p)]
    [DiscreteTopology H]
    (hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)
    (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
    (w : FreeGroup X)
    (hw :
      zcFreeGroupFoxDerivativeVector
        (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
        ψ w = 0) :
    FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0

theorem

relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_pGroup_of_surj

L869 ↗

FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_pGroup_of_surj

Documentation

Over the finite \(p\)-group coefficient class, a zero completed universal differential on an arbitrary finite discrete \(p\)-group target map already forces the ordinary integral relative Fox derivative to vanish.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u
section FiniteTarget
variable {X : Type u} [DecidableEq X]
variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_pGroup_of_surj
    (p : ℕ) [Fact (Nat.Prime p)]
    [DiscreteTopology H]
    (hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)
    (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
    (w : FreeGroup X)
    (hw :
      zcUniversalDifferential
        (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{u})
        ψ w = 0) :
    FoxCalculus.relativeFreeGroupFoxDerivative (H := H) X ψ w = 0

Module documentation

Fox differential: completed — comparison — discrete completion

Declarations