English
The quotient equivalence is built via projectQuotient and liftQuotient, with left and right inverses given by lift_projectSubobject and Subobject.lift.
Русский
Квота-эквивалентность строится через projectQuotient и liftQuotient; левый и правый обороты даны lift и Subobject.lift.
LaTeX
$$$\\mathrm{quotientEquiv} = \\langle \\mathrm{toFun} , \\mathrm{invFun}, \\mathrm{leftInv}, \\mathrm{rightInv} \\rangle.$$$
Lean4
/-- If `A : S.obj B ⟶ T` is a costructured arrow for `S : C ⥤ D` and `T : D`, then we can
explicitly describe the quotients of `A` as the quotients `P` of `B` in `C` for which `A.hom`
factors through the image of `P` under `S`. -/
def quotientEquiv [HasFiniteColimits C] [PreservesFiniteColimits S] (A : CostructuredArrow S T) :
Subobject (op A) ≃o { P : Subobject (op A.left) // ∃ q, S.map P.arrow.unop ≫ q = A.hom }
where
toFun P := ⟨projectQuotient P, projectQuotient_factors P⟩
invFun P := liftQuotient P.val P.prop.choose_spec
left_inv _ := lift_projectQuotient _ _
right_inv
P :=
Subtype.ext
(by
simp only [liftQuotient, Quiver.Hom.unop_op, homMk_left, Quiver.Hom.op_unop, projectQuotient_mk,
Subobject.mk_arrow])
map_rel_iff' := by
apply Subobject.ind₂
intro P Q f g hf hg
refine ⟨fun h => Subobject.mk_le_mk_of_comm ?_ ?_, fun h => ?_⟩
· refine (homMk (Subobject.ofMkLEMk _ _ h).unop ((cancel_epi (S.map g.unop.left)).1 ?_)).op
dsimp
simp only [← S.map_comp_assoc, unop_left_comp_ofMkLEMk_unop, unop_op, CommaMorphism.w, Functor.const_obj_obj,
right_eq_id, Functor.const_obj_map, Category.comp_id]
· apply Quiver.Hom.unop_inj
ext
exact unop_left_comp_ofMkLEMk_unop _
· refine Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).unop.left.op ?_
refine Quiver.Hom.unop_inj ?_
have := congr_arg Quiver.Hom.unop (Subobject.ofMkLEMk_comp h)
simpa only [unop_op, Functor.id_obj, Functor.const_obj_obj, MonoOver.mk'_obj, Over.mk_left, MonoOver.mk'_arrow,
unop_comp, Quiver.Hom.unop_op, comp_left] using congr_arg CommaMorphism.left this
