English
A compatibility lemma for lifting maps across MonoidAlgebra via ρ and σ, showing equality for all r and x.
Русский
Лемма совместимости для подъёма отображений через MonoidAlgebra через ρ и σ, равенство для всех r и x.
LaTeX
$$$$ \\text{to_Module_monoidAlgebra_map_aux } \\{k G \\} (f, w, r, x) $$$$
Lean4
/-- Auxiliary lemma for `toModuleMonoidAlgebra`. -/
theorem to_Module_monoidAlgebra_map_aux {k G : Type*} [CommRing k] [Monoid G] (V W : Type*) [AddCommGroup V]
[AddCommGroup W] [Module k V] [Module k W] (ρ : G →* V →ₗ[k] V) (σ : G →* W →ₗ[k] W) (f : V →ₗ[k] W)
(w : ∀ g : G, f.comp (ρ g) = (σ g).comp f) (r : MonoidAlgebra k G) (x : V) :
f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) r) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) r) (f x) :=
by
apply MonoidAlgebra.induction_on r
· intro g
simp only [one_smul, MonoidAlgebra.lift_single, MonoidAlgebra.of_apply]
exact LinearMap.congr_fun (w g) x
· intro g h gw hw; simp only [map_add, LinearMap.add_apply, hw, gw]
· intro r g w
simp only [map_smul, w, LinearMap.smul_apply]
