mathlib3 documentation

category_theory.subobject.comma

Subobjects in the category of structured arrows #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We compute the subobjects of an object A in the category structured_arrow S T for T : C ⥤ D and S : D as a subtype of the subobjects of A.right. We deduce that structured_arrow S T is well-powered if C is.

Main declarations #

Implementation notes #

Our computation requires that C has all limits and T preserves all limits. Furthermore, we require that the morphisms of C and D are in the same universe. It is possible that both of these requirements can be relaxed by refining the results about limits in comma categories.

We also provide the dual results. As usual, we use subobject (op A) for the quotient objects of A.

source
def category_theory.structured_arrow.project_subobject {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C ⥤ D} [category_theory.limits.has_limits C] [category_theory.limits.preserves_limits T] {A : category_theory.structured_arrow S T} :
category_theory.subobject A → category_theory.subobject A.right

Every subobject of a structured arrow can be projected to a subobject of the underlying object.

Equations
source
@[simp]
theorem category_theory.structured_arrow.project_subobject_mk {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C ⥤ D} [category_theory.limits.has_limits C] [category_theory.limits.preserves_limits T] {A P : category_theory.structured_arrow S T} (f : P ⟶ A) [category_theory.mono f] :
category_theory.structured_arrow.project_subobject (category_theory.subobject.mk f) = category_theory.subobject.mk f.right
source
theorem category_theory.structured_arrow.project_subobject_factors {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C ⥤ D} [category_theory.limits.has_limits C] [category_theory.limits.preserves_limits T] {A : category_theory.structured_arrow S T} (P : category_theory.subobject A) :
∃ (q : (category_theory.functor.from_punit S).obj A.left ⟶ T.obj ↑(category_theory.structured_arrow.project_subobject P)), q ≫ T.map (category_theory.structured_arrow.project_subobject P).arrow = A.hom
source
@[simp]
noncomputable def category_theory.structured_arrow.lift_subobject {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C ⥤ D} {A : category_theory.structured_arrow S T} (P : category_theory.subobject A.right) {q : (category_theory.functor.from_punit S).obj A.left ⟶ T.obj ↑P} (hq : q ≫ T.map P.arrow = A.hom) :
category_theory.subobject A

A subobject of the underlying object of a structured arrow can be lifted to a subobject of the structured arrow, provided that there is a morphism making the subobject into a structured arrow.

Equations
source
theorem category_theory.structured_arrow.lift_project_subobject {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C ⥤ D} [category_theory.limits.has_limits C] [category_theory.limits.preserves_limits T] {A : category_theory.structured_arrow S T} (P : category_theory.subobject A) {q : (category_theory.functor.from_punit S).obj A.left ⟶ T.obj ↑(category_theory.structured_arrow.project_subobject P)} (hq : q ≫ T.map (category_theory.structured_arrow.project_subobject P).arrow = A.hom) :
category_theory.structured_arrow.lift_subobject (category_theory.structured_arrow.project_subobject P) hq = P

Projecting and then lifting a subobject recovers the original subobject, because there is at most one morphism making the projected subobject into a structured arrow.

source
@[simp]
theorem category_theory.structured_arrow.subobject_equiv_apply_coe {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C ⥤ D} [category_theory.limits.has_limits C] [category_theory.limits.preserves_limits T] (A : category_theory.structured_arrow S T) (P : category_theory.subobject A) :
↑(⇑(A.subobject_equiv) P) = category_theory.structured_arrow.project_subobject P
source
@[simp]
theorem category_theory.structured_arrow.subobject_equiv_symm_apply {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C ⥤ D} [category_theory.limits.has_limits C] [category_theory.limits.preserves_limits T] (A : category_theory.structured_arrow S T) (P : {P // ∃ (q : (category_theory.functor.from_punit S).obj A.left ⟶ T.obj ↑P), q ≫ T.map P.arrow = A.hom}) :
⇑(rel_iso.symm A.subobject_equiv) P = category_theory.structured_arrow.lift_subobject P.val _
source
noncomputable def category_theory.structured_arrow.subobject_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C ⥤ D} [category_theory.limits.has_limits C] [category_theory.limits.preserves_limits T] (A : category_theory.structured_arrow S T) :
category_theory.subobject A ≃o {P // ∃ (q : (category_theory.functor.from_punit S).obj A.left ⟶ T.obj ↑P), q ≫ T.map P.arrow = A.hom}

If A : S → T.obj B is a structured arrow for S : D and T : C ⥤ D, then we can explicitly describe the subobjects of A as the subobjects P of B in C for which A.hom factors through the image of P under T.

Equations
source
@[protected, instance]
def category_theory.structured_arrow.well_powered_structured_arrow {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : D} {T : C ⥤ D} [category_theory.well_powered C] [category_theory.limits.has_limits C] [category_theory.limits.preserves_limits T] :
category_theory.well_powered (category_theory.structured_arrow S T)

If C is well-powered and complete and T preserves limits, then structured_arrow S T is well-powered.

source
def category_theory.costructured_arrow.project_quotient {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : C ⥤ D} {T : D} [category_theory.limits.has_colimits C] [category_theory.limits.preserves_colimits S] {A : category_theory.costructured_arrow S T} :
category_theory.subobject (opposite.op A) → category_theory.subobject (opposite.op A.left)

Every quotient of a costructured arrow can be projected to a quotient of the underlying object.

Equations
source
@[simp]
theorem category_theory.costructured_arrow.project_quotient_mk {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : C ⥤ D} {T : D} [category_theory.limits.has_colimits C] [category_theory.limits.preserves_colimits S] {A : category_theory.costructured_arrow S T} {P : (category_theory.costructured_arrow S T)ᵒᵖ} (f : P ⟶ opposite.op A) [category_theory.mono f] :
category_theory.costructured_arrow.project_quotient (category_theory.subobject.mk f) = category_theory.subobject.mk f.unop.left.op
source
theorem category_theory.costructured_arrow.project_quotient_factors {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : C ⥤ D} {T : D} [category_theory.limits.has_colimits C] [category_theory.limits.preserves_colimits S] {A : category_theory.costructured_arrow S T} (P : category_theory.subobject (opposite.op A)) :
∃ (q : S.obj (opposite.unop ↑(category_theory.costructured_arrow.project_quotient P)) ⟶ (category_theory.functor.from_punit T).obj A.right), S.map (category_theory.costructured_arrow.project_quotient P).arrow.unop ≫ q = A.hom
source
@[simp]
noncomputable def category_theory.costructured_arrow.lift_quotient {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : C ⥤ D} {T : D} {A : category_theory.costructured_arrow S T} (P : category_theory.subobject (opposite.op A.left)) {q : S.obj (opposite.unop ↑P) ⟶ (category_theory.functor.from_punit T).obj A.right} (hq : S.map P.arrow.unop ≫ q = A.hom) :
category_theory.subobject (opposite.op A)

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.

Equations
source
@[simp]
theorem category_theory.costructured_arrow.unop_left_comp_underlying_iso_hom_unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : C ⥤ D} {T : D} {A : category_theory.costructured_arrow S T} {P : (category_theory.costructured_arrow S T)ᵒᵖ} (f : P ⟶ opposite.op A) [category_theory.mono f.unop.left.op] :
f.unop.left ≫ (category_theory.subobject.underlying_iso f.unop.left.op).hom.unop = (category_theory.subobject.mk f.unop.left.op).arrow.unop

Technical lemma for lift_project_quotient.

source
theorem category_theory.costructured_arrow.lift_project_quotient {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : C ⥤ D} {T : D} [category_theory.limits.has_colimits C] [category_theory.limits.preserves_colimits S] {A : category_theory.costructured_arrow S T} (P : category_theory.subobject (opposite.op A)) {q : S.obj (opposite.unop ↑(category_theory.costructured_arrow.project_quotient P)) ⟶ (category_theory.functor.from_punit T).obj A.right} (hq : S.map (category_theory.costructured_arrow.project_quotient P).arrow.unop ≫ q = A.hom) :
category_theory.costructured_arrow.lift_quotient (category_theory.costructured_arrow.project_quotient P) hq = P

Projecting and then lifting a quotient recovers the original quotient, because there is at most one morphism making the projected quotient into a costructured arrow.

source
theorem category_theory.costructured_arrow.unop_left_comp_of_mk_le_mk_unop {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : C ⥤ D} {T : D} {A : category_theory.costructured_arrow S T} {P Q : (category_theory.costructured_arrow S T)ᵒᵖ} {f : P ⟶ opposite.op A} {g : Q ⟶ opposite.op A} [category_theory.mono f.unop.left.op] [category_theory.mono g.unop.left.op] (h : category_theory.subobject.mk f.unop.left.op ≤ category_theory.subobject.mk g.unop.left.op) :
g.unop.left ≫ (category_theory.subobject.of_mk_le_mk f.unop.left.op g.unop.left.op h).unop = f.unop.left

Technical lemma for quotient_equiv.

source
noncomputable def category_theory.costructured_arrow.quotient_equiv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : C ⥤ D} {T : D} [category_theory.limits.has_colimits C] [category_theory.limits.preserves_colimits S] (A : category_theory.costructured_arrow S T) :
category_theory.subobject (opposite.op A) ≃o {P // ∃ (q : S.obj (opposite.unop ↑P) ⟶ (category_theory.functor.from_punit T).obj A.right), S.map P.arrow.unop ≫ q = A.hom}

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.

Equations
source
@[protected, instance]
def category_theory.costructured_arrow.well_copowered_costructured_arrow {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {S : C ⥤ D} {T : D} [category_theory.well_powered Cᵒᵖ] [category_theory.limits.has_colimits C] [category_theory.limits.preserves_colimits S] :
category_theory.well_powered (category_theory.costructured_arrow S T)ᵒᵖ

If C is well-copowered and cocomplete and S preserves colimits, then costructured_arrow S T is well-copowered.