unop_left_comp_underlyingIso_hom_unop

English

The inverse of projection via liftSubobject yields the original quotient up to isomorphism, i.e., lift_projectQuotient (projectQuotient P) hq = P.

Русский

Обратная связь проекции через lift_projectQuotient и projectQuotient возвращает исходную квоту вплоть до изоморфизма.

LaTeX

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

Lean4

/-- Technical lemma for `lift_projectQuotient`. -/
@[simp]
theorem unop_left_comp_underlyingIso_hom_unop {A : CostructuredArrow S T} {P : (CostructuredArrow S T)ᵒᵖ} (f : P ⟶ op A)
    [Mono f.unop.left.op] :
    f.unop.left ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop = (Subobject.mk f.unop.left.op).arrow.unop :=
  by
  conv_lhs =>
    congr
    rw [← Quiver.Hom.unop_op f.unop.left]
  rw [← unop_comp, Subobject.underlyingIso_hom_comp_eq_mk]

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