instEpiHSMulHomOfInvertible — Mathlib

English

If f: X → Y is epi and r ∈ R is invertible, then r • f is epi.

Русский

Если морфизм f: X → Y является эпи, и r обратим в R, то r • f снова эпиморфизм.

LaTeX

$$$\\text{If } f \\text{ is epi and } r \\in R\\text{ is invertible, then } r \\cdot f\\text{ is epi.}$$$

Lean4

instance {X Y : C} (f : X ⟶ Y) [Epi f] (r : R) [Invertible r] : Epi (r • f) :=
  ⟨fun g g' H => by
    rw [smul_comp, smul_comp, ← comp_smul, ← comp_smul, cancel_epi] at H
    simpa [smul_smul] using congr_arg (fun f => ⅟r • f) H⟩

Похожие утверждения