FoxDifferential.Discrete.DifferentialModule.Basic
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
import
- 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.
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 proof
by
simp only [groupRingMap, MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk,
MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 proof
by
simp only [groupRingMap, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□abbrev DifferentialPreModule (H : Type*) (G : Type*) : Type _ :=
G →₀ GroupRing HThe free \(\mathbb{Z}[H]\)-module on the underlying set of G.
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 proof
by
classical
ext a
by_cases ha : a = 1
· subst ha
simp only [MonoidAlgebra.of_apply, Finsupp.single_eq_same, MonoidAlgebra.one_def]
· simp only [MonoidAlgebra.of_apply, ne_eq, ha, not_false_eq_true, Finsupp.single_eq_of_ne,
MonoidAlgebra.one_def]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 proof
by
exact Submodule.subset_span ⟨(g₁, g₂), rfl⟩Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 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''Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem universalDifferential_one (ψ : G →* H) : universalDifferential ψ (1 : G) = 0The universal differential vanishes at the group identity.
Show 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''.symmProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem universalDifferential_mul_inv_right (ψ : G →* H) (g : G) :
universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ g⁻¹ = 0Show proof
by
have h : 0 = universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ g⁻¹ := by
simpa using universalDifferential_mul ψ g g⁻¹
simpa using h.symmProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem 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 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]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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\).
theorem groupRingScalar_apply (ψ : G →* H) (g : G) :
groupRingScalar ψ g = (MonoidAlgebra.of ℤ H (ψ g) : GroupRing H)The Fox differential coordinate map is evaluated by the generator formula and the crossed-derivation rule.
Show proof
rflProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 proof
rflProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 proof
rflProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□def 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}\).
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 proof
rflProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□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 proof
rflProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□