English
Automorphization on the quotient is equivalent to automorphization by the corresponding action on the representative via equality of quotient representations.
Русский
Эквивалентность автоматизации на фактор-группе и через действие на представителе через равенство представлений группы.
LaTeX
$$$\\operatorname{QuotientGroup}.automorphize(f) = \\operatorname{MulAction}.automorphize(f)$$$
Lean4
/-- Given a subgroup `Γ` of a group `G`, and a function `f : G → M`, we "automorphize" `f` to a
function `G ⧸ Γ → M` by summing over `Γ` orbits, `g ↦ ∑' (γ : Γ), f(γ • g)`. -/
@[to_additive /-- Given a subgroup `Γ` of an additive group `G`, and a function `f : G → M`, we
automorphize `f` to a function `G ⧸ Γ → M` by summing over `Γ` orbits,
`g ↦ ∑' (γ : Γ), f(γ • g)`. -/
]
noncomputable def automorphize (f : G → M) : G ⧸ Γ → M :=
MulAction.automorphize f
