ProCGroups.FoxDifferential.Discrete.DifferentialModule.Basic
The principal declarations in this module are:
GroupRingThe integral group ring \(\mathbb{Z}[H]\), realized as a monoid algebra. -groupRingMapA group homomorphism induces the corresponding group-ring map. -groupRingMap_ofThe induced group-ring map sends monomials to monomials. -groupRingMap_singleThe induced group-ring map sends Finsupp.single basis terms along the group map.
imports
- ProCGroups.FoxDifferential.Common.CrossedDifferentialModule
- Mathlib.Algebra.MonoidAlgebra.MapDomain
abbrev GroupRing (H : Type*) : Type _ := MonoidAlgebra ℤ HThe integral group ring \(\mathbb{Z}[H]\), realized as a monoid algebra.
def groupRingMap {H K : Type*} [Group H] [Group K] (φ : H →* K) :
GroupRing H →+* GroupRing K :=
MonoidAlgebra.mapDomainRingHom ℤ φA group homomorphism induces the corresponding group-ring map.
@[simp]
theorem groupRingMap_of {H K : Type*} [Group H] [Group K]
(φ : H →* K) (h : H) :
groupRingMap φ (MonoidAlgebra.of ℤ H h) =
MonoidAlgebra.of ℤ K (φ h)The induced group-ring map sends monomials to monomials.
Show Lean proof
by
change
MonoidAlgebra.mapDomain φ (MonoidAlgebra.single h 1) =
MonoidAlgebra.single (φ h) 1
exact MonoidAlgebra.mapDomain_single@[simp]
theorem groupRingMap_single {H K : Type*} [Group H] [Group K]
(φ : H →* K) (h : H) (z : ℤ) :
groupRingMap φ (MonoidAlgebra.single h z : GroupRing H) =
(MonoidAlgebra.single (φ h) z : GroupRing K)The induced group-ring map sends Finsupp.single basis terms along the group map.
Show Lean proof
by
change
MonoidAlgebra.mapDomain φ (MonoidAlgebra.single h z) =
MonoidAlgebra.single (φ h) z
exact MonoidAlgebra.mapDomain_singleabbrev DifferentialPreModule (H : Type*) (G : Type*) : Type _ :=
G →₀ GroupRing HThe free \(\mathbb{Z}[H]\)-module on the underlying set of G.
@[simp]
theorem groupRing_of_one : (MonoidAlgebra.of ℤ H (1 : H) : GroupRing H) = 1The group-ring monomial attached to the group identity is the ring identity.
Show Lean proof
by
exact map_one (MonoidAlgebra.of ℤ H)def relationElement (ψ : G →* H) (g₁ g₂ : G) : DifferentialPreModule H G :=
Finsupp.single (g₁ * g₂) 1 -
(Finsupp.single g₁ 1 + (MonoidAlgebra.of ℤ H (ψ g₁)) • Finsupp.single g₂ 1)The pre-module element imposing the Fox product relation \(d(g_1g_2)=d(g_1)+\psi(g_1)\,d(g_2)\).
def relationSubmodule (ψ : G →* H) : Submodule (GroupRing H) (DifferentialPreModule H G) :=
Submodule.span (GroupRing H) (Set.range fun p : G × G => relationElement ψ p.1 p.2)The submodule generated by the Fox differential relations.
abbrev DifferentialModule (ψ : G →* H) : Type _ := DifferentialPreModule H G ⧸ relationSubmodule ψThe differential module is the universal module receiving the crossed Fox differential.
def universalDifferential (ψ : G →* H) (g : G) : DifferentialModule ψ :=
(relationSubmodule ψ).mkQ (Finsupp.single g 1)The universal differential \(G \to A_{\psi}\).
theorem relationElement_mem (ψ : G →* H) (g₁ g₂ : G) :
relationElement ψ g₁ g₂ ∈ relationSubmodule ψEvery defining Fox relation belongs to the relation submodule.
Show Lean proof
by
exact Submodule.subset_span ⟨(g₁, g₂), rfl⟩theorem universalDifferential_mul (ψ : G →* H) (g₁ g₂ : G) :
universalDifferential ψ (g₁ * g₂) =
universalDifferential ψ g₁ +
(MonoidAlgebra.of ℤ H (ψ g₁)) • universalDifferential ψ g₂The universal differential satisfies the Fox product rule.
Show Lean proof
by
have hzero : (relationSubmodule ψ).mkQ (relationElement ψ g₁ g₂) = 0 := by
exact
(Submodule.Quotient.mk_eq_zero (p := relationSubmodule ψ) (x := relationElement ψ g₁ g₂)).2
(relationElement_mem ψ g₁ g₂)
have hzero' :
universalDifferential ψ (g₁ * g₂) -
(universalDifferential ψ g₁ +
(relationSubmodule ψ).mkQ
((MonoidAlgebra.of ℤ H (ψ g₁)) • Finsupp.single g₂ 1)) = 0 := by
simpa [universalDifferential, relationElement] using hzero
have hsmul :
(relationSubmodule ψ).mkQ ((MonoidAlgebra.of ℤ H (ψ g₁)) • Finsupp.single g₂ 1) =
(MonoidAlgebra.of ℤ H (ψ g₁)) • universalDifferential ψ g₂ := by
simpa [universalDifferential, Submodule.mkQ_apply] using
(Submodule.Quotient.mk_smul (p := relationSubmodule ψ)
(r := MonoidAlgebra.of ℤ H (ψ g₁)) (x := Finsupp.single g₂ 1))
have hzero'' :
universalDifferential ψ (g₁ * g₂) -
(universalDifferential ψ g₁ +
(MonoidAlgebra.of ℤ H (ψ g₁)) • universalDifferential ψ g₂) = 0 := by
rw [hsmul] at hzero'
exact hzero'
exact sub_eq_zero.mp hzero''@[simp]
theorem universalDifferential_one (ψ : G →* H) : universalDifferential ψ (1 : G) = 0The universal differential vanishes at the group identity.
Show Lean proof
by
have h := universalDifferential_mul ψ (1 : G) (1 : G)
rw [map_one, groupRing_of_one (H := H), one_smul] at h
have h' := congrArg (fun z : DifferentialModule ψ => z - universalDifferential ψ (1 : G)) h
have h'' : 0 = universalDifferential ψ (1 : G) := by
simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h'
simpa using h''.symmtheorem universalDifferential_mul_inv_right (ψ : G →* H) (g : G) :
universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ g⁻¹ = 0The universal differentials of \(g\) and \(g^{-1}\) add to zero with the Fox twist.
Show Lean proof
by
have h : 0 = universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential
ψ g⁻¹ := by
simpa using universalDifferential_mul ψ g g⁻¹
simpa using h.symmtheorem universalDifferential_conj_of_mem_ker (ψ : G →* H) (g n : G) (hn : ψ n = 1) :
universalDifferential ψ (g * n * g⁻¹) = (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential
ψ nConjugation by \(g\) acts on the differential of a kernel element by the \(\psi(g)\) scalar.
Show Lean proof
by
calc
universalDifferential ψ (g * n * g⁻¹)
= universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ (n
* g⁻¹) := by
simpa [mul_assoc] using universalDifferential_mul ψ g (n * g⁻¹)
_ = universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) •
(universalDifferential ψ n + (MonoidAlgebra.of ℤ H (ψ n)) • universalDifferential ψ
g⁻¹) := by
rw [universalDifferential_mul]
_ = universalDifferential ψ g +
(MonoidAlgebra.of ℤ H (ψ g)) •
(universalDifferential ψ n + universalDifferential ψ g⁻¹) := by
rw [hn, groupRing_of_one (H := H), one_smul]
_ = (universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ g⁻¹) +
(MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ n := by
simp only [MonoidAlgebra.of_apply, smul_add, add_comm, add_left_comm]
_ = (0 : DifferentialModule ψ) + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ n := by
rw [universalDifferential_mul_inv_right]
_ = (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ n := by
simp only [MonoidAlgebra.of_apply, zero_add]def groupRingScalar (ψ : G →* H) : G →* GroupRing H :=
(MonoidAlgebra.of ℤ H).comp ψThe coefficient homomorphism \(G \to \mathbb{Z}[H]\) induced by \(\psi: G \to H\).
@[simp]
theorem groupRingScalar_apply (ψ : G →* H) (g : G) :
groupRingScalar ψ g = (MonoidAlgebra.of ℤ H (ψ g) : GroupRing H)The group-ring scalar associated to g is the basis element supported at ψ g.
Show Lean proof
rfl@[simp]
theorem relationElement_eq_crossedDifferentialRelationElement
(ψ : G →* H) (g₁ g₂ : G) :
relationElement ψ g₁ g₂ =
crossedDifferentialRelationElement (groupRingScalar ψ) g₁ g₂The discrete Fox relation is the coefficient-ring-agnostic crossed-differential relation for the group-ring coefficient homomorphism.
Show Lean proof
rfl@[simp]
theorem relationSubmodule_eq_crossedDifferentialRelationSubmodule (ψ : G →* H) :
relationSubmodule ψ =
crossedDifferentialRelationSubmodule (groupRingScalar ψ)The discrete Fox relation submodule agrees with the generic crossed-differential relation submodule for the group-ring coefficient homomorphism.
Show Lean proof
rfldef differentialModuleEquivCrossedDifferentialModule (ψ : G →* H) :
DifferentialModule ψ ≃ₗ[GroupRing H]
CrossedDifferentialModule (groupRingScalar ψ) :=
LinearEquiv.refl _ _The discrete universal differential module is linearly equivalent to the generic universal crossed-differential module for the group-ring coefficient homomorphism.
def crossedDifferentialModuleEquivDifferentialModule (ψ : G →* H) :
CrossedDifferentialModule (groupRingScalar ψ) ≃ₗ[GroupRing H]
DifferentialModule ψ :=
(differentialModuleEquivCrossedDifferentialModule ψ).symmThe generic universal crossed-differential module for the group-ring scalar homomorphism associated to \(\psi\) is linearly equivalent to the discrete universal differential module \(A_{\psi}\).
@[simp]
theorem differentialModuleEquivCrossedDifferentialModule_d
(ψ : G →* H) (g : G) :
differentialModuleEquivCrossedDifferentialModule ψ (universalDifferential ψ g) =
universalCrossedDifferential (groupRingScalar ψ) gThe discrete universal differential is the generic universal crossed differential under the canonical linear equivalence.
Show Lean proof
rfl@[simp]
theorem crossedDifferentialModuleEquivDifferentialModule_universal
(ψ : G →* H) (g : G) :
crossedDifferentialModuleEquivDifferentialModule ψ
(universalCrossedDifferential (groupRingScalar ψ) g) =
universalDifferential ψ gThe generic universal crossed differential maps back to the discrete universal differential under the canonical linear equivalence.
Show Lean proof
rfl