exists_larger_subobject — Mathlib

English

Given a subobject A of X that is not top, there exists a strictly larger subobject A' with a pushout relation via generatingMonomorphisms.

Русский

Для подобъекта A ⊂ X найдётся больший A' с пуш-оут-отношением через generatingMonomorphisms.

LaTeX

$$$\exists A',\ A < A' \wedge (generatingMonomorphisms G).pushouts (A \to A')$$$

Lean4

theorem exists_larger_subobject {X : C} (A : Subobject X) (hA : A ≠ ⊤) :
    ∃ (A' : Subobject X) (h : A < A'), (generatingMonomorphisms G).pushouts (Subobject.ofLE A A' h.le) :=
  by
  induction A using Subobject.ind with
  | _ f
  obtain ⟨X', i, p', hi, hi', hp', fac⟩ := exists_pushouts hG f (by simpa only [Subobject.isIso_iff_mk_eq_top] using hA)
  refine ⟨Subobject.mk p', Subobject.mk_lt_mk_of_comm i fac hi', (MorphismProperty.arrow_mk_iso_iff _ ?_).2 hi⟩
  refine Arrow.isoMk (Subobject.underlyingIso f) (Subobject.underlyingIso p') ?_
  dsimp
  simp only [← cancel_mono p', assoc, fac, Subobject.underlyingIso_hom_comp_eq_mk, Subobject.ofLE_arrow]

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