English
If M-action is pretransitive and f:M→* N, then N-action is pretransitive.
Русский
Если M-действие предтранситивно и f — гомоморфизм, то N-действие предтранситивно.
LaTeX
$$$\\text{IsPretransitive } M α \\Rightarrow \\text{IsPretransitive } N α$ via $f$.$$
Lean4
/-- If an action is transitive, then composing this action with a surjective homomorphism gives
again a transitive action. -/
@[to_additive]
theorem isPretransitive_compHom {E F G : Type*} [Monoid E] [Monoid F] [MulAction F G] [IsPretransitive F G] {f : E →* F}
(hf : Surjective f) :
letI : MulAction E G := MulAction.compHom _ f
IsPretransitive E G :=
by
let _ : MulAction E G := MulAction.compHom _ f
refine ⟨fun x y ↦ ?_⟩
obtain ⟨m, rfl⟩ : ∃ m : F, m • x = y := exists_smul_eq F x y
obtain ⟨e, rfl⟩ : ∃ e, f e = m := hf m
exact ⟨e, rfl⟩
