projectQuotient — Mathlib

English

Every quotient (subobject) of the opposite of a costructured arrow projects to a quotient of the left part; i.e., Subobject (op A) → Subobject (op A.left).

Русский

Любая квота (подобъект) противоположного costructured_arrow проецируется на квоту левой части; т.е. Subobject(op A) → Subobject(op A.left).

LaTeX

$$$\\forall A, \\mathrm{Subobject}(\\mathrm{op}\; A) \\to \\mathrm{Subobject}(\\mathrm{op}\; A.left).$$$

Lean4

/-- Every quotient of a costructured arrow can be projected to a quotient of the underlying
    object. -/
def projectQuotient [HasFiniteColimits C] [PreservesFiniteColimits S] {A : CostructuredArrow S T} :
    Subobject (op A) → Subobject (op A.left) :=
  by
  refine Subobject.lift (fun P f hf => Subobject.mk f.unop.left.op) ?_
  intro P Q f g hf hg i hi
  refine Subobject.mk_eq_mk_of_comm _ _ ((proj S T).mapIso i.unop).op (Quiver.Hom.unop_inj ?_)
  have := congr_arg Quiver.Hom.unop hi
  simpa using congr_arg CommaMorphism.left this

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