English
Pull back a multiplicative action along an injective map respecting the action: given an injective f: β → α and a smul compatibility, one obtains a MulAction M on β with smul := (•) and preserved action.
Русский
Вытягивание умножающего действия по инъекции: при несовпадаемой связи f: β → α и совместимости скалярного действия образуется MulAction на β с тем же действием.
LaTeX
$$$\\\\exists (smul : M \\times β \\to β), \\\\ &\\forall c \\in M, x \\in β, f(c \\cdot x) = c \\cdot f(x) \\\\ &\\text{инъекция } f \\\\rightarrow \\\\text{MulAction } M β.$$$
Lean4
/-- Pushforward a multiplicative action along a surjective map respecting `•`.
See note [reducible non-instances]. -/
@[to_additive /-- Pushforward an additive action along a surjective map respecting `+ᵥ`. -/
]
protected abbrev mulAction [SMul M β] (f : α → β) (hf : Surjective f) (smul : ∀ (c : M) (x), f (c • x) = c • f x) :
MulAction M β where
smul := (· • ·)
one_smul := by simp [hf.forall, ← smul]
mul_smul := by simp [hf.forall, ← smul, mul_smul]
