English
Automorphize a function f: G → M to a function on the quotient G/Γ by summing over Γ-orbits: (G → M) → (G/Γ → M).
Русский
Пусть Γ — подгруппа G; автоформирование функции f: G → M в функцию на фактор-группе G/Γ осуществляется суммированием по орбитам Γ.
LaTeX
$$$\\text{automorphize}:\\; G \\to M \\quad\\text{is given by}\\quad (G/Γ) \\ni gΓ \\mapsto \\sum_{\\gamma\\in Γ} f(\\gamma g)$$$
Lean4
/-- Given a group `α` acting on a type `β`, and a function `f : β → M`, we "automorphize" `f` to a
function `β ⧸ α → M` by summing over `α` orbits, `b ↦ ∑' (a : α), f(a • b)`. -/
@[to_additive /-- Given an additive group `α` acting on a type `β`, and a function `f : β → M`,
we automorphize `f` to a function `β ⧸ α → M` by summing over `α` orbits,
`b ↦ ∑' (a : α), f(a • b)`. -/
]
noncomputable def automorphize [Group α] [MulAction α β] (f : β → M) : Quotient (MulAction.orbitRel α β) → M :=
by
refine @Quotient.lift _ _ (_) (fun b ↦ ∑' (a : α), f (a • b)) ?_
intro b₁ b₂ ⟨a, (ha : a • b₂ = b₁)⟩
simp only
rw [← ha]
convert (Equiv.mulRight a).tsum_eq (fun a' ↦ f (a' • b₂)) using 1
simp only [Equiv.coe_mulRight]
congr
ext
congr 1
simp only [mul_smul]
-- we can't use `to_additive`, because it tries to translate `•` into `+ᵥ`
