liftQuotient — Mathlib

English

For a subobject P of op A, there exists q with S.map (projectQuotient P).arrow.unop ≫ q = A.hom.

Русский

Для подобъекта P над op A существует q такой, что S.map (projectQuotient P).arrow.unop ≫ q = A.hom.

LaTeX

$$$\\forall P : \\mathrm{Subobject}(op A),\\; \\exists q, S.map (projectQuotient P).arrow.unop \\\\circ q = A.hom.$$$

Lean4

/-- A quotient of the underlying object of a costructured arrow can be lifted to a quotient of
    the costructured arrow, provided that there is a morphism making the quotient into a
    costructured arrow. -/
@[simp]
def liftQuotient {A : CostructuredArrow S T} (P : Subobject (op A.left)) {q} (hq : S.map P.arrow.unop ≫ q = A.hom) :
    Subobject (op A) :=
  Subobject.mk (homMk P.arrow.unop hq : A ⟶ mk q).op

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