comp_eq_top_iff — Mathlib

English

For two morphism properties W1 and W2, the composite W1.comp W2 equals the top element if and only if there exists a factorization of morphisms with respect to W1 and W2.

Русский

Для свойств морфизмов W1 и W2 композиция W1.comp W2 равна верхнему элементу тогда и только тогда существует факторизация морфизмов относительно W1 и W2.

LaTeX

$$$W_1 \cdot W_2 = \top \; \Leftrightarrow \; HasFactorization W_1 W_2$$$

Lean4

theorem comp_eq_top_iff : W₁.comp W₂ = ⊤ ↔ HasFactorization W₁ W₂ :=
  by
  constructor
  · intro h
    refine ⟨fun f => ?_⟩
    have : W₁.comp W₂ f := by simp only [h, top_apply]
    exact ⟨this.some⟩
  · intro
    ext X Y f
    simp only [top_apply, iff_true]
    exact ⟨factorizationData W₁ W₂ f⟩

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