ofMkLEMk_comp_ofMkLE — Mathlib

English

The composition of ofMkLE and ofLEMk yields the ofMkLEMk for transitive mk f ≤ mk g ≤ X.

Русский

Сложение ofMkLE и ofLEMk даёт ofMkLEMk для переходного mk f ≤ mk g ≤ X.

LaTeX

$$$\operatorname{ofMkLE} f X h_1 \;\circ\; \operatorname{ofLEMk} X g h_2 = \operatorname{ofMkLEMk} f g (h_1.trans h_2)$$$

Lean4

@[reassoc (attr := simp)]
theorem ofMkLEMk_comp_ofMkLE {B A₁ A₂ : C} (f : A₁ ⟶ B) [Mono f] (g : A₂ ⟶ B) [Mono g] (X : Subobject B)
    (h₁ : mk f ≤ mk g) (h₂ : mk g ≤ X) : ofMkLEMk f g h₁ ≫ ofMkLE g X h₂ = ofMkLE f X (h₁.trans h₂) :=
  by
  simp only [ofMkLE, ofLE, ofMkLEMk, ← Functor.map_comp underlying, assoc, Iso.hom_inv_id_assoc]
  congr 1

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