English
If an action is pretransitive and we push it forward along a surjective monoid homomorphism, the resulting action remains pretransitive.
Русский
Если действие предварительно транзитивно и его проталкивают вдоль сюръективного гомоморфизма моноидов, полученное действие остаётся предтранзитивным.
LaTeX
$$$\\text{IsPretransitive } E G \\Rightarrow \\text{IsPretransitive } N G$ under a surjective $f:E\\to* N$ with $\\text{MulAction.IsPretransitive}$.$$
Lean4
/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →* S`.
See also `Function.Surjective.distribMulActionLeft` and `Function.Surjective.moduleLeft`.
-/
@[to_additive /-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →+ S`. -/
]
abbrev mulActionLeft {R S M : Type*} [Monoid R] [MulAction R M] [Monoid S] [SMul S M] (f : R →* S) (hf : Surjective f)
(hsmul : ∀ (c) (x : M), f c • x = c • x) : MulAction S M
where
smul := (· • ·)
one_smul b := by rw [← f.map_one, hsmul, one_smul]
mul_smul := hf.forall₂.mpr fun a b x ↦ by simp only [← f.map_mul, hsmul, mul_smul]
