Yamaguchi Lean 4 Library
FoxDifferential/Discrete/DifferentialModule/Universal.lean
FoxDifferential/Discrete/DifferentialModule/Universal/Source

FoxDifferential/Discrete/DifferentialModule/Universal.lean

1import FoxDifferential.Discrete.DifferentialModule.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Discrete/DifferentialModule/Universal.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Discrete group-ring Fox calculus
14The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.
15-/
16namespace FoxDifferential
18noncomputable section
20variable {H G : Type*} [Group H] [Group G]
22section UniversalProperty
24variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]
26/-- A `ψ`-differential map is a map satisfying the Fox Leibniz rule. -/
27abbrev IsDifferentialMap (ψ : G →* H) (δ : G → A) : Prop :=
30/-- The linear map out of the free pre-module determined by `δ`. -/
31def liftLinear (δ : G → A) : DifferentialPreModule H G →ₗ[GroupRing H] A :=
32 Finsupp.linearCombination (GroupRing H) δ
34omit [Group G] in
35/-- The linear extension of a map evaluates on a single basis vector by scalar multiplication. -/
36@[simp]
37theorem liftLinear_single (δ : G → A) (g : G) (r : GroupRing H) :
38 liftLinear δ (Finsupp.single g r) = r • δ g := by
39 simp only [liftLinear, Finsupp.linearCombination_single]
41/-- A crossed differential kills each defining relation of the universal differential module. -/
43 (ψ : G →* H) (δ : G → A) (hδ : IsDifferentialMap (A := A) ψ δ) (g₁ g₂ : G) :
44 liftLinear δ (relationElement ψ g₁ g₂) = 0 := by
45 simp only [liftLinear, relationElement, MonoidAlgebra.of_apply, Finsupp.smul_single, smul_eq_mul, mul_one,
46 map_sub, Finsupp.linearCombination_single, hδ g₁ g₂, groupRingScalar_apply, smul_add, one_smul, map_add, sub_self]
48/-- The relation submodule is contained in the kernel of the linear extension of a crossed
49differential. -/
51 (ψ : G →* H) (δ : G → A) (hδ : IsDifferentialMap (A := A) ψ δ) :
52 relationSubmodule ψ ≤ LinearMap.ker (liftLinear δ) := by
53 refine Submodule.span_le.2 ?_
54 rintro _ ⟨⟨g₁, g₂⟩, rfl⟩
55 simpa [LinearMap.mem_ker] using liftLinear_relationElement (A := A) ψ δ hδ g₁ g₂
57/-- The universal map induced by a `ψ`-differential map. -/
58def lift (ψ : G →* H) (δ : G → A) (hδ : IsDifferentialMap (A := A) ψ δ) :
59 DifferentialModule ψ →ₗ[GroupRing H] A :=
60 (relationSubmodule ψ).liftQ (liftLinear δ) (relationSubmodule_le_ker (A := A) ψ δ hδ)
62/-- The universal lift evaluates on `universalDifferential g` as the original crossed differential. -/
63theorem lift_d (ψ : G →* H) (δ : G → A) (hδ : IsDifferentialMap (A := A) ψ δ) (g : G) :
64 lift ψ δ hδ (universalDifferential ψ g) = δ g := by
65 change
67 (relationSubmodule_le_ker (A := A) ψ δ hδ)
68 ((relationSubmodule ψ).mkQ (Finsupp.single g 1)) = δ g
69 rw [Submodule.mkQ_apply, Submodule.liftQ_apply]
70 simp only [liftLinear_single, one_smul]
72/-- Linear maps out of the universal differential module are equal when they agree on all
73universal differentials. -/
74@[ext]
75theorem hom_ext (ψ : G →* H) {f g : DifferentialModule ψ →ₗ[GroupRing H] A}
76 (hfg : ∀ g', f (universalDifferential ψ g') = g (universalDifferential ψ g')) : f = g := by
77 apply Submodule.linearMap_qext _
78 apply Finsupp.lhom_ext
79 intro g' r
80 have hsingle : ((relationSubmodule ψ).mkQ (Finsupp.single g' r) : DifferentialModule ψ) =
81 r • universalDifferential ψ g' := by
82 rw [← Finsupp.smul_single_one]
83 rfl
84 change f ((relationSubmodule ψ).mkQ (Finsupp.single g' r)) =
85 g ((relationSubmodule ψ).mkQ (Finsupp.single g' r))
86 rw [hsingle]
87 simpa [map_smul] using congrArg (fun z => r • z) (hfg g')
89/-- The universal lift is the unique linear map with prescribed values on universal
90differentials. -/
91theorem lift_unique
92 (ψ : G →* H) (δ : G → A) (hδ : IsDifferentialMap (A := A) ψ δ)
93 (f : DifferentialModule ψ →ₗ[GroupRing H] A)
94 (hf : ∀ g, f (universalDifferential ψ g) = δ g) :
95 f = lift (A := A) ψ δ hδ := by
96 apply hom_ext ψ
97 intro g
98 rw [hf g, lift_d]
100/-- Existence and uniqueness of the linear map representing a discrete Fox crossed
101differential. -/
103 (ψ : G →* H) (δ : G → A) (hδ : IsDifferentialMap (A := A) ψ δ) :
104 ∃! f : DifferentialModule ψ →ₗ[GroupRing H] A, ∀ g, f (universalDifferential ψ g) = δ g := by
105 refine ⟨lift (A := A) ψ δ hδ, ?_, ?_⟩
106 · intro g
107 exact lift_d (A := A) ψ δ hδ g
108 · intro f hf
109 exact lift_unique (A := A) ψ δ hδ f hf
111/-- The crossed differential induced by a linear map out of the universal differential module. -/
113 (ψ : G →* H) (f : DifferentialModule ψ →ₗ[GroupRing H] A) : G → A :=
114 fun g => f (universalDifferential ψ g)
116/-- A linear map out of the universal differential module induces a crossed differential. -/
118 (ψ : G →* H) (f : DifferentialModule ψ →ₗ[GroupRing H] A) :
119 IsDifferentialMap (A := A) ψ (crossedDifferentialOfLinearMap (A := A) ψ f) := by
120 intro g₁ g₂
124/-- Universal representation theorem for discrete Fox crossed differentials.
126Crossed differentials `G -> A` with respect to `ψ : G ->* H` are the same as
127`ℤ[H]`-linear maps out of the universal differential module `A_ψ`. -/
129 {δ : G → A // IsDifferentialMap (A := A) ψ δ} ≃
130 (DifferentialModule ψ →ₗ[GroupRing H] A) where
131 toFun δ := lift (A := A) ψ δ.1 δ.2
132 invFun f :=
135 left_inv δ := by
136 apply Subtype.ext
137 funext g
138 exact lift_d (A := A) ψ δ.1 δ.2 g
139 right_inv f := by
140 apply hom_ext ψ
141 intro g
142 exact lift_d (A := A) ψ (crossedDifferentialOfLinearMap (A := A) ψ f)
145/-- Compatibility between the discrete representation theorem and the generic
146crossed-differential-module representation theorem. -/
148 (ψ : G →* H)
149 (δ : {δ : G → A // IsDifferentialMap (A := A) ψ δ}) :
152 (A := A) (groupRingScalar ψ) δ).comp
154 apply hom_ext ψ
155 intro g
156 change
157 lift (A := A) ψ δ.1 δ.2 (universalDifferential ψ g) =
162end UniversalProperty
164end
166end FoxDifferential