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