Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Discrete.DifferentialModule.Universal
ProCGroups/FoxDifferential/Discrete/DifferentialModule/Universal

ProCGroups.FoxDifferential.Discrete.DifferentialModule.Universal

9 Theorems | 4 Definitions | 1 Abbreviation

The principal declarations in this module are:

  • DifferentialHom A \(\psi\)-differential map is a map satisfying the Fox Leibniz rule. - liftLinear The linear map out of the free pre-module determined by \(\delta\). - liftLinear_single The linear extension of a map evaluates on a single basis vector by scalar multiplication. - differentialHomLiftLinear_relationElement A crossed differential kills each defining relation of the universal differential module.
import
Imported by

Declarations

Abbreviation FoxDifferential.DifferentialHom 
abbrev DifferentialHom (ψ : G →* H) (A : Type*) [AddCommGroup A] [Module (GroupRing H) A] :=
  ScalarCrossedHom (groupRingScalar ψ) A

A \(\psi\)-differential map is a map satisfying the Fox Leibniz rule.

Definition FoxDifferential.liftLinear 
def liftLinear (δ : G → A) : DifferentialPreModule H G →ₗ[GroupRing H] A :=
  Finsupp.linearCombination (GroupRing H) δ

The linear map out of the free pre-module determined by \(\delta\).

Theorem FoxDifferential.liftLinear_single 
omit [Group G] in
@[simp]
theorem liftLinear_single (δ : G → A) (g : G) (r : GroupRing H) :
    liftLinear δ (Finsupp.single g r) = r • δ g

The linear extension of a map evaluates on a single basis vector by scalar multiplication.

Show Lean proof
Theorem FoxDifferential.differentialHomLiftLinear_relationElement 
theorem differentialHomLiftLinear_relationElement
    (ψ : G →* H) (δ : DifferentialHom ψ A) (g₁ g₂ : G) :
    liftLinear δ (relationElement ψ g₁ g₂) = 0

A crossed differential kills each defining relation of the universal differential module.

Show Lean proof
Theorem FoxDifferential.differentialHomRelationSubmodule_le_ker 
theorem differentialHomRelationSubmodule_le_ker
    (ψ : G →* H) (δ : DifferentialHom ψ A) :
    relationSubmodule ψ ≤ LinearMap.ker (liftLinear δ)

The relation submodule is contained in the kernel of the linear extension of a crossed differential.

Show Lean proof
Definition FoxDifferential.differentialModuleLift 
def differentialModuleLift (ψ : G →* H) (δ : DifferentialHom ψ A) :
    DifferentialModule ψ →ₗ[GroupRing H] A :=
  (relationSubmodule ψ).liftQ (liftLinear δ)
    (differentialHomRelationSubmodule_le_ker (A := A) ψ δ)

A crossed differential factors uniquely through the universal differential module as a linear map.

Theorem FoxDifferential.differentialModuleLift_d 
@[simp]
theorem differentialModuleLift_d (ψ : G →* H) (δ : DifferentialHom ψ A) (g : G) :
    differentialModuleLift ψ δ (universalDifferential ψ g) = δ g

The universal lift evaluates on universalDifferential g as the original crossed differential.

Show Lean proof
Theorem FoxDifferential.hom_ext 
@[ext]
theorem hom_ext (ψ : G →* H) {f g : DifferentialModule ψ →ₗ[GroupRing H] A}
    (hfg : ∀ g', f (universalDifferential ψ g') = g (universalDifferential ψ g')) : f = g

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

Show Lean proof
Theorem FoxDifferential.differentialModuleLift_unique 
theorem differentialModuleLift_unique
    (ψ : G →* H) (δ : DifferentialHom ψ A)
    (f : DifferentialModule ψ →ₗ[GroupRing H] A)
    (hf : ∀ g, f (universalDifferential ψ g) = δ g) :
    f = differentialModuleLift (A := A) ψ δ

The universal lift is the unique linear map with prescribed values on universal differentials.

Show Lean proof
Theorem FoxDifferential.existsUnique_differentialModuleLift 
theorem existsUnique_differentialModuleLift
    (ψ : G →* H) (δ : DifferentialHom ψ A) :
    ∃! f : DifferentialModule ψ →ₗ[GroupRing H] A,
      ∀ g, f (universalDifferential ψ g) = δ g

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

Show Lean proof
Definition FoxDifferential.differentialHomOfLinearMap 
def differentialHomOfLinearMap
    (ψ : G →* H) (f : DifferentialModule ψ →ₗ[GroupRing H] A) : DifferentialHom ψ A where
  toFun g := f (universalDifferential ψ g)
  map_mul' := by
    intro g₁ g₂
    change f (universalDifferential ψ (g₁ * g₂)) =
      f (universalDifferential ψ g₁) +
        (MonoidAlgebra.of ℤ H (ψ g₁) : GroupRing H) •
          f (universalDifferential ψ g₂)
    rw [universalDifferential_mul, map_add, map_smul]

The crossed differential induced by a linear map out of the universal differential module.

Theorem FoxDifferential.differentialHomOfLinearMap_apply 
@[simp]
theorem differentialHomOfLinearMap_apply
    (ψ : G →* H) (f : DifferentialModule ψ →ₗ[GroupRing H] A) (g : G) :
    differentialHomOfLinearMap (A := A) ψ f g = f (universalDifferential ψ g)

The differential induced by a linear map evaluates that map on the universal differential.

Show Lean proof
Definition FoxDifferential.differentialHomEquivLinearMap 
def differentialHomEquivLinearMap (ψ : G →* H) :
    DifferentialHom ψ A ≃ (DifferentialModule ψ →ₗ[GroupRing H] A) where
  toFun δ := differentialModuleLift (A := A) ψ δ
  invFun f := differentialHomOfLinearMap (A := A) ψ f
  left_inv δ := by
    apply CrossedHom.ext
    intro g
    exact differentialModuleLift_d (A := A) ψ δ g
  right_inv f := by
    apply hom_ext ψ
    intro g
    exact differentialModuleLift_d (A := A) ψ
      (differentialHomOfLinearMap (A := A) ψ f) g

Discrete Fox crossed differentials \(G \to A\) with respect to \(\psi: G \to H\) are represented by \(\mathbb{Z}[H]\)-linear maps out of the universal differential module \(A_{\psi}\).

Theorem FoxDifferential.differentialHomEquivLinearMap_eq_generic 
theorem differentialHomEquivLinearMap_eq_generic
    (ψ : G →* H) (δ : DifferentialHom ψ A) :
    differentialHomEquivLinearMap (A := A) ψ δ =
      (crossedHomModuleEquivLinearMap
        (A := A) (groupRingScalar ψ) δ).comp
        (differentialModuleEquivCrossedDifferentialModule ψ).toLinearMap

The compatibility between the discrete representation theorem and the generic crossed-differential-module representation theorem.

Show Lean proof