Module

Universal.lean

Nyll.ProCGroups.FoxDifferential.Discrete.DifferentialModule.Universal

14 declarations indexed from sourceView source ↗

Module documentation

Fox differential: discrete — differential module — universal

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.

Imports1

Nyll.ProCGroups.FoxDifferential.Discrete.DifferentialModule.Basic

Imported by3

abbrev

DifferentialHom

L35 ↗

FoxDifferential.DifferentialHom

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]

Lean source · statement

abbrev DifferentialHom (ψ : G →* H) (A : Type*) [AddCommGroup A] [Module (GroupRing H) A]

def

liftLinear

L39 ↗

FoxDifferential.liftLinear

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]

Lean source · statement

def liftLinear (δ : G → A) : DifferentialPreModule H G →ₗ[GroupRing H] A

theorem

liftLinear_single

L45 ↗

FoxDifferential.liftLinear_single

Documentation

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

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]
omit [Group G] in

Lean source · statement

theorem liftLinear_single (δ : G → A) (g : G) (r : GroupRing H) :
    liftLinear δ (Finsupp.single g r) = r • δ g

theorem

differentialHomLiftLinear_relationElement

L50 ↗

FoxDifferential.differentialHomLiftLinear_relationElement

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]

Lean source · statement

theorem differentialHomLiftLinear_relationElement
    (ψ : G →* H) (δ : DifferentialHom ψ A) (g₁ g₂ : G) :
    liftLinear δ (relationElement ψ g₁ g₂) = 0

theorem

differentialHomRelationSubmodule_le_ker

L62 ↗

FoxDifferential.differentialHomRelationSubmodule_le_ker

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]

Lean source · statement

theorem differentialHomRelationSubmodule_le_ker
    (ψ : G →* H) (δ : DifferentialHom ψ A) :
    relationSubmodule ψ ≤ LinearMap.ker (liftLinear δ)

def

differentialModuleLift

L74 ↗

FoxDifferential.differentialModuleLift

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]

Lean source · statement

def differentialModuleLift (ψ : G →* H) (δ : DifferentialHom ψ A) :
    DifferentialModule ψ →ₗ[GroupRing H] A

theorem

differentialModuleLift_d

L81 ↗

FoxDifferential.differentialModuleLift_d

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]

Lean source · statement

theorem differentialModuleLift_d (ψ : G →* H) (δ : DifferentialHom ψ A) (g : G) :
    differentialModuleLift ψ δ (universalDifferential ψ g) = δ g

theorem

hom_ext

L95 ↗

FoxDifferential.hom_ext

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]

Lean source · statement

theorem hom_ext (ψ : G →* H) {f g : DifferentialModule ψ →ₗ[GroupRing H] A}
    (hfg : ∀ g', f (universalDifferential ψ g') = g (universalDifferential ψ g')) : f = g

theorem

differentialModuleLift_unique

L112 ↗

FoxDifferential.differentialModuleLift_unique

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]

Lean source · statement

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

theorem

existsUnique_differentialModuleLift

L122 ↗

FoxDifferential.existsUnique_differentialModuleLift

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]

Lean source · statement

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

def

differentialHomOfLinearMap

L133 ↗

FoxDifferential.differentialHomOfLinearMap

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]

Lean source · full declaration

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]

theorem

differentialHomOfLinearMap_apply

L147 ↗

FoxDifferential.differentialHomOfLinearMap_apply

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]

Lean source · statement

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

def

differentialHomEquivLinearMap

L156 ↗

FoxDifferential.differentialHomEquivLinearMap

Documentation

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}\).

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]

Lean source · full declaration

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

theorem

differentialHomEquivLinearMap_eq_generic

L174 ↗

FoxDifferential.differentialHomEquivLinearMap_eq_generic

Documentation

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

Source context 5 commands

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

namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]

Lean source · statement

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

Module documentation

Fox differential: discrete — differential module — universal

Declarations