projectQuotient_mk — Mathlib

English

For a morphism f : P ⟶ A with P a subobject, the projection of Subobject.mk f is Subobject.mk f.unop.left.op.

Русский

Для морфизма f: P ⟶ A с P подобъект, проекция Subobject.mk f равна Subobject.mk f.unop.left.op.

LaTeX

$$$projectQuotient (Subobject.mk f) = Subobject.mk f.unop.left.op$$$

Lean4

@[simp]
theorem projectQuotient_mk [HasFiniteColimits C] [PreservesFiniteColimits S] {A : CostructuredArrow S T}
    {P : (CostructuredArrow S T)ᵒᵖ} (f : P ⟶ op A) [Mono f] :
    projectQuotient (Subobject.mk f) = Subobject.mk f.unop.left.op :=
  rfl

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