Evaluating an automorphized function #
QuotientGroup.automorphize f sums f over the orbits of a subgroup Γ. At the class of a
point g it is the orbit sum ∑' γ, f (γ • g), where γ ranges over the opposite subgroup
Γ.op acting on G by right multiplication.
theorem
QuotientGroup.automorphize_mk
{M : Type u_1}
[TopologicalSpace M]
[AddCommMonoid M]
{G : Type u_2}
[Group G]
{Γ : Subgroup G}
(f : G → M)
(g : G)
:
The automorphization of f, evaluated at the class of g, is the sum of f over the orbit
of g under right multiplication by Γ.
theorem
QuotientAddGroup.automorphize_mk
{M : Type u_1}
[TopologicalSpace M]
[AddCommMonoid M]
{G : Type u_2}
[AddGroup G]
{Γ : AddSubgroup G}
(f : G → M)
(g : G)
:
The automorphization of f, evaluated at the class of g, is the sum of f
over the orbit of g under right addition by Γ.