Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Common.CrossedDifferential
ProCGroups/FoxDifferential/Common/CrossedDifferential/Source

Source: ProCGroups.FoxDifferential.Common.CrossedDifferential

1import Mathlib.Algebra.Group.Commutator
2import Mathlib.Algebra.Group.Units.Hom
3import Mathlib.Algebra.GroupWithZero.Action.Basic
4import Mathlib.Algebra.Group.Subgroup.Lattice
5import Mathlib.Algebra.Module.BigOperators
6import Mathlib.Algebra.Module.LinearMap.Basic
7import Mathlib.GroupTheory.SemidirectProduct
9/-!
10# Bundled crossed homomorphisms
12This module defines crossed homomorphisms for an additive group action and their scalar-character
13specialization. It supplies the Fox product, inverse, conjugation, commutator, and power rules;
14restriction to coefficient-trivial subgroups; linear pushforward and group-homomorphism pullback;
15the standard semidirect-product representation; and the additive-group structure on the space of
16crossed homomorphisms.
18`CrossedHom` and `ScalarCrossedHom` are the only crossed-differential representations exposed by
19this module. The former parallel raw-function predicate and its conversion layer have been
20removed, so downstream APIs operate on the bundled maps directly.
21-/
23namespace FoxDifferential
25open scoped BigOperators commutatorElement
27/-- Scalar multiplication by a character `coeff : G →* R`, expressed as an additive action.
29Because `G` is a group, every `coeff g` is automatically a unit; `toHomUnits` records that fact
30and produces actual additive automorphisms rather than mere additive endomorphisms. -/
31def scalarCrossedAction
32 {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
33 (coeff : G →* R) : G →* Multiplicative (AddAut A) :=
34 (DistribMulAction.toAddAut Rˣ A).comp coeff.toHomUnits
36/-- The action induced by a scalar character evaluates as scalar multiplication. -/
37@[simp]
38theorem scalarCrossedAction_apply
39 {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
40 (coeff : G →* R) (g : G) (a : A) :
41 scalarCrossedAction (A := A) coeff g a = coeff g • a :=
42 rfl
44/-- Convert an additive action to the multiplicative action used by Mathlib's standard
45`SemidirectProduct`. -/
46def crossedSemidirectMulAction
47 {G A : Type*} [Group G] [AddCommGroup A]
48 (action : G →* Multiplicative (AddAut A)) : G →* MulAut (Multiplicative A) :=
49 (MulAutMultiplicative A).symm.toMonoidHom.comp action
51/-- The standard Mathlib semidirect product attached to an additive action. -/
52abbrev CrossedSemidirectProduct
53 {G A : Type*} [Group G] [AddCommGroup A]
54 (action : G →* Multiplicative (AddAut A)) :=
55 SemidirectProduct (Multiplicative A) G (crossedSemidirectMulAction action)
57/-- The multiplicative form of an additive action agrees with the original action on elements. -/
58@[simp]
59theorem crossedSemidirectMulAction_apply
60 {G A : Type*} [Group G] [AddCommGroup A]
61 (action : G →* Multiplicative (AddAut A)) (g : G) (a : A) :
62 crossedSemidirectMulAction action g (Multiplicative.ofAdd a) =
63 Multiplicative.ofAdd (action g a) :=
64 rfl
66/-- Read the multiplicative presentation of the action back in the original additive group. -/
67@[simp]
68theorem crossedSemidirectMulAction_toAdd
69 {G A : Type*} [Group G] [AddCommGroup A]
70 (action : G →* Multiplicative (AddAut A)) (g : G) (a : Multiplicative A) :
71 Multiplicative.toAdd (crossedSemidirectMulAction action g a) =
72 action g (Multiplicative.toAdd a) :=
73 rfl
75/-- A crossed homomorphism bundled with its acting representation and Fox--Leibniz law. -/
76structure CrossedHom
77 {G A : Type*} [Group G] [AddCommGroup A]
78 (action : G →* Multiplicative (AddAut A)) where
79 /-- The function from the source group to the additive target. -/
80 toFun : G → A
81 /-- The crossed-homomorphism law with respect to the specified action. -/
82 map_mul' : ∀ g h, toFun (g * h) = toFun g + action g (toFun h)
84/-- Scalar-character crossed homomorphisms are a specialization of general crossed
85homomorphisms for the action `scalarCrossedAction coeff`. -/
86abbrev ScalarCrossedHom
87 {R G : Type*} [Semiring R] [Group G]
88 (coeff : G →* R) (A : Type*) [AddCommGroup A] [Module R A] :=
89 CrossedHom (scalarCrossedAction (A := A) coeff)
91namespace CrossedHom
93variable {G A : Type*} [Group G] [AddCommGroup A]
94variable {action : G →* Multiplicative (AddAut A)}
96/-- Crossed homomorphisms coerce to their underlying functions. -/
97instance instFunLike : FunLike (CrossedHom action) G A where
98 coe := CrossedHom.toFun
99 coe_injective f g h := by
100 cases f
101 cases g
102 simp_all
104/-- The underlying function of a crossed homomorphism agrees with its coercion to a function. -/
105@[simp]
106theorem toFun_apply (d : CrossedHom action) (g : G) : d.toFun g = d g := rfl
108/-- Equality of crossed homomorphisms is pointwise equality. -/
109@[ext]
110theorem ext {d e : CrossedHom action} (h : ∀ g, d g = e g) : d = e := by
111 apply DFunLike.ext d e
112 exact h
114/-- The bundled Fox--Leibniz rule for a general additive action. -/
115@[simp]
116theorem map_mul (d : CrossedHom action) (g h : G) :
117 d (g * h) = d g + action g (d h) :=
118 d.map_mul' g h
120/-- A crossed homomorphism vanishes at the identity. -/
121@[simp]
122theorem map_one (d : CrossedHom action) : d 1 = 0 := by
123 have h := d.map_mul 1 1
124 have hmul : d 1 = d 1 + d 1 := by
125 simpa only [one_mul, action.map_one, toAdd_one, AddAut.zero_apply] using h
126 have h' := congrArg (fun z : A => z - d 1) hmul
127 have hzero : 0 = d 1 := by
128 simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h'
129 exact hzero.symm
131/-- Inverse rule for a crossed homomorphism. -/
132theorem map_inv (d : CrossedHom action) (g : G) :
133 d g⁻¹ = -(action g⁻¹ (d g)) := by
134 have h := d.map_mul g⁻¹ g
135 rw [inv_mul_cancel, map_one] at h
136 rw [eq_neg_iff_add_eq_zero]
137 exact h.symm
139/-- Formula for multiplying by an inverse on the left. -/
140theorem map_inv_mul (d : CrossedHom action) (g h : G) :
141 d (g⁻¹ * h) = -(action g⁻¹ (d g)) + action g⁻¹ (d h) := by
142 rw [d.map_mul, d.map_inv]
144/-- Formula for multiplying by an inverse on the right. -/
145theorem map_mul_inv (d : CrossedHom action) (g h : G) :
146 d (g * h⁻¹) = d g - action (g * h⁻¹) (d h) := by
147 rw [d.map_mul, d.map_inv]
148 simp only [map_neg, sub_eq_add_neg, ← AddAut.add_apply]
149 rw [← toAdd_mul, ← action.map_mul]
151/-- Division rule for a crossed homomorphism. -/
152theorem map_div (d : CrossedHom action) (g h : G) :
153 d (g / h) = d g - action (g / h) (d h) := by
154 simpa [div_eq_mul_inv] using d.map_mul_inv g h
156/-- Conjugation rule for a crossed homomorphism. -/
157theorem map_conj (d : CrossedHom action) (g h : G) :
158 d (g * h * g⁻¹) =
159 d g + action g (d h) - action (g * h * g⁻¹) (d g) := by
160 rw [d.map_mul_inv (g * h) g, d.map_mul g h]
162/-- Commutator rule for a crossed homomorphism. -/
163theorem map_commutator (d : CrossedHom action) (g h : G) :
164 d ⁅g, h⁆ =
165 d g + action g (d h) - action (g * h * g⁻¹) (d g) -
166 action ⁅g, h⁆ (d h) := by
167 rw [commutatorElement_def, d.map_mul_inv (g * h * g⁻¹) h, d.map_conj g h]
169/-- Positive-power rule for a crossed homomorphism. -/
170theorem map_pow (d : CrossedHom action) (g : G) (n : ℕ) :
171 d (g ^ n) = (Finset.range n).sum (fun k => action (g ^ k) (d g)) := by
172 induction n with
173 | zero => simp only [pow_zero, map_one, Finset.range_zero, Finset.sum_empty]
174 | succ n ih =>
175 rw [pow_succ, d.map_mul, ih, Finset.sum_range_succ]
177/-- The graph of a crossed homomorphism is an ordinary homomorphism into the standard
178semidirect product. -/
179def toSemidirectMonoidHom (d : CrossedHom action) :
180 G →* CrossedSemidirectProduct action where
181 toFun g := ⟨Multiplicative.ofAdd (d g), g⟩
182 map_one' := by
183 apply SemidirectProduct.ext
184 · change d 1 = 0
185 exact d.map_one
186 · rfl
187 map_mul' g h := by
188 apply SemidirectProduct.ext
189 · change d (g * h) = d g + action g (d h)
190 exact d.map_mul g h
191 · rfl
193/-- The left component of the semidirect-product graph is the value of the crossed homomorphism. -/
194@[simp]
195theorem toSemidirectMonoidHom_left (d : CrossedHom action) (g : G) :
196 Multiplicative.toAdd (d.toSemidirectMonoidHom g).left = d g :=
197 rfl
199/-- The right component of the semidirect-product graph is the original group element. -/
200@[simp]
201theorem toSemidirectMonoidHom_right (d : CrossedHom action) (g : G) :
202 (d.toSemidirectMonoidHom g).right = g :=
203 rfl
205/-- Recover a crossed homomorphism from a semidirect-product homomorphism whose right component
206is the identity. -/
207def ofSemidirectMonoidHom
208 (f : G →* CrossedSemidirectProduct action)
209 (hright : ∀ g, (f g).right = g) : CrossedHom action where
210 toFun g := Multiplicative.toAdd (f g).left
211 map_mul' := by
212 intro g h
213 have hleft := congrArg SemidirectProduct.left (f.map_mul g h)
214 rw [SemidirectProduct.mul_left] at hleft
215 have hleftAdd := congrArg Multiplicative.toAdd hleft
216 simpa only [toAdd_mul, crossedSemidirectMulAction_toAdd, hright] using hleftAdd
218/-- Recovering a crossed homomorphism takes the additive form of the graph's left component. -/
219@[simp]
220theorem ofSemidirectMonoidHom_apply
221 (f : G →* CrossedSemidirectProduct action)
222 (hright : ∀ g, (f g).right = g) (g : G) :
223 ofSemidirectMonoidHom f hright g = Multiplicative.toAdd (f g).left :=
224 rfl
226/-- Recovering a crossed homomorphism from its semidirect-product graph returns the original map. -/
227@[simp]
228theorem ofSemidirectMonoidHom_toSemidirectMonoidHom (d : CrossedHom action) :
229 ofSemidirectMonoidHom d.toSemidirectMonoidHom
230 (fun g => toSemidirectMonoidHom_right d g) = d := by
231 apply CrossedHom.ext
232 intro g
233 rfl
235/-- The graph construction loses no information: a semidirect-product homomorphism over the
236identity is exactly the graph of the crossed homomorphism obtained from its left component. -/
237theorem toSemidirectMonoidHom_ofSemidirectMonoidHom
238 (f : G →* CrossedSemidirectProduct action)
239 (hright : ∀ g, (f g).right = g) :
240 (ofSemidirectMonoidHom f hright).toSemidirectMonoidHom = f := by
241 apply MonoidHom.ext
242 intro g
243 apply SemidirectProduct.ext
244 · rfl
245 · exact (hright g).symm
247/-- Pull back a crossed homomorphism along a group homomorphism. -/
248def compMonoidHom {K : Type*} [Group K]
249 (d : CrossedHom action) (φ : K →* G) : CrossedHom (action.comp φ) where
250 toFun k := d (φ k)
251 map_mul' := by
252 intro g h
253 change d (φ (g * h)) = d (φ g) + action (φ g) (d (φ h))
254 rw [φ.map_mul]
255 exact d.map_mul (φ g) (φ h)
257/-- Pullback along a group homomorphism evaluates by precomposition. -/
258@[simp]
259theorem compMonoidHom_apply {K : Type*} [Group K]
260 (d : CrossedHom action) (φ : K →* G) (k : K) :
261 d.compMonoidHom φ k = d (φ k) :=
262 rfl
264/-- Push a crossed homomorphism through an equivariant additive homomorphism. -/
265def mapAddEquivariant (d : CrossedHom action) {B : Type*} [AddCommGroup B]
266 (actionB : G →* Multiplicative (AddAut B)) (f : A →+ B)
267 (hf : ∀ g a, f (action g a) = actionB g (f a))
268 : CrossedHom actionB where
269 toFun g := f (d g)
270 map_mul' := by
271 intro g h
272 rw [d.map_mul g h, map_add, hf]
274/-- Equivariant pushforward evaluates by applying the additive homomorphism to each value. -/
275@[simp]
276theorem mapAddEquivariant_apply {B : Type*} [AddCommGroup B]
277 (actionB : G →* Multiplicative (AddAut B)) (f : A →+ B)
278 (hf : ∀ g a, f (action g a) = actionB g (f a))
279 (d : CrossedHom action) (g : G) :
280 d.mapAddEquivariant actionB f hf g = f (d g) :=
281 rfl
283/-- Crossed homomorphisms agreeing on a set agree on the subgroup it generates. -/
284theorem eqOn_closure (d e : CrossedHom action) {s : Set G}
285 (hs : Set.EqOn d e s) :
286 Set.EqOn d e ((Subgroup.closure s : Subgroup G) : Set G) := by
287 intro g hg
288 exact Subgroup.closure_induction
289 (p := fun g _ => d g = e g)
290 (fun x hx => hs hx)
291 (by
292 rw [d.map_one, e.map_one])
293 (fun x y _ _ hx hy => by
294 rw [d.map_mul x y, e.map_mul x y, hx, hy])
295 (fun x _ hx => by
296 rw [d.map_inv x, e.map_inv x, hx]) hg
298/-- Crossed homomorphisms are determined by their values on a generating set. -/
299theorem eq_of_closure_eq_top (d e : CrossedHom action) {s : Set G}
300 (hsgen : Subgroup.closure s = ⊤) (hs : Set.EqOn d e s) : d = e := by
301 apply CrossedHom.ext
302 intro g
303 exact d.eqOn_closure e hs (by simp only [hsgen, Subgroup.coe_top, Set.mem_univ])
305/-- The zero crossed homomorphism. -/
306instance instZero : Zero (CrossedHom action) where
307 zero := ⟨fun _ => 0, by intro g h; simp only [map_zero, add_zero]⟩
309/-- Pointwise addition of crossed homomorphisms. -/
310instance instAdd : Add (CrossedHom action) where
311 add d e := ⟨fun g => d g + e g, by
312 intro g h
313 rw [d.map_mul g h, e.map_mul g h, map_add]
314 ac_rfl⟩
316/-- The zero crossed homomorphism vanishes at every group element. -/
317@[simp]
318theorem zero_apply (g : G) : (0 : CrossedHom action) g = 0 := rfl
320/-- Addition of crossed homomorphisms is computed pointwise. -/
321@[simp]
322theorem add_apply (d e : CrossedHom action) (g : G) : (d + e) g = d g + e g := rfl
324/-- Natural-number scalar multiplication of crossed homomorphisms is repeated pointwise addition. -/
325instance instSMulNat : SMul ℕ (CrossedHom action) := ⟨nsmulRec⟩
327/-- Natural-number scalar multiplication of crossed homomorphisms is computed pointwise. -/
328@[simp]
329theorem nsmul_apply (n : ℕ) (d : CrossedHom action) (g : G) :
330 (n • d) g = n • d g := by
331 change (nsmulRec n d).toFun g = n • d g
332 induction n with
333 | zero => simp only [zero_nsmul]; rfl
334 | succ n ih =>
335 rw [nsmulRec, succ_nsmul]
336 change (nsmulRec n d).toFun g + d.toFun g = n • d.toFun g + d.toFun g
337 simpa only [toFun_apply] using congrArg (fun x : A => x + d.toFun g) ih
339/-- A temporary additive-monoid structure used while constructing the stronger additive group. -/
340local instance instAddCommMonoid : AddCommMonoid (CrossedHom action) :=
341 Function.Injective.addCommMonoid
342 (fun d : CrossedHom action => d.toFun)
343 (by intro d e h; exact CrossedHom.ext (congrFun h))
344 rfl (fun _ _ => rfl) (fun d n => by funext g; exact nsmul_apply n d g)
346/-- Negation of crossed homomorphisms is computed pointwise. -/
347instance instNeg : Neg (CrossedHom action) where
348 neg d := ⟨fun g => -d g, by
349 intro g h
350 rw [d.map_mul g h, map_neg]
351 simp only [neg_add_rev, add_comm]⟩
353/-- Subtraction of crossed homomorphisms is computed pointwise. -/
354instance instSub : Sub (CrossedHom action) where
355 sub d e := ⟨fun g => d g - e g, by
356 intro g h
357 rw [d.map_mul g h, e.map_mul g h, map_sub]
358 simp only [sub_eq_add_neg, neg_add_rev]
359 ac_rfl⟩
361/-- Evaluating a negated crossed homomorphism negates its value. -/
362@[simp]
363theorem neg_apply (d : CrossedHom action) (g : G) : (-d) g = -d g := rfl
365/-- Evaluating a difference of crossed homomorphisms subtracts their values. -/
366@[simp]
367theorem sub_apply (d e : CrossedHom action) (g : G) : (d - e) g = d g - e g := rfl
369/-- Integer scalar multiplication of crossed homomorphisms is repeated pointwise addition or
370subtraction. -/
371instance instSMulInt : SMul ℤ (CrossedHom action) :=
372 ⟨zsmulRec (nsmul := nsmulRec)⟩
374/-- Integer scalar multiplication of crossed homomorphisms is computed pointwise. -/
375@[simp]
376theorem zsmul_apply (z : ℤ) (d : CrossedHom action) (g : G) :
377 (z • d) g = z • d g := by
378 change (zsmulRec (nsmul := nsmulRec) z d).toFun g = z • d g
379 cases z with
380 | ofNat n => rw [zsmulRec]; change (n • d) g = (n : ℤ) • d g; rw [nsmul_apply, natCast_zsmul]
381 | negSucc n =>
382 rw [zsmulRec]
383 change (-(n.succ • d)) g = Int.negSucc n • d g
384 rw [neg_apply, nsmul_apply, negSucc_zsmul]
386/-- Pointwise operations make crossed homomorphisms an additive commutative group. -/
387instance instAddCommGroup : AddCommGroup (CrossedHom action) :=
388 Function.Injective.addCommGroup
389 (fun d : CrossedHom action => d.toFun)
390 (by intro d e h; exact CrossedHom.ext (congrFun h))
391 rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
392 (fun d n => by funext g; exact nsmul_apply n d g)
393 (fun d z => by funext g; exact zsmul_apply z d g)
395end CrossedHom
397namespace ScalarCrossedHom
399variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
400variable {coeff : G →* R}
402/-- Scalar crossed homomorphisms satisfy the scalar Fox--Leibniz product rule. -/
403@[simp]
404theorem map_mul (d : ScalarCrossedHom coeff A) (g h : G) :
405 d (g * h) = d g + coeff g • d h := by
406 simpa only [scalarCrossedAction_apply] using CrossedHom.map_mul d g h
408/-- A scalar crossed homomorphism vanishes at the identity. -/
409@[simp]
410theorem map_one (d : ScalarCrossedHom coeff A) : d 1 = 0 :=
411 CrossedHom.map_one d
413/-- The value of a scalar crossed homomorphism at an inverse is the transported negative value. -/
414theorem map_inv (d : ScalarCrossedHom coeff A) (g : G) :
415 d g⁻¹ = -(coeff g⁻¹ • d g) := by
416 simpa only [scalarCrossedAction_apply] using CrossedHom.map_inv d g
418/-- Formula for a scalar crossed homomorphism on a product with an inverse on the left. -/
419theorem map_inv_mul (d : ScalarCrossedHom coeff A) (g h : G) :
420 d (g⁻¹ * h) = -(coeff g⁻¹ • d g) + coeff g⁻¹ • d h := by
421 simpa only [scalarCrossedAction_apply] using CrossedHom.map_inv_mul d g h
423/-- Formula for a scalar crossed homomorphism on a product with an inverse on the right. -/
424theorem map_mul_inv (d : ScalarCrossedHom coeff A) (g h : G) :
425 d (g * h⁻¹) = d g - coeff (g * h⁻¹) • d h := by
426 simpa only [scalarCrossedAction_apply] using CrossedHom.map_mul_inv d g h
428/-- The scalar Fox rule written for group division. -/
429theorem map_div (d : ScalarCrossedHom coeff A) (g h : G) :
430 d (g / h) = d g - coeff (g / h) • d h := by
431 simpa only [scalarCrossedAction_apply] using CrossedHom.map_div d g h
433/-- The scalar crossed-homomorphism formula for a conjugate. -/
434theorem map_conj (d : ScalarCrossedHom coeff A) (g h : G) :
435 d (g * h * g⁻¹) = d g + coeff g • d h - coeff (g * h * g⁻¹) • d g := by
436 simpa only [scalarCrossedAction_apply] using CrossedHom.map_conj d g h
438/-- The scalar crossed-homomorphism formula for a commutator. -/
439theorem map_commutator (d : ScalarCrossedHom coeff A) (g h : G) :
440 d ⁅g, h⁆ = d g + coeff g • d h - coeff (g * h * g⁻¹) • d g -
441 coeff ⁅g, h⁆ • d h := by
442 simpa only [scalarCrossedAction_apply] using CrossedHom.map_commutator d g h
444/-- The value on a positive power is the sum of the translates of the value on its base. -/
445theorem map_pow (d : ScalarCrossedHom coeff A) (g : G) (n : ℕ) :
446 d (g ^ n) = (Finset.range n).sum (fun k => coeff (g ^ k) • d g) := by
447 simpa only [scalarCrossedAction_apply] using CrossedHom.map_pow d g n
449/-- Restrict a scalar crossed homomorphism to a subgroup on which its coefficient is trivial. -/
450def restrictTrivialSubgroupAddMonoidHom
451 (d : ScalarCrossedHom coeff A) (N : Subgroup G)
452 (hN : ∀ n : N, coeff n = 1) :
453 Additive N →+ A where
454 toFun n := d ((Additive.toMul n : N) : G)
455 map_zero' := by
456 change d (1 : G) = 0
457 exact map_one d
458 map_add' g h := by
459 change d (((Additive.toMul g : N) * (Additive.toMul h : N) : N) : G) =
460 d ((Additive.toMul g : N) : G) + d ((Additive.toMul h : N) : G)
461 have hmul :=
462 d.map_mul ((Additive.toMul g : N) : G) ((Additive.toMul h : N) : G)
463 simpa only [Subgroup.coe_mul, hN (Additive.toMul g), one_smul] using hmul
465/-- Restriction to a coefficient-trivial subgroup evaluates as the original crossed homomorphism. -/
466@[simp]
467theorem restrictTrivialSubgroupAddMonoidHom_apply
468 (d : ScalarCrossedHom coeff A) (N : Subgroup G)
469 (hN : ∀ n : N, coeff n = 1) (g : N) :
470 restrictTrivialSubgroupAddMonoidHom d N hN (Additive.ofMul g) = d g :=
471 rfl
473/-- A linear map is equivariant for scalar crossed actions and hence maps scalar crossed
474homomorphisms to scalar crossed homomorphisms. -/
475def mapLinear (d : ScalarCrossedHom coeff A) {B : Type*} [AddCommGroup B] [Module R B]
476 (f : A →ₗ[R] B) : ScalarCrossedHom coeff B :=
477 d.mapAddEquivariant (scalarCrossedAction (A := B) coeff) f.toAddMonoidHom
478 (by
479 intro g a
480 change f (coeff g • a) = coeff g • f a
481 exact f.map_smul (coeff g) a)
483/-- Linear pushforward evaluates by applying the linear map to each crossed-homomorphism value. -/
484@[simp]
485theorem mapLinear_apply {B : Type*} [AddCommGroup B] [Module R B]
486 (d : ScalarCrossedHom coeff A) (f : A →ₗ[R] B) (g : G) :
487 d.mapLinear f g = f (d g) :=
488 rfl
490/-- Pull back a scalar crossed homomorphism while retaining its scalar specialization. -/
491def compMonoidHom {K : Type*} [Group K]
492 (d : ScalarCrossedHom coeff A) (φ : K →* G) : ScalarCrossedHom (coeff.comp φ) A where
493 toFun k := d (φ k)
494 map_mul' := by
495 intro g h
496 change d (φ (g * h)) = d (φ g) + coeff (φ g) • d (φ h)
497 rw [φ.map_mul]
498 exact d.map_mul (φ g) (φ h)
500/-- Pullback of a scalar crossed homomorphism evaluates by precomposition. -/
501@[simp]
502theorem compMonoidHom_apply {K : Type*} [Group K]
503 (d : ScalarCrossedHom coeff A) (φ : K →* G) (k : K) :
504 d.compMonoidHom φ k = d (φ k) :=
505 rfl
507end ScalarCrossedHom
509end FoxDifferential