English
Automorphization commutes with scalar action in the quotient by a subgroup: automorphize (g•f) = g•automorphize f.
Русский
Автоматизизация в отношении скалярного действия в отношении фактор-группы: automorphize( g•f ) = g•automorphize(f).
LaTeX
$$$\\operatorname{automorphize}((g\\circ (quotient.mk'))\\,f) = g\\cdot(\\operatorname{automorphize} f)$$$
Lean4
/-- Automorphization of a function into an `R`-`Module` distributes, that is, commutes with the
`R`-scalar multiplication. -/
theorem automorphize_smul_left [AddGroup α] [AddAction α β] (f : β → M) (g : Quotient (AddAction.orbitRel α β) → R) :
AddAction.automorphize ((g ∘ (@Quotient.mk' _ (_))) • f) =
g • (AddAction.automorphize f : Quotient (AddAction.orbitRel α β) → M) :=
by
ext x
apply @Quotient.inductionOn' β (AddAction.orbitRel α β) _ x _
intro b
simp only [automorphize, Pi.smul_apply', comp_apply]
set π : β → Quotient (AddAction.orbitRel α β) := Quotient.mk (AddAction.orbitRel α β)
have H₁ : ∀ a : α, π (a +ᵥ b) = π b := by
intro a
apply (@Quotient.eq _ (AddAction.orbitRel α β) (a +ᵥ b) b).mpr
use a
change ∑' a : α, g (π (a +ᵥ b)) • f (a +ᵥ b) = g (π b) • ∑' a : α, f (a +ᵥ b)
simp_rw [H₁]
exact tsum_const_smul'' _
