ProCGroups.FoxDifferential.Completed.Residue.Core

7 Theorems | 6 Definitions | 2 Abbreviations

The principal declarations in this module are:

ResidueGroupRing The residue group ring \((\mathbb{Z}/n\mathbb{Z})[H]\). - residueGroupRingScalar The coefficient homomorphism \(G \to (\mathbb{Z}/n\mathbb{Z})[H]\) induced by a group homomorphism \(\psi: G \to H\). - residueGroupRingScalar_apply The residue coefficient homomorphism sends a group element to the residue group-ring basis element of its image. - residueGroupRingBoundary_one The residue Fox boundary vanishes at the identity.

imports

Imported by

Abbreviation FoxDifferential.ResidueGroupRing

abbrev ResidueGroupRing (n : ℕ) (H : Type*) : Type _ :=
  ModNCompletedGroupRing n H

The residue group ring \((\mathbb{Z}/n\mathbb{Z})[H]\).

Definition FoxDifferential.residueGroupRingScalar

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 FoxDifferential.residueGroupRingScalar_apply

@[simp]
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 Lean proof

Abbreviation FoxDifferential.ResidueDifferentialModule

abbrev ResidueDifferentialModule (n : ℕ) (ψ : G →* H) : Type _ :=
  CrossedDifferentialModule (residueGroupRingScalar n ψ)

The residue universal differential module attached to \(\psi : G \to H\).

Definition FoxDifferential.residueUniversalDifferential

def residueUniversalDifferential (n : ℕ) (ψ : G →* H) :
    ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueDifferentialModule n ψ) :=
  universalCrossedHom (residueGroupRingScalar n ψ)

The universal residue crossed homomorphism.

Definition FoxDifferential.residueGroupRingBoundary

def residueGroupRingBoundary (n : ℕ) (ψ : G →* H) :
    ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueGroupRing n H) where
  toFun g := MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ g) - 1
  map_mul' := by
    intro g h
    simp only [scalarCrossedAction_apply, 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]

The residue Fox boundary \(g \mapsto [\psi(g)] - 1\), bundled as a crossed homomorphism.

Theorem FoxDifferential.residueGroupRingBoundary_one

@[simp]
theorem residueGroupRingBoundary_one (n : ℕ) (ψ : G →* H) :
    residueGroupRingBoundary n ψ (1 : G) = 0

The residue Fox boundary vanishes at the identity.

Show Lean proof

Definition FoxDifferential.residueDifferentialModuleLift

def residueDifferentialModuleLift
    (ψ : G →* H)
    (delta : ScalarCrossedHom (residueGroupRingScalar n ψ) A) :
    ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A :=
  crossedHomModuleLift (A := A) (residueGroupRingScalar n ψ) delta

The universal linear map induced by a residue crossed differential.

Theorem FoxDifferential.residueDifferentialModuleLift_universal

@[simp]
theorem residueDifferentialModuleLift_universal
    (ψ : G →* H) (delta : ScalarCrossedHom (residueGroupRingScalar n ψ) A)
    (g : G) :
    residueDifferentialModuleLift (A := A) n ψ delta
        (residueUniversalDifferential n ψ g) =
      delta g

The residue universal lift evaluates on the universal differential as the original crossed differential.

Show Lean proof

Theorem FoxDifferential.residueDifferentialModuleHom_ext

@[ext]
theorem residueDifferentialModuleHom_ext
    (ψ : G →* H)
    {f h : ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A}
    (hfh : ∀ g, f (residueUniversalDifferential n ψ g) =
      h (residueUniversalDifferential n ψ g)) :
    f = h

Linear maps out of the residue universal module are equal when they agree on universal residue differentials.

Show Lean proof

Theorem FoxDifferential.existsUnique_residueDifferentialModuleLift

theorem existsUnique_residueDifferentialModuleLift
    (ψ : G →* H) (delta : ScalarCrossedHom (residueGroupRingScalar n ψ) A) :
    ∃! f : ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A,
      ∀ g, f (residueUniversalDifferential n ψ g) = delta g

Existence and uniqueness of the linear map representing a residue crossed differential.

Show Lean proof

Definition FoxDifferential.residueCrossedHomEquivLinearMap

def residueCrossedHomEquivLinearMap (ψ : G →* H) :
    ScalarCrossedHom (residueGroupRingScalar n ψ) A ≃
      (ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A) :=
  crossedHomModuleEquivLinearMap (A := A) (residueGroupRingScalar n ψ)

Residue crossed homomorphisms are represented by the corresponding universal residue module.

Definition FoxDifferential.residueToGroupRing

def residueToGroupRing (ψ : G →* H) :
    ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] ResidueGroupRing n H :=
  residueDifferentialModuleLift (A := ResidueGroupRing n H) n ψ
    (residueGroupRingBoundary n ψ)

The universal residue Fox boundary map from the residue differential module to the residue group ring.

Theorem FoxDifferential.residueToGroupRing_universal

@[simp]
theorem residueToGroupRing_universal (ψ : G →* H) (g : G) :
    residueToGroupRing n ψ (residueUniversalDifferential n ψ g) =
      residueGroupRingBoundary n ψ g

The universal residue Fox boundary sends \(d g\) to \([\psi(g)] - 1\).

Show Lean proof

Theorem FoxDifferential.existsUnique_residueToGroupRing

theorem existsUnique_residueToGroupRing (ψ : G →* H) :
    ∃! f : ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] ResidueGroupRing n H,
      ∀ g, f (residueUniversalDifferential n ψ g) =
        residueGroupRingBoundary n ψ g

Existence and uniqueness of the universal residue Fox boundary map.

Show Lean proof

ProCGroups.FoxDifferential.Completed.Residue.Core

Declarations