projectQuotient_factors — Mathlib

English

A subobject of A.left can be lifted to a subobject of A, provided a morphism q with the required commutativity exists.

Русский

Подобъект A.left может быть поднят до подобъекта A, если существует морфизм q, удовлетворяющий требуемой сомкнутости.

LaTeX

$$$\\forall P : \\mathrm{Subobject}(op\\; A.left),\\; \\forall q, (hq: S.map P.arrow.unop \\circ q = A.hom) \\Rightarrow \\mathrm{liftQuotient} P hq \\in \\mathrm{Subobject}(op\\; A).$$$

Lean4

theorem projectQuotient_factors [HasFiniteColimits C] [PreservesFiniteColimits S] {A : CostructuredArrow S T} :
    ∀ P : Subobject (op A), ∃ q, S.map (projectQuotient P).arrow.unop ≫ q = A.hom :=
  Subobject.ind _ fun P f hf =>
    ⟨S.map (Subobject.underlyingIso _).unop.inv ≫ P.unop.hom,
      by
      dsimp
      rw [← Category.assoc, ← S.map_comp, ← unop_comp]
      simp⟩

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