English
Automorphization distributes over scalar multiplication by a quotient of an action: (g ∘ quotient.mk') • f maps to g • automorphize f.
Русский
Автоматизизация распределяется по умножению на скаляр слева, формально: automorphize( (g ∘ quotient.mk') • f ) = g • automorphize f.
LaTeX
$$$\\operatorname{automorphize}((g\\circ \\mathrm{Quotient.mk}')\\cdot 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 [Group α] [MulAction α β] (f : β → M) (g : Quotient (MulAction.orbitRel α β) → R) :
MulAction.automorphize ((g ∘ (@Quotient.mk' _ (_))) • f) =
g • (MulAction.automorphize f : Quotient (MulAction.orbitRel α β) → M) :=
by
ext x
apply @Quotient.inductionOn' β (MulAction.orbitRel α β) _ x _
intro b
simp only [automorphize, Pi.smul_apply', comp_apply]
set π : β → Quotient (MulAction.orbitRel α β) := Quotient.mk (MulAction.orbitRel α β)
have H₁ : ∀ a : α, π (a • b) = π b := by
intro a
apply (@Quotient.eq _ (MulAction.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'' _
