Module

Boundary.lean

Nyll.ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Boundary

3 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — residue — free group — boundary

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.

Imports2

Imported by2

def

residueFreeGroupFoxBoundary

L41 ↗

FoxDifferential.residueFreeGroupFoxBoundary

Documentation

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

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
section FiniteBasis
variable [Fintype X]

Lean source · full declaration

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]

theorem

residueFreeGroupFoxBoundary_apply

L60 ↗

FoxDifferential.residueFreeGroupFoxBoundary_apply

Documentation

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

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
section FiniteBasis
variable [Fintype X]
omit [DecidableEq X] in

Lean source · statement

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)

theorem

residueFreeGroupFoxBoundary_single

L73 ↗

FoxDifferential.residueFreeGroupFoxBoundary_single

Documentation

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

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
section FiniteBasis
variable [Fintype X]

Lean source · statement

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

Module documentation

Fox differential: completed — residue — free group — boundary

Declarations

residueFreeGroupFoxBoundary

residueFreeGroupFoxBoundary_apply

residueFreeGroupFoxBoundary_single