English
Let f: P → Q and g: Q → R be arrows in a category. If the composite f; g is a strong epimorphism, then g is a strong epimorphism.
Русский
Пусть существуют стрелы f: P → Q и g: Q → R в категории. Если композиция f ∘ g является сильной эпиморфизмом, то и g является сильной эпиморфизмом.
LaTeX
$$$\\forall \\; P,Q,R \\;\\text{objects},\\; f: P \\to Q,\\; g: Q \\to R,\\; [\\mathrm{StrongEpi}(f \\circ g)] \\Rightarrow \\mathrm{StrongEpi}(g).$$$
Lean4
/-- If `f ≫ g` is a strong epimorphism, then so is `g`. -/
theorem strongEpi_of_strongEpi [StrongEpi (f ≫ g)] : StrongEpi g :=
{ epi := epi_of_epi f g
llp := fun {X Y} z _ => by
constructor
intro u v sq
have h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v := by simp only [Category.assoc, sq.w]
exact
CommSq.HasLift.mk'
⟨(CommSq.mk h₀).lift, by simp only [← cancel_mono z, Category.assoc, CommSq.fac_right, sq.w], by simp⟩ }
