FoxDifferential.Completed.Residue.Core
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
import
abbrev ResidueGroupRing (n : ℕ) (H : Type*) : Type _ :=
ModNCompletedGroupRing n HThe residue group ring \((\mathbb{Z}/n\mathbb{Z})[H]\).
def residueGroupRingScalar (n : ℕ) (ψ : G →* H) : G →* ResidueGroupRing n H :=
(MonoidAlgebra.of (ModNCompletedCoeff n) H).comp ψThe coefficient homomorphism \(G \to (\mathbb{Z}/n\mathbb{Z})[H]\) induced by a group homomorphism \(\psi: G \to H\).
theorem residueGroupRingScalar_apply (n : ℕ) (ψ : G →* H) (g : G) :
residueGroupRingScalar n ψ g =
(MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ g) : ResidueGroupRing n H)The residue coefficient homomorphism sends a group element to the residue group-ring basis element of its image.
Show proof
rflProof. Work in the residue coefficient ring and the corresponding finite quotient group algebra. The residue Fox derivative and boundary are determined by their generator values and the crossed-differential rule, while quotient and coefficient maps act on supports and coefficients at the residue stage. Fundamental formulas, naturality, and component identities are checked on group-like generators and then extended by linearity and finite support.
□abbrev ResidueDifferentialModule (n : ℕ) (ψ : G →* H) : Type _ :=
CrossedDifferentialModule (residueGroupRingScalar n ψ)The residue universal differential module attached to \(\psi : G \to H\).
def residueUniversalDifferential (n : ℕ) (ψ : G →* H) (g : G) :
ResidueDifferentialModule n ψ :=
universalCrossedDifferential (residueGroupRingScalar n ψ) gThe universal residue crossed differential.
theorem residueUniversalDifferential_isCrossedDifferential (n : ℕ) (ψ : G →* H) :
IsCrossedDifferential
(residueGroupRingScalar n ψ) (residueUniversalDifferential n ψ)The universal residue differential is a crossed differential.
Show proof
by
exact universalCrossedDifferential_isCrossedDifferential (residueGroupRingScalar n ψ)Proof. Work in the residue coefficient ring and the corresponding finite quotient group algebra. The residue Fox derivative and boundary are determined by their generator values and the crossed-differential rule, while quotient and coefficient maps act on supports and coefficients at the residue stage. Fundamental formulas, naturality, and component identities are checked on group-like generators and then extended by linearity and finite support.
□def residueGroupRingBoundary (n : ℕ) (ψ : G →* H) (g : G) : ResidueGroupRing n H :=
MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ g) - 1The residue Fox boundary \(g \mapsto [\psi(g)] - 1\).
theorem residueGroupRingBoundary_one (n : ℕ) (ψ : G →* H) :
residueGroupRingBoundary n ψ (1 : G) = 0The residue Fox boundary vanishes at the identity.
Show proof
by
simp only [residueGroupRingBoundary, map_one, MonoidAlgebra.one_def, sub_self]Proof. Work in the residue coefficient ring and the corresponding finite quotient group algebra. The residue Fox derivative and boundary are determined by their generator values and the crossed-differential rule, while quotient and coefficient maps act on supports and coefficients at the residue stage. Fundamental formulas, naturality, and component identities are checked on group-like generators and then extended by linearity and finite support.
□theorem residueGroupRingBoundary_isCrossedDifferential (n : ℕ) (ψ : G →* H) :
IsCrossedDifferential
(residueGroupRingScalar n ψ) (residueGroupRingBoundary n ψ)The residue Fox boundary is a crossed differential.
Show proof
by
intro g h
simp only [residueGroupRingBoundary, map_mul, MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single,
mul_one, sub_eq_add_neg, add_comm, residueGroupRingScalar_apply, smul_eq_mul, mul_add, mul_neg, add_assoc,
add_neg_cancel_comm_assoc]Proof. Work in the residue coefficient ring and the corresponding finite quotient group algebra. The residue Fox derivative and boundary are determined by their generator values and the crossed-differential rule, while quotient and coefficient maps act on supports and coefficients at the residue stage. Fundamental formulas, naturality, and component identities are checked on group-like generators and then extended by linearity and finite support.
□def residueDifferentialModuleLift
(ψ : G →* H) (delta : G → A)
(hdelta : IsCrossedDifferential (residueGroupRingScalar n ψ) delta) :
ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A :=
crossedDifferentialModuleLift (A := A) (residueGroupRingScalar n ψ) delta hdeltaThe universal linear map induced by a residue crossed differential.
theorem residueDifferentialModuleLift_universal
(ψ : G →* H) (delta : G → A)
(hdelta : IsCrossedDifferential (residueGroupRingScalar n ψ) delta) (g : G) :
residueDifferentialModuleLift (A := A) n ψ delta hdelta
(residueUniversalDifferential n ψ g) =
delta gThe residue universal lift evaluates on the universal differential as the original crossed differential.
Show proof
by
exact crossedDifferentialModuleLift_universal
(A := A) (residueGroupRingScalar n ψ) delta hdelta gProof. Work in the residue coefficient ring and the corresponding finite quotient group algebra. The residue Fox derivative and boundary are determined by their generator values and the crossed-differential rule, while quotient and coefficient maps act on supports and coefficients at the residue stage. Fundamental formulas, naturality, and component identities are checked on group-like generators and then extended by linearity and finite support.
□theorem residueDifferentialModuleHom_ext
(ψ : G →* H)
{f h : ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A}
(hfh : ∀ g, f (residueUniversalDifferential n ψ g) =
h (residueUniversalDifferential n ψ g)) :
f = hLinear maps out of the residue universal module are equal when they agree on universal residue differentials.
Show proof
by
exact crossedDifferentialModuleHom_ext (A := A) (residueGroupRingScalar n ψ) hfhProof. Work in the residue coefficient ring and the corresponding finite quotient group algebra. The residue Fox derivative and boundary are determined by their generator values and the crossed-differential rule, while quotient and coefficient maps act on supports and coefficients at the residue stage. Fundamental formulas, naturality, and component identities are checked on group-like generators and then extended by linearity and finite support.
□theorem existsUnique_residueDifferentialModuleLift
(ψ : G →* H) (delta : G → A)
(hdelta : IsCrossedDifferential (residueGroupRingScalar n ψ) delta) :
∃! f : ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A,
∀ g, f (residueUniversalDifferential n ψ g) = delta gExistence and uniqueness of the linear map representing a residue crossed differential.
Show proof
by
exact existsUnique_crossedDifferentialModuleLift
(A := A) (residueGroupRingScalar n ψ) delta hdeltaProof. Work in the residue coefficient ring and the corresponding finite quotient group algebra. The residue Fox derivative and boundary are determined by their generator values and the crossed-differential rule, while quotient and coefficient maps act on supports and coefficients at the residue stage. Fundamental formulas, naturality, and component identities are checked on group-like generators and then extended by linearity and finite support.
□def residueCrossedDifferentialEquivLinearMap (ψ : G →* H) :
{delta : G → A // IsCrossedDifferential (residueGroupRingScalar n ψ) delta} ≃
(ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A) :=
crossedDifferentialModuleEquivLinearMap (A := A) (residueGroupRingScalar n ψ)Residue crossed differentials are represented by the corresponding universal residue module.
def residueToGroupRing (ψ : G →* H) :
ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] ResidueGroupRing n H :=
residueDifferentialModuleLift (A := ResidueGroupRing n H) n ψ
(residueGroupRingBoundary n ψ)
(residueGroupRingBoundary_isCrossedDifferential n ψ)The universal residue Fox boundary map from the residue differential module to the residue group ring.
theorem residueToGroupRing_universal (ψ : G →* H) (g : G) :
residueToGroupRing n ψ (residueUniversalDifferential n ψ g) =
residueGroupRingBoundary n ψ gThe universal residue Fox boundary sends \(d g\) to \([\psi(g)] - 1\).
Show proof
by
exact residueDifferentialModuleLift_universal
(A := ResidueGroupRing n H) n ψ
(residueGroupRingBoundary n ψ)
(residueGroupRingBoundary_isCrossedDifferential n ψ) gProof. Work in the residue coefficient ring and the corresponding finite quotient group algebra. The residue Fox derivative and boundary are determined by their generator values and the crossed-differential rule, while quotient and coefficient maps act on supports and coefficients at the residue stage. Fundamental formulas, naturality, and component identities are checked on group-like generators and then extended by linearity and finite support.
□theorem existsUnique_residueToGroupRing (ψ : G →* H) :
∃! f : ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] ResidueGroupRing n H,
∀ g, f (residueUniversalDifferential n ψ g) =
residueGroupRingBoundary n ψ gExistence and uniqueness of the universal residue Fox boundary map.
Show proof
by
exact existsUnique_residueDifferentialModuleLift
(A := ResidueGroupRing n H) n ψ
(residueGroupRingBoundary n ψ)
(residueGroupRingBoundary_isCrossedDifferential n ψ)Proof. Work in the residue coefficient ring and the corresponding finite quotient group algebra. The residue Fox derivative and boundary are determined by their generator values and the crossed-differential rule, while quotient and coefficient maps act on supports and coefficients at the residue stage. Fundamental formulas, naturality, and component identities are checked on group-like generators and then extended by linearity and finite support.
□