ProCGroups.FoxDifferential.Common.CrossedDifferentialModule

20 Theorems | 11 Definitions | 2 Abbreviations

The principal declarations in this module are:

CrossedDifferentialPreModule The free \(R\)-module on the underlying set of a group \(G\). - crossedDifferentialRelationElement The universal crossed-differential relation \(d(g_1g_2) = d(g_1) + \mathrm{coeff}(g_1) \cdot d(g_2)\) in the free pre-module. - crossedDifferentialRelationElement_mem Every defining crossed-differential relation belongs to the relation submodule. - universalCrossedDifferential_mul The universal crossed differential satisfies the crossed product rule.

imports

ProCGroups.FoxDifferential.Common.CrossedDifferential
Mathlib.Algebra.MonoidAlgebra.Basic
Mathlib.LinearAlgebra.Finsupp.LinearCombination
Mathlib.LinearAlgebra.Quotient.Basic

Imported by

Abbreviation FoxDifferential.CrossedDifferentialPreModule

abbrev CrossedDifferentialPreModule (R G : Type*) [Ring R] : Type _ :=
  G →₀ R

The free \(R\)-module on the underlying set of a group \(G\).

Definition FoxDifferential.crossedDifferentialRelationElement

def crossedDifferentialRelationElement (coeff : G →* R) (g₁ g₂ : G) :
    CrossedDifferentialPreModule R G :=
  Finsupp.single (g₁ * g₂) 1 -
    (Finsupp.single g₁ 1 + coeff g₁ • Finsupp.single g₂ 1)

The universal crossed-differential relation \(d(g_1g_2) = d(g_1) + \mathrm{coeff}(g_1) \cdot d(g_2)\) in the free pre-module.

Definition FoxDifferential.crossedDifferentialRelationSubmodule

def crossedDifferentialRelationSubmodule (coeff : G →* R) :
    Submodule R (CrossedDifferentialPreModule R G) :=
  Submodule.span R (Set.range fun p : G × G =>
    crossedDifferentialRelationElement coeff p.1 p.2)

The submodule generated by all universal crossed-differential relations.

Abbreviation FoxDifferential.CrossedDifferentialModule

abbrev CrossedDifferentialModule (coeff : G →* R) : Type _ :=
  CrossedDifferentialPreModule R G ⧸ crossedDifferentialRelationSubmodule coeff

The universal module representing crossed differentials with coefficient homomorphism \(\mathrm{coeff}:G\to R\), viewed multiplicatively.

Definition FoxDifferential.universalCrossedDifferential

def universalCrossedDifferential (coeff : G →* R) (g : G) :
    CrossedDifferentialModule coeff :=
  (crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g 1)

The universal crossed differential d_coeff : G -> CrossedDifferentialModule coeff.

Theorem FoxDifferential.crossedDifferentialRelationElement_mem

theorem crossedDifferentialRelationElement_mem (coeff : G →* R) (g₁ g₂ : G) :
    crossedDifferentialRelationElement coeff g₁ g₂ ∈
      crossedDifferentialRelationSubmodule coeff

Every defining crossed-differential relation belongs to the relation submodule.

Show Lean proof

Theorem FoxDifferential.universalCrossedDifferential_mul

theorem universalCrossedDifferential_mul (coeff : G →* R) (g₁ g₂ : G) :
    universalCrossedDifferential coeff (g₁ * g₂) =
      universalCrossedDifferential coeff g₁ +
        coeff g₁ • universalCrossedDifferential coeff g₂

The universal crossed differential satisfies the crossed product rule.

Show Lean proof

Definition FoxDifferential.universalCrossedHom

def universalCrossedHom (coeff : G →* R) :
    ScalarCrossedHom coeff (CrossedDifferentialModule coeff) where
  toFun := universalCrossedDifferential coeff
  map_mul' := by
    intro g₁ g₂
    change universalCrossedDifferential coeff (g₁ * g₂) =
      universalCrossedDifferential coeff g₁ +
        coeff g₁ • universalCrossedDifferential coeff g₂
    exact universalCrossedDifferential_mul coeff g₁ g₂

The universal crossed differential \(d_{\mathrm{coeff}} : G \to \mathrm{CrossedDifferentialModule}(\mathrm{coeff})\).

Theorem FoxDifferential.universalCrossedDifferential_one

@[simp]
theorem universalCrossedDifferential_one (coeff : G →* R) :
    universalCrossedDifferential coeff (1 : G) = 0

The universal crossed differential vanishes at the identity.

Show Lean proof

Definition FoxDifferential.crossedDifferentialModuleLiftLinear

def crossedDifferentialModuleLiftLinear (delta : G → A) :
    CrossedDifferentialPreModule R G →ₗ[R] A :=
  Finsupp.linearCombination R delta

The linear extension of a map out of G to the free crossed-differential pre-module.

Theorem FoxDifferential.crossedDifferentialModuleLiftLinear_single

omit [Group G] in
@[simp]
theorem crossedDifferentialModuleLiftLinear_single (delta : G → A) (g : G) (r : R) :
    crossedDifferentialModuleLiftLinear (R := R) delta (Finsupp.single g r) = r • delta g

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

Show Lean proof

Theorem FoxDifferential.crossedHomModuleLiftLinear_relationElement

theorem crossedHomModuleLiftLinear_relationElement
    (coeff : G →* R) (delta : ScalarCrossedHom coeff A) (g₁ g₂ : G) :
    crossedDifferentialModuleLiftLinear (R := R) delta
      (crossedDifferentialRelationElement coeff g₁ g₂) = 0

A crossed differential kills each defining universal relation.

Show Lean proof

Theorem FoxDifferential.crossedHomRelationSubmodule_le_ker

theorem crossedHomRelationSubmodule_le_ker
    (coeff : G →* R) (delta : ScalarCrossedHom coeff A) :
    crossedDifferentialRelationSubmodule coeff ≤
      LinearMap.ker (crossedDifferentialModuleLiftLinear (R := R) delta)

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

Show Lean proof

Definition FoxDifferential.crossedHomModuleLift

def crossedHomModuleLift
    (coeff : G →* R) (delta : ScalarCrossedHom coeff A) :
    CrossedDifferentialModule coeff →ₗ[R] A :=
  (crossedDifferentialRelationSubmodule coeff).liftQ
    (crossedDifferentialModuleLiftLinear (R := R) delta)
    (crossedHomRelationSubmodule_le_ker (A := A) coeff delta)

The universal linear map induced by a crossed differential.

Theorem FoxDifferential.crossedHomModuleLift_mkQ

theorem crossedHomModuleLift_mkQ
    (coeff : G →* R) (delta : ScalarCrossedHom coeff A)
    (x : CrossedDifferentialPreModule R G) :
    crossedHomModuleLift (A := A) coeff delta
        ((crossedDifferentialRelationSubmodule coeff).mkQ x) =
      crossedDifferentialModuleLiftLinear (R := R) delta x

The universal lift evaluated on a quotient representative is the finite linear combination of the prescribed crossed differential on that representative.

Show Lean proof

Theorem FoxDifferential.crossedHomModuleLift_universal

@[simp]
theorem crossedHomModuleLift_universal
    (coeff : G →* R) (delta : ScalarCrossedHom coeff A) (g : G) :
    crossedHomModuleLift (A := A) coeff delta (universalCrossedDifferential coeff g) = delta g

The universal lift evaluates on \(d_{\mathrm{coeff}}(g)\) as the original crossed differential.

Show Lean proof

Theorem FoxDifferential.crossedDifferentialModuleHom_ext

@[ext]
theorem crossedDifferentialModuleHom_ext
    (coeff : G →* R) {f h : CrossedDifferentialModule coeff →ₗ[R] A}
    (hfh : ∀ g, f (universalCrossedDifferential coeff g) =
      h (universalCrossedDifferential coeff g)) :
    f = h

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

Show Lean proof

Theorem FoxDifferential.crossedHomModuleLift_unique

theorem crossedHomModuleLift_unique
    (coeff : G →* R) (delta : ScalarCrossedHom coeff A)
    (f : CrossedDifferentialModule coeff →ₗ[R] A)
    (hf : ∀ g, f (universalCrossedDifferential coeff g) = delta g) :
    f = crossedHomModuleLift (A := A) coeff delta

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

Show Lean proof

Theorem FoxDifferential.existsUnique_crossedHomModuleLift

theorem existsUnique_crossedHomModuleLift
    (coeff : G →* R) (delta : ScalarCrossedHom coeff A) :
    ∃! f : CrossedDifferentialModule coeff →ₗ[R] A,
      ∀ g, f (universalCrossedDifferential coeff g) = delta g

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

Show Lean proof

Definition FoxDifferential.crossedHomOfModuleLinearMap

def crossedHomOfModuleLinearMap
    (coeff : G →* R) (f : CrossedDifferentialModule coeff →ₗ[R] A) :
    ScalarCrossedHom coeff A where
  toFun g := f (universalCrossedDifferential coeff g)
  map_mul' := by
    intro g₁ g₂
    change f (universalCrossedDifferential coeff (g₁ * g₂)) =
      f (universalCrossedDifferential coeff g₁) +
        coeff g₁ • f (universalCrossedDifferential coeff g₂)
    rw [universalCrossedDifferential_mul, map_add, map_smul]

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

Theorem FoxDifferential.crossedHomOfModuleLinearMap_apply

@[simp]
theorem crossedHomOfModuleLinearMap_apply
    (coeff : G →* R) (f : CrossedDifferentialModule coeff →ₗ[R] A) (g : G) :
    crossedHomOfModuleLinearMap (A := A) coeff f g =
      f (universalCrossedDifferential coeff g)

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

Show Lean proof

Definition FoxDifferential.crossedHomModuleEquivLinearMap

def crossedHomModuleEquivLinearMap (coeff : G →* R) :
    ScalarCrossedHom coeff A ≃ (CrossedDifferentialModule coeff →ₗ[R] A) where
  toFun delta := crossedHomModuleLift (A := A) coeff delta
  invFun f := crossedHomOfModuleLinearMap (A := A) coeff f
  left_inv delta := by
    apply CrossedHom.ext
    intro g
    change crossedHomModuleLift (A := A) coeff delta
      (universalCrossedDifferential coeff g) = delta g
    exact crossedHomModuleLift_universal (A := A) coeff delta g
  right_inv f := by
    apply crossedDifferentialModuleHom_ext coeff
    intro g
    change crossedHomModuleLift (A := A) coeff
      (crossedHomOfModuleLinearMap (A := A) coeff f)
        (universalCrossedDifferential coeff g) =
      f (universalCrossedDifferential coeff g)
    exact crossedHomModuleLift_universal (A := A) coeff
      (crossedHomOfModuleLinearMap (A := A) coeff f) g

Crossed differentials \(G \to A\) with coefficient homomorphism \(\mathrm{coeff}:G \to R\) are represented by \(R\)-linear maps out of the universal module \(\mathrm{CrossedDifferentialModule}\,\mathrm{coeff}\).

Definition FoxDifferential.monoidAlgebraToIdentityCrossedDifferentialModule

def monoidAlgebraToIdentityCrossedDifferentialModule :
    MonoidAlgebra S G →ₗ[S]
      CrossedDifferentialModule (MonoidAlgebra.of S G) :=
  (Finsupp.linearCombination S
    (fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g)).comp
      (MonoidAlgebra.coeffLinearEquiv S).toLinearMap

The S-linear map from a group algebra to the identity crossed-differential module sending \([g]\) to the universal differential d g.

Theorem FoxDifferential.monoidAlgebraToIdentityCrossedDifferentialModule_single

@[simp]
theorem monoidAlgebraToIdentityCrossedDifferentialModule_single (g : G) (a : S) :
    monoidAlgebraToIdentityCrossedDifferentialModule
        (MonoidAlgebra.single g a : MonoidAlgebra S G) =
      a • universalCrossedDifferential (MonoidAlgebra.of S G) g

A group-algebra basis term maps to its coefficient times the corresponding universal differential.

Show Lean proof

Theorem FoxDifferential.monoidAlgebraToIdentityCrossedDifferentialModule_mul_sub_one

theorem monoidAlgebraToIdentityCrossedDifferentialModule_mul_sub_one
    (a : MonoidAlgebra S G) (g : G) :
    monoidAlgebraToIdentityCrossedDifferentialModule
        (a * (MonoidAlgebra.of S G g - 1)) =
      a • universalCrossedDifferential (MonoidAlgebra.of S G) g

The linear map from the group algebra to the identity crossed-differential module sends \(a([g]-1)\) to \(a\) acting on the universal differential of \(g\).

Show Lean proof

Definition FoxDifferential.identityGroupAlgebraCrossedHom

def identityGroupAlgebraCrossedHom :
    ScalarCrossedHom (MonoidAlgebra.of S G) (MonoidAlgebra S G) where
  toFun g := MonoidAlgebra.of S G g - 1
  map_mul' := by
    intro g h
    change MonoidAlgebra.of S G (g * h) - 1 =
      (MonoidAlgebra.of S G g - 1) +
        MonoidAlgebra.of S G g • (MonoidAlgebra.of S G h - 1)
    simp only [map_mul, MonoidAlgebra.of_apply,
      MonoidAlgebra.single_mul_single, mul_one, sub_eq_add_neg, smul_eq_mul, mul_add,
      mul_neg, add_comm, add_assoc, neg_add_cancel_left]

The group-algebra boundary g ↦ [g] - 1, bundled as a scalar crossed homomorphism.

Theorem FoxDifferential.identityGroupAlgebraCrossedHom_apply

@[simp]
theorem identityGroupAlgebraCrossedHom_apply (g : G) :
    identityGroupAlgebraCrossedHom (S := S) (G := G) g =
      MonoidAlgebra.of S G g - 1

The identity-coefficient crossed homomorphism sends a group element to its group-like term minus one.

Show Lean proof

Definition FoxDifferential.identityCrossedDifferentialBoundary

def identityCrossedDifferentialBoundary :
    CrossedDifferentialModule (MonoidAlgebra.of S G) →ₗ[MonoidAlgebra S G]
      MonoidAlgebra S G :=
  crossedHomModuleLift
    (A := MonoidAlgebra S G) (MonoidAlgebra.of S G)
    (identityGroupAlgebraCrossedHom (S := S) (G := G))

The identity crossed-differential boundary sends \(d g\) to \([g] - 1\) over a group algebra.

Theorem FoxDifferential.identityCrossedDifferentialBoundary_universal

@[simp]
theorem identityCrossedDifferentialBoundary_universal (g : G) :
    identityCrossedDifferentialBoundary
        (universalCrossedDifferential (MonoidAlgebra.of S G) g) =
      MonoidAlgebra.of S G g - 1

The identity crossed-differential boundary sends the universal differential at \(g\) to the group-algebra element \([g]-1\).

Show Lean proof

Theorem FoxDifferential.monoidAlgebraToIdentityCrossedDifferentialModule_comp_identityBoundary_mkQ

theorem monoidAlgebraToIdentityCrossedDifferentialModule_comp_identityBoundary_mkQ
    (x : CrossedDifferentialPreModule (MonoidAlgebra S G) G) :
    monoidAlgebraToIdentityCrossedDifferentialModule
        (crossedDifferentialModuleLiftLinear
          (R := MonoidAlgebra S G)
          (fun g : G => MonoidAlgebra.of S G g - 1) x) =
      (crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ x

Composing the identity-boundary map with the monoid-algebra comparison has the stated value on quotient generators.

Show Lean proof

Theorem FoxDifferential.idCrossedDiffBoundary_monoidAlgebraToModule

theorem idCrossedDiffBoundary_monoidAlgebraToModule
    (a : MonoidAlgebra S G) :
    identityCrossedDifferentialBoundary
        (monoidAlgebraToIdentityCrossedDifferentialModule (S := S) (G := G) a) =
      a -
        MonoidAlgebra.single (1 : G)
          ((MonoidAlgebra.lift S S G (1 : G →* S)) a)

The boundary of the additive lift \(\sum a_g [g] \mapsto \sum a_g d g\) is the augmentation-zero part of the group-algebra element.

Show Lean proof

Theorem FoxDifferential.idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero

theorem idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero
    {a : MonoidAlgebra S G}
    (ha : (MonoidAlgebra.lift S S G (1 : G →* S)) a = 0) :
    identityCrossedDifferentialBoundary
        (monoidAlgebraToIdentityCrossedDifferentialModule (S := S) (G := G) a) = a

On the augmentation ideal, the additive lift \(\sum a_g [g] \mapsto \sum a_g d g\) is a right inverse to the identity crossed-differential boundary.

Show Lean proof

Theorem FoxDifferential.identityCrossedDifferentialBoundary_injective

theorem identityCrossedDifferentialBoundary_injective :
    Function.Injective (identityCrossedDifferentialBoundary (S := S) (G := G))

For the identity coefficient map into a group algebra, the boundary map sending \(d g\) to \([g]

1\) is injective.

Show Lean proof

ProCGroups.FoxDifferential.Common.CrossedDifferentialModule

Declarations