ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Boundary

2 Theorems | 1 Definition

The principal declarations in this module are:

residueFreeGroupFoxBoundary The residue Fox boundary/Euler map \(v \mapsto \sum_i v_i * ([\psi(x_i)]-1)\). - residueFreeGroupFoxBoundary_apply The residue free-group Fox boundary is evaluated on the canonical generators and then extended linearly to the residue coordinate module. - residueFreeGroupFoxBoundary_single The residue Fox boundary sends a coordinate basis vector to the corresponding augmentation generator.

imports

Imported by

Definition FoxDifferential.residueFreeGroupFoxBoundary

def residueFreeGroupFoxBoundary (n : ℕ) (ψ : FreeGroup X →* H) :
    ResidueFreeFoxCoordinates n H X →ₗ[ResidueGroupRing n H] ResidueGroupRing n H where
  toFun v :=
    ∑ i : X,
      v i *
        (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1)
  map_add' := by
    intro v w
    simp only [Pi.add_apply, MonoidAlgebra.of_apply, add_mul, Finset.sum_add_distrib]
  map_smul' := by
    intro r v
    simp only [Pi.smul_apply, smul_eq_mul, MonoidAlgebra.of_apply, mul_assoc, RingHom.id_apply,
        Finset.mul_sum]

The residue Fox boundary/Euler map \(v \mapsto \sum_i v_i * ([\psi(x_i)]-1)\).

Theorem FoxDifferential.residueFreeGroupFoxBoundary_apply

omit [DecidableEq X] in
theorem residueFreeGroupFoxBoundary_apply
    (n : ℕ) (ψ : FreeGroup X →* H) (v : ResidueFreeFoxCoordinates n H X) :
    residueFreeGroupFoxBoundary n ψ v =
      ∑ i : X,
        v i *
          (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1)

The residue free-group Fox boundary is evaluated on the canonical generators and then extended linearly to the residue coordinate module.

Show Lean proof

Theorem FoxDifferential.residueFreeGroupFoxBoundary_single

@[simp]
theorem residueFreeGroupFoxBoundary_single (n : ℕ) (ψ : FreeGroup X →* H) (i : X) :
    residueFreeGroupFoxBoundary n ψ
        (Pi.single i (1 : ResidueGroupRing n H)) =
      residueGroupRingBoundary n ψ (FreeGroup.of i)

The residue Fox boundary sends a coordinate basis vector to the corresponding augmentation generator.

Show Lean proof

ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Boundary

Declarations