isomorphisms_le_pushouts — Mathlib

English

If every object X admits a morphism p in P with IsIso p, then all isomorphisms lie in P.pushouts.

Русский

Если для каждого объекта X существует морфизм p ∈ P, который является изоморфизмом, то все изоморфизмы лежат в P.pushouts.

LaTeX

$$(∀X, ∃A,B,p,q with P(p) and IsIso p) ⇒ isomorphisms(C) ≤ P.pushouts$$

Lean4

/-- If `P : MorphismProperty C` is such that any object in `C` maps to the
target of some morphism in `P`, then `P.pushouts` contains the isomorphisms. -/
theorem isomorphisms_le_pushouts (h : ∀ (X : C), ∃ (A B : C) (p : A ⟶ B) (_ : P p) (_ : B ⟶ X), IsIso p) :
    isomorphisms C ≤ P.pushouts := by
  intro X Y f (_ : IsIso f)
  obtain ⟨A, B, p, hp, g, _⟩ := h X
  exact
    ⟨A, B, p, p ≫ g, g ≫ f, hp,
      (IsPushout.of_id_snd (f := p ≫ g)).of_iso (Iso.refl _) (Iso.refl _) (asIso p) (asIso f) (by simp) (by simp)
        (by simp) (by simp)⟩

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