Subobjects in the category of structured arrows #
We compute the subobjects of an object A in the category StructuredArrow S T for T : C ⥤ D
and S : D as a subtype of the subobjects of A.right. We deduce that StructuredArrow S T is
well-powered if C is.
Main declarations #
StructuredArrow.subobjectEquiv: the order-equivalence betweenSubobject Aand a subtype ofSubobject A.right.
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.
def
CategoryTheory.StructuredArrow.projectSubobject
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : D}
{T : CategoryTheory.Functor C D}
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits T]
{A : CategoryTheory.StructuredArrow S T}
:
CategoryTheory.Subobject A → CategoryTheory.Subobject A.right
Every subobject of a structured arrow can be projected to a subobject of the underlying object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.StructuredArrow.projectSubobject_mk
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : D}
{T : CategoryTheory.Functor C D}
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits T]
{A P : CategoryTheory.StructuredArrow S T}
(f : P ⟶ A)
[CategoryTheory.Mono f]
:
theorem
CategoryTheory.StructuredArrow.projectSubobject_factors
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : D}
{T : CategoryTheory.Functor C D}
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits T]
{A : CategoryTheory.StructuredArrow S T}
(P : CategoryTheory.Subobject A)
:
∃ (q :
(CategoryTheory.Functor.fromPUnit S).obj A.left ⟶ T.obj (CategoryTheory.Subobject.underlying.obj (CategoryTheory.StructuredArrow.projectSubobject P))),
CategoryTheory.CategoryStruct.comp q (T.map (CategoryTheory.StructuredArrow.projectSubobject P).arrow) = A.hom
def
CategoryTheory.StructuredArrow.liftSubobject
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : D}
{T : CategoryTheory.Functor C D}
{A : CategoryTheory.StructuredArrow S T}
(P : CategoryTheory.Subobject A.right)
{q : (CategoryTheory.Functor.fromPUnit S).obj A.left ⟶ T.obj (CategoryTheory.Subobject.underlying.obj P)}
(hq : CategoryTheory.CategoryStruct.comp q (T.map P.arrow) = A.hom)
:
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
Instances For
theorem
CategoryTheory.StructuredArrow.lift_projectSubobject
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : D}
{T : CategoryTheory.Functor C D}
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits T]
{A : CategoryTheory.StructuredArrow S T}
(P : CategoryTheory.Subobject A)
{q :
(CategoryTheory.Functor.fromPUnit S).obj A.left ⟶ T.obj (CategoryTheory.Subobject.underlying.obj (CategoryTheory.StructuredArrow.projectSubobject P))}
(hq : CategoryTheory.CategoryStruct.comp q (T.map (CategoryTheory.StructuredArrow.projectSubobject P).arrow) = A.hom)
:
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.
def
CategoryTheory.StructuredArrow.subobjectEquiv
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : D}
{T : CategoryTheory.Functor C D}
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits T]
(A : CategoryTheory.StructuredArrow S T)
:
CategoryTheory.Subobject A ≃o { P : CategoryTheory.Subobject A.right //
∃ (q : (CategoryTheory.Functor.fromPUnit S).obj A.left ⟶ T.obj (CategoryTheory.Subobject.underlying.obj P)),
CategoryTheory.CategoryStruct.comp 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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.StructuredArrow.subobjectEquiv_symm_apply
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : D}
{T : CategoryTheory.Functor C D}
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits T]
(A : CategoryTheory.StructuredArrow S T)
(P :
{ P : CategoryTheory.Subobject A.right //
∃ (q : (CategoryTheory.Functor.fromPUnit S).obj A.left ⟶ T.obj (CategoryTheory.Subobject.underlying.obj P)),
CategoryTheory.CategoryStruct.comp q (T.map P.arrow) = A.hom })
:
(RelIso.symm A.subobjectEquiv) P = CategoryTheory.Subobject.mk (CategoryTheory.StructuredArrow.homMk (↑P).arrow ⋯)
@[simp]
theorem
CategoryTheory.StructuredArrow.subobjectEquiv_apply_coe
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : D}
{T : CategoryTheory.Functor C D}
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits T]
(A : CategoryTheory.StructuredArrow S T)
(P : CategoryTheory.Subobject A)
:
↑(A.subobjectEquiv P) = CategoryTheory.StructuredArrow.projectSubobject P
instance
CategoryTheory.StructuredArrow.wellPowered_structuredArrow
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : D}
{T : CategoryTheory.Functor C D}
[CategoryTheory.WellPowered C]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.Limits.PreservesLimits T]
:
If C is well-powered and complete and T preserves limits, then StructuredArrow S T is
well-powered.
Equations
- ⋯ = ⋯
def
CategoryTheory.CostructuredArrow.projectQuotient
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : CategoryTheory.Functor C D}
{T : D}
[CategoryTheory.Limits.HasColimits C]
[CategoryTheory.Limits.PreservesColimits S]
{A : CategoryTheory.CostructuredArrow S T}
:
CategoryTheory.Subobject (Opposite.op A) → CategoryTheory.Subobject (Opposite.op A.left)
Every quotient of a costructured arrow can be projected to a quotient of the underlying object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.CostructuredArrow.projectQuotient_mk
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : CategoryTheory.Functor C D}
{T : D}
[CategoryTheory.Limits.HasColimits C]
[CategoryTheory.Limits.PreservesColimits S]
{A : CategoryTheory.CostructuredArrow S T}
{P : (CategoryTheory.CostructuredArrow S T)ᵒᵖ}
(f : P ⟶ Opposite.op A)
[CategoryTheory.Mono f]
:
theorem
CategoryTheory.CostructuredArrow.projectQuotient_factors
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : CategoryTheory.Functor C D}
{T : D}
[CategoryTheory.Limits.HasColimits C]
[CategoryTheory.Limits.PreservesColimits S]
{A : CategoryTheory.CostructuredArrow S T}
(P : CategoryTheory.Subobject (Opposite.op A))
:
∃ (q :
S.obj (Opposite.unop (CategoryTheory.Subobject.underlying.obj (CategoryTheory.CostructuredArrow.projectQuotient P))) ⟶ (CategoryTheory.Functor.fromPUnit T).obj A.right),
CategoryTheory.CategoryStruct.comp (S.map (CategoryTheory.CostructuredArrow.projectQuotient P).arrow.unop) q = A.hom
def
CategoryTheory.CostructuredArrow.liftQuotient
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : CategoryTheory.Functor C D}
{T : D}
{A : CategoryTheory.CostructuredArrow S T}
(P : CategoryTheory.Subobject (Opposite.op A.left))
{q :
S.obj (Opposite.unop (CategoryTheory.Subobject.underlying.obj P)) ⟶ (CategoryTheory.Functor.fromPUnit T).obj A.right}
(hq : CategoryTheory.CategoryStruct.comp (S.map P.arrow.unop) q = A.hom)
:
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
- CategoryTheory.CostructuredArrow.liftQuotient P hq = CategoryTheory.Subobject.mk (CategoryTheory.CostructuredArrow.homMk P.arrow.unop hq).op
Instances For
@[simp]
theorem
CategoryTheory.CostructuredArrow.unop_left_comp_underlyingIso_hom_unop
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : CategoryTheory.Functor C D}
{T : D}
{A : CategoryTheory.CostructuredArrow S T}
{P : (CategoryTheory.CostructuredArrow S T)ᵒᵖ}
(f : P ⟶ Opposite.op A)
[CategoryTheory.Mono f.unop.left.op]
:
CategoryTheory.CategoryStruct.comp f.unop.left (CategoryTheory.Subobject.underlyingIso f.unop.left.op).hom.unop = (CategoryTheory.Subobject.mk f.unop.left.op).arrow.unop
Technical lemma for lift_projectQuotient.
theorem
CategoryTheory.CostructuredArrow.lift_projectQuotient
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : CategoryTheory.Functor C D}
{T : D}
[CategoryTheory.Limits.HasColimits C]
[CategoryTheory.Limits.PreservesColimits S]
{A : CategoryTheory.CostructuredArrow S T}
(P : CategoryTheory.Subobject (Opposite.op A))
{q :
S.obj (Opposite.unop (CategoryTheory.Subobject.underlying.obj (CategoryTheory.CostructuredArrow.projectQuotient P))) ⟶ (CategoryTheory.Functor.fromPUnit T).obj A.right}
(hq :
CategoryTheory.CategoryStruct.comp (S.map (CategoryTheory.CostructuredArrow.projectQuotient P).arrow.unop) q = A.hom)
:
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.
theorem
CategoryTheory.CostructuredArrow.unop_left_comp_ofMkLEMk_unop
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : CategoryTheory.Functor C D}
{T : D}
{A : CategoryTheory.CostructuredArrow S T}
{P Q : (CategoryTheory.CostructuredArrow S T)ᵒᵖ}
{f : P ⟶ Opposite.op A}
{g : Q ⟶ Opposite.op A}
[CategoryTheory.Mono f.unop.left.op]
[CategoryTheory.Mono g.unop.left.op]
(h : CategoryTheory.Subobject.mk f.unop.left.op ≤ CategoryTheory.Subobject.mk g.unop.left.op)
:
CategoryTheory.CategoryStruct.comp g.unop.left
(CategoryTheory.Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left
Technical lemma for quotientEquiv.
def
CategoryTheory.CostructuredArrow.quotientEquiv
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : CategoryTheory.Functor C D}
{T : D}
[CategoryTheory.Limits.HasColimits C]
[CategoryTheory.Limits.PreservesColimits S]
(A : CategoryTheory.CostructuredArrow S T)
:
CategoryTheory.Subobject (Opposite.op A) ≃o { P : CategoryTheory.Subobject (Opposite.op A.left) //
∃ (q :
S.obj (Opposite.unop (CategoryTheory.Subobject.underlying.obj P)) ⟶ (CategoryTheory.Functor.fromPUnit T).obj A.right),
CategoryTheory.CategoryStruct.comp (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
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.CostructuredArrow.well_copowered_costructuredArrow
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{S : CategoryTheory.Functor C D}
{T : D}
[CategoryTheory.WellPowered Cᵒᵖ]
[CategoryTheory.Limits.HasColimits C]
[CategoryTheory.Limits.PreservesColimits S]
:
If C is well-copowered and cocomplete and S preserves colimits, then
CostructuredArrow S T is well-copowered.
Equations
- ⋯ = ⋯