Subobjects #
We define Subobject X as the quotient (by isomorphisms) of
MonoOver X := {f : Over X // Mono f.hom}.
Here MonoOver X is a thin category (a pair of objects has at most one morphism between them),
so we can think of it as a preorder. However as it is not skeletal, it is not a partial order.
There is a coercion from Subobject X back to the ambient category C
(using choice to pick a representative), and for P : Subobject X,
P.arrow : (P : C) ⟶ X is the inclusion morphism.
We provide
def pullback [HasPullbacks C] (f : X ⟶ Y) : Subobject Y ⥤ Subobject Xdef map (f : X ⟶ Y) [Mono f] : Subobject X ⥤ Subobject Ydef «exists_» [HasImages C] (f : X ⟶ Y) : Subobject X ⥤ Subobject Yand prove their basic properties and relationships. These are all easy consequences of the earlier development of the corresponding functors forMonoOver.
The subobjects of X form a preorder making them into a category. We have X ≤ Y if and only if
X.arrow factors through Y.arrow: see ofLE/ofLEMk/ofMkLE/ofMkLEMk and
le_of_comm. Similarly, to show that two subobjects are equal, we can supply an isomorphism between
the underlying objects that commutes with the arrows (eq_of_comm).
See also
CategoryTheory.Subobject.factorThru: an API describing factorization of morphisms through subobjects.CategoryTheory.Subobject.lattice: the lattice structures on subobjects.
Notes #
This development originally appeared in Bhavik Mehta's "Topos theory for Lean" repository, and was ported to mathlib by Scott Morrison.
Implementation note #
Currently we describe pullback, map, etc., as functors.
It may be better to just say that they are monotone functions,
and even avoid using categorical language entirely when describing Subobject X.
(It's worth keeping this in mind in future use; it should be a relatively easy change here
if it looks preferable.)
Relation to pseudoelements #
There is a separate development of pseudoelements in CategoryTheory.Abelian.Pseudoelements,
as a quotient (but not by isomorphism) of Over X.
When a morphism f has an image, the image represents the same pseudoelement.
In a category with images Pseudoelements X could be constructed as a quotient of MonoOver X.
In fact, in an abelian category (I'm not sure in what generality beyond that),
Pseudoelements X agrees with Subobject X, but we haven't developed this in mathlib yet.
We now construct the subobject lattice for X : C,
as the quotient by isomorphisms of MonoOver X.
Since MonoOver X is a thin category, we use ThinSkeleton to take the quotient.
Essentially all the structure defined above on MonoOver X descends to Subobject X,
with morphisms becoming inequalities, and isomorphisms becoming equations.
def
CategoryTheory.Subobject
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : C)
:
Type (max u₁ v₁)
The category of subobjects of X : C, defined as isomorphism classes of monomorphisms into X.
Instances For
instance
CategoryTheory.instPartialOrderSubobject
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : C)
:
Equations
- CategoryTheory.instPartialOrderSubobject X = id inferInstance
def
CategoryTheory.Subobject.mk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{A : C}
(f : A ⟶ X)
[CategoryTheory.Mono f]
:
Convenience constructor for a subobject.
Equations
Instances For
theorem
CategoryTheory.Comma.ext_iff
{A : Type u₁}
:
∀ {inst : CategoryTheory.Category.{v₁, u₁} A} {B : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} B} {T : Type u₃}
{inst_2 : CategoryTheory.Category.{v₃, u₃} T} {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
(x y : CategoryTheory.Comma L R), x = y ↔ x.left = y.left ∧ x.right = y.right ∧ HEq x.hom y.hom
theorem
CategoryTheory.Comma.ext
{A : Type u₁}
:
∀ {inst : CategoryTheory.Category.{v₁, u₁} A} {B : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} B} {T : Type u₃}
{inst_2 : CategoryTheory.Category.{v₃, u₃} T} {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
(x y : CategoryTheory.Comma L R), x.left = y.left → x.right = y.right → HEq x.hom y.hom → x = y
theorem
CategoryTheory.Subobject.ind
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(p : CategoryTheory.Subobject X → Prop)
(h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : CategoryTheory.Mono f], p (CategoryTheory.Subobject.mk f))
(P : CategoryTheory.Subobject X)
:
p P
theorem
CategoryTheory.Subobject.ind₂
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(p : CategoryTheory.Subobject X → CategoryTheory.Subobject X → Prop)
(h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : CategoryTheory.Mono f] [inst_1 : CategoryTheory.Mono g],
p (CategoryTheory.Subobject.mk f) (CategoryTheory.Subobject.mk g))
(P : CategoryTheory.Subobject X)
(Q : CategoryTheory.Subobject X)
:
p P Q
def
CategoryTheory.Subobject.lift
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Sort u_1}
{X : C}
(F : ⦃A : C⦄ → (f : A ⟶ X) → [inst : CategoryTheory.Mono f] → α)
(h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : CategoryTheory.Mono f] [inst_1 : CategoryTheory.Mono g] (i : A ≅ B),
CategoryTheory.CategoryStruct.comp i.hom g = f → F f = F g)
:
CategoryTheory.Subobject X → α
Declare a function on subobjects of X by specifying a function on monomorphisms with
codomain X.
Equations
- CategoryTheory.Subobject.lift F h P = Quotient.liftOn' P (fun (m : CategoryTheory.MonoOver X) => F m.arrow) ⋯
Instances For
@[simp]
theorem
CategoryTheory.Subobject.lift_mk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Sort u_1}
{X : C}
(F : ⦃A : C⦄ → (f : A ⟶ X) → [inst : CategoryTheory.Mono f] → α)
{h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : CategoryTheory.Mono f] [inst_1 : CategoryTheory.Mono g] (i : A ≅ B),
CategoryTheory.CategoryStruct.comp i.hom g = f → F f = F g}
{A : C}
(f : A ⟶ X)
[CategoryTheory.Mono f]
:
noncomputable def
CategoryTheory.Subobject.equivMonoOver
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : C)
:
The category of subobjects is equivalent to the MonoOver category. It is more convenient to
use the former due to the partial order instance, but oftentimes it is easier to define structures
on the latter.
Equations
Instances For
noncomputable def
CategoryTheory.Subobject.representative
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
:
Use choice to pick a representative MonoOver X for each Subobject X.
Equations
- CategoryTheory.Subobject.representative = (CategoryTheory.Subobject.equivMonoOver X).functor
Instances For
noncomputable def
CategoryTheory.Subobject.representativeIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(A : CategoryTheory.MonoOver X)
:
CategoryTheory.Subobject.representative.obj ((CategoryTheory.toThinSkeleton (CategoryTheory.MonoOver X)).obj A) ≅ A
Starting with A : MonoOver X, we can take its equivalence class in Subobject X
then pick an arbitrary representative using representative.obj.
This is isomorphic (in MonoOver X) to the original A.
Equations
- CategoryTheory.Subobject.representativeIso A = (CategoryTheory.Subobject.equivMonoOver X).counitIso.app A
Instances For
noncomputable def
CategoryTheory.Subobject.underlying
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
:
Use choice to pick a representative underlying object in C for any Subobject X.
Prefer to use the coercion P : C rather than explicitly writing underlying.obj P.
Equations
- CategoryTheory.Subobject.underlying = CategoryTheory.Subobject.representative.comp ((CategoryTheory.MonoOver.forget X).comp (CategoryTheory.Over.forget X))
Instances For
instance
CategoryTheory.Subobject.instCoeOut
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
:
Equations
- CategoryTheory.Subobject.instCoeOut = { coe := fun (Y : CategoryTheory.Subobject X) => CategoryTheory.Subobject.underlying.obj Y }
noncomputable def
CategoryTheory.Subobject.underlyingIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
CategoryTheory.Subobject.underlying.obj (CategoryTheory.Subobject.mk f) ≅ X
If we construct a Subobject Y from an explicit f : X ⟶ Y with [Mono f],
then pick an arbitrary choice of underlying object (Subobject.mk f : C) back in C,
it is isomorphic (in C) to the original X.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Subobject.arrow
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(Y : CategoryTheory.Subobject X)
:
CategoryTheory.Subobject.underlying.obj Y ⟶ X
The morphism in C from the arbitrarily chosen underlying object to the ambient object.
Equations
- Y.arrow = (CategoryTheory.Subobject.representative.obj Y).obj.hom
Instances For
instance
CategoryTheory.Subobject.arrow_mono
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(Y : CategoryTheory.Subobject X)
:
CategoryTheory.Mono Y.arrow
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Subobject.arrow_congr
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : C}
(X : CategoryTheory.Subobject A)
(Y : CategoryTheory.Subobject A)
(h : X = Y)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) Y.arrow = X.arrow
@[simp]
theorem
CategoryTheory.Subobject.representative_coe
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(Y : CategoryTheory.Subobject X)
:
(CategoryTheory.Subobject.representative.obj Y).obj.left = CategoryTheory.Subobject.underlying.obj Y
@[simp]
theorem
CategoryTheory.Subobject.representative_arrow
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(Y : CategoryTheory.Subobject X)
:
(CategoryTheory.Subobject.representative.obj Y).arrow = Y.arrow
@[simp]
theorem
CategoryTheory.Subobject.underlying_arrow_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : CategoryTheory.Subobject X}
{Z : CategoryTheory.Subobject X}
(f : Y ⟶ Z✝)
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlying.map f)
(CategoryTheory.CategoryStruct.comp Z✝.arrow h) = CategoryTheory.CategoryStruct.comp Y.arrow h
@[simp]
theorem
CategoryTheory.Subobject.underlying_arrow
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : CategoryTheory.Subobject X}
{Z : CategoryTheory.Subobject X}
(f : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlying.map f) Z.arrow = Y.arrow
@[simp]
theorem
CategoryTheory.Subobject.underlyingIso_arrow_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Subobject.underlyingIso_arrow_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).obj X)
:
(CategoryTheory.Subobject.mk f).arrow ((CategoryTheory.Subobject.underlyingIso f).inv x) = f x
@[simp]
theorem
CategoryTheory.Subobject.underlyingIso_arrow
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
@[simp]
theorem
CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
theorem
CategoryTheory.Subobject.eq_of_comp_arrow_eq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{P : CategoryTheory.Subobject Y}
{f : X ⟶ CategoryTheory.Subobject.underlying.obj P}
{g : X ⟶ CategoryTheory.Subobject.underlying.obj P}
(h : CategoryTheory.CategoryStruct.comp f P.arrow = CategoryTheory.CategoryStruct.comp g P.arrow)
:
f = g
Two morphisms into a subobject are equal exactly if the morphisms into the ambient object are equal
theorem
CategoryTheory.Subobject.mk_le_mk_of_comm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
{f₁ : A₁ ⟶ B}
{f₂ : A₂ ⟶ B}
[CategoryTheory.Mono f₁]
[CategoryTheory.Mono f₂]
(g : A₁ ⟶ A₂)
(w : CategoryTheory.CategoryStruct.comp g f₂ = f₁)
:
@[simp]
theorem
CategoryTheory.Subobject.mk_arrow
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(P : CategoryTheory.Subobject X)
:
CategoryTheory.Subobject.mk P.arrow = P
theorem
CategoryTheory.Subobject.le_of_comm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{X : CategoryTheory.Subobject B}
{Y : CategoryTheory.Subobject B}
(f : CategoryTheory.Subobject.underlying.obj X ⟶ CategoryTheory.Subobject.underlying.obj Y)
(w : CategoryTheory.CategoryStruct.comp f Y.arrow = X.arrow)
:
X ≤ Y
theorem
CategoryTheory.Subobject.le_mk_of_comm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
{X : CategoryTheory.Subobject B}
{f : A ⟶ B}
[CategoryTheory.Mono f]
(g : CategoryTheory.Subobject.underlying.obj X ⟶ A)
(w : CategoryTheory.CategoryStruct.comp g f = X.arrow)
:
theorem
CategoryTheory.Subobject.mk_le_of_comm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
{X : CategoryTheory.Subobject B}
{f : A ⟶ B}
[CategoryTheory.Mono f]
(g : A ⟶ CategoryTheory.Subobject.underlying.obj X)
(w : CategoryTheory.CategoryStruct.comp g X.arrow = f)
:
theorem
CategoryTheory.Subobject.eq_of_comm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{X : CategoryTheory.Subobject B}
{Y : CategoryTheory.Subobject B}
(f : CategoryTheory.Subobject.underlying.obj X ≅ CategoryTheory.Subobject.underlying.obj Y)
(w : CategoryTheory.CategoryStruct.comp f.hom Y.arrow = X.arrow)
:
X = Y
To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with the arrows.
theorem
CategoryTheory.Subobject.eq_mk_of_comm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
{X : CategoryTheory.Subobject B}
(f : A ⟶ B)
[CategoryTheory.Mono f]
(i : CategoryTheory.Subobject.underlying.obj X ≅ A)
(w : CategoryTheory.CategoryStruct.comp i.hom f = X.arrow)
:
To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with the arrows.
theorem
CategoryTheory.Subobject.mk_eq_of_comm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
{X : CategoryTheory.Subobject B}
(f : A ⟶ B)
[CategoryTheory.Mono f]
(i : A ≅ CategoryTheory.Subobject.underlying.obj X)
(w : CategoryTheory.CategoryStruct.comp i.hom X.arrow = f)
:
To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with the arrows.
theorem
CategoryTheory.Subobject.mk_eq_mk_of_comm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
(f : A₁ ⟶ B)
(g : A₂ ⟶ B)
[CategoryTheory.Mono f]
[CategoryTheory.Mono g]
(i : A₁ ≅ A₂)
(w : CategoryTheory.CategoryStruct.comp i.hom g = f)
:
To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with the arrows.
def
CategoryTheory.Subobject.ofLE
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
(X : CategoryTheory.Subobject B)
(Y : CategoryTheory.Subobject B)
(h : X ≤ Y)
:
CategoryTheory.Subobject.underlying.obj X ⟶ CategoryTheory.Subobject.underlying.obj Y
An inequality of subobjects is witnessed by some morphism between the corresponding objects.
Equations
- X.ofLE Y h = CategoryTheory.Subobject.underlying.map h.hom
Instances For
@[simp]
theorem
CategoryTheory.Subobject.ofLE_arrow_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{X : CategoryTheory.Subobject B}
{Y : CategoryTheory.Subobject B}
(h : X ≤ Y)
{Z : C}
(h : B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (X.ofLE Y h✝) (CategoryTheory.CategoryStruct.comp Y.arrow h) = CategoryTheory.CategoryStruct.comp X.arrow h
@[simp]
theorem
CategoryTheory.Subobject.ofLE_arrow
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{X : CategoryTheory.Subobject B}
{Y : CategoryTheory.Subobject B}
(h : X ≤ Y)
:
CategoryTheory.CategoryStruct.comp (X.ofLE Y h) Y.arrow = X.arrow
instance
CategoryTheory.Subobject.instMonoOfLE
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
(X : CategoryTheory.Subobject B)
(Y : CategoryTheory.Subobject B)
(h : X ≤ Y)
:
CategoryTheory.Mono (X.ofLE Y h)
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Subobject.ofLE_mk_le_mk_of_comm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
{f₁ : A₁ ⟶ B}
{f₂ : A₂ ⟶ B}
[CategoryTheory.Mono f₁]
[CategoryTheory.Mono f₂]
(g : A₁ ⟶ A₂)
(w : CategoryTheory.CategoryStruct.comp g f₂ = f₁)
:
def
CategoryTheory.Subobject.ofLEMk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
(X : CategoryTheory.Subobject B)
(f : A ⟶ B)
[CategoryTheory.Mono f]
(h : X ≤ CategoryTheory.Subobject.mk f)
:
CategoryTheory.Subobject.underlying.obj X ⟶ A
An inequality of subobjects is witnessed by some morphism between the corresponding objects.
Equations
- X.ofLEMk f h = CategoryTheory.CategoryStruct.comp (X.ofLE (CategoryTheory.Subobject.mk f) h) (CategoryTheory.Subobject.underlyingIso f).hom
Instances For
instance
CategoryTheory.Subobject.instMonoOfLEMk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
(X : CategoryTheory.Subobject B)
(f : A ⟶ B)
[CategoryTheory.Mono f]
(h : X ≤ CategoryTheory.Subobject.mk f)
:
CategoryTheory.Mono (X.ofLEMk f h)
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Subobject.ofLEMk_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
{X : CategoryTheory.Subobject B}
{f : A ⟶ B}
[CategoryTheory.Mono f]
(h : X ≤ CategoryTheory.Subobject.mk f)
:
CategoryTheory.CategoryStruct.comp (X.ofLEMk f h) f = X.arrow
def
CategoryTheory.Subobject.ofMkLE
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
(f : A ⟶ B)
[CategoryTheory.Mono f]
(X : CategoryTheory.Subobject B)
(h : CategoryTheory.Subobject.mk f ≤ X)
:
A ⟶ CategoryTheory.Subobject.underlying.obj X
An inequality of subobjects is witnessed by some morphism between the corresponding objects.
Equations
- CategoryTheory.Subobject.ofMkLE f X h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso f).inv ((CategoryTheory.Subobject.mk f).ofLE X h)
Instances For
instance
CategoryTheory.Subobject.instMonoOfMkLE
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
(f : A ⟶ B)
[CategoryTheory.Mono f]
(X : CategoryTheory.Subobject B)
(h : CategoryTheory.Subobject.mk f ≤ X)
:
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Subobject.ofMkLE_arrow
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
{f : A ⟶ B}
[CategoryTheory.Mono f]
{X : CategoryTheory.Subobject B}
(h : CategoryTheory.Subobject.mk f ≤ X)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f X h) X.arrow = f
def
CategoryTheory.Subobject.ofMkLEMk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
(f : A₁ ⟶ B)
(g : A₂ ⟶ B)
[CategoryTheory.Mono f]
[CategoryTheory.Mono g]
(h : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g)
:
A₁ ⟶ A₂
An inequality of subobjects is witnessed by some morphism between the corresponding objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.Subobject.instMonoOfMkLEMk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
(f : A₁ ⟶ B)
(g : A₂ ⟶ B)
[CategoryTheory.Mono f]
[CategoryTheory.Mono g]
(h : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g)
:
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Subobject.ofMkLEMk_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
{f : A₁ ⟶ B}
{g : A₂ ⟶ B}
[CategoryTheory.Mono f]
[CategoryTheory.Mono g]
(h : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g)
:
@[simp]
theorem
CategoryTheory.Subobject.ofLE_comp_ofLE_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
(X : CategoryTheory.Subobject B)
(Y : CategoryTheory.Subobject B)
(Z : CategoryTheory.Subobject B)
(h₁ : X ≤ Y)
(h₂ : Y ≤ Z✝)
{Z : C}
(h : CategoryTheory.Subobject.underlying.obj Z✝ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (X.ofLE Y h₁) (CategoryTheory.CategoryStruct.comp (Y.ofLE Z✝ h₂) h) = CategoryTheory.CategoryStruct.comp (X.ofLE Z✝ ⋯) h
@[simp]
theorem
CategoryTheory.Subobject.ofLE_comp_ofLE
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
(X : CategoryTheory.Subobject B)
(Y : CategoryTheory.Subobject B)
(Z : CategoryTheory.Subobject B)
(h₁ : X ≤ Y)
(h₂ : Y ≤ Z)
:
CategoryTheory.CategoryStruct.comp (X.ofLE Y h₁) (Y.ofLE Z h₂) = X.ofLE Z ⋯
@[simp]
theorem
CategoryTheory.Subobject.ofLE_comp_ofLEMk_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
(X : CategoryTheory.Subobject B)
(Y : CategoryTheory.Subobject B)
(f : A ⟶ B)
[CategoryTheory.Mono f]
(h₁ : X ≤ Y)
(h₂ : Y ≤ CategoryTheory.Subobject.mk f)
{Z : C}
(h : A ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (X.ofLE Y h₁) (CategoryTheory.CategoryStruct.comp (Y.ofLEMk f h₂) h) = CategoryTheory.CategoryStruct.comp (X.ofLEMk f ⋯) h
@[simp]
theorem
CategoryTheory.Subobject.ofLE_comp_ofLEMk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
(X : CategoryTheory.Subobject B)
(Y : CategoryTheory.Subobject B)
(f : A ⟶ B)
[CategoryTheory.Mono f]
(h₁ : X ≤ Y)
(h₂ : Y ≤ CategoryTheory.Subobject.mk f)
:
CategoryTheory.CategoryStruct.comp (X.ofLE Y h₁) (Y.ofLEMk f h₂) = X.ofLEMk f ⋯
@[simp]
theorem
CategoryTheory.Subobject.ofLEMk_comp_ofMkLE_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
(X : CategoryTheory.Subobject B)
(f : A ⟶ B)
[CategoryTheory.Mono f]
(Y : CategoryTheory.Subobject B)
(h₁ : X ≤ CategoryTheory.Subobject.mk f)
(h₂ : CategoryTheory.Subobject.mk f ≤ Y)
{Z : C}
(h : CategoryTheory.Subobject.underlying.obj Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (X.ofLEMk f h₁)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f Y h₂) h) = CategoryTheory.CategoryStruct.comp (X.ofLE Y ⋯) h
@[simp]
theorem
CategoryTheory.Subobject.ofLEMk_comp_ofMkLE
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
(X : CategoryTheory.Subobject B)
(f : A ⟶ B)
[CategoryTheory.Mono f]
(Y : CategoryTheory.Subobject B)
(h₁ : X ≤ CategoryTheory.Subobject.mk f)
(h₂ : CategoryTheory.Subobject.mk f ≤ Y)
:
CategoryTheory.CategoryStruct.comp (X.ofLEMk f h₁) (CategoryTheory.Subobject.ofMkLE f Y h₂) = X.ofLE Y ⋯
@[simp]
theorem
CategoryTheory.Subobject.ofLEMk_comp_ofMkLEMk_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
(X : CategoryTheory.Subobject B)
(f : A₁ ⟶ B)
[CategoryTheory.Mono f]
(g : A₂ ⟶ B)
[CategoryTheory.Mono g]
(h₁ : X ≤ CategoryTheory.Subobject.mk f)
(h₂ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g)
{Z : C}
(h : A₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (X.ofLEMk f h₁)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk f g h₂) h) = CategoryTheory.CategoryStruct.comp (X.ofLEMk g ⋯) h
@[simp]
theorem
CategoryTheory.Subobject.ofLEMk_comp_ofMkLEMk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
(X : CategoryTheory.Subobject B)
(f : A₁ ⟶ B)
[CategoryTheory.Mono f]
(g : A₂ ⟶ B)
[CategoryTheory.Mono g]
(h₁ : X ≤ CategoryTheory.Subobject.mk f)
(h₂ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g)
:
CategoryTheory.CategoryStruct.comp (X.ofLEMk f h₁) (CategoryTheory.Subobject.ofMkLEMk f g h₂) = X.ofLEMk g ⋯
@[simp]
theorem
CategoryTheory.Subobject.ofMkLE_comp_ofLE_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
(f : A₁ ⟶ B)
[CategoryTheory.Mono f]
(X : CategoryTheory.Subobject B)
(Y : CategoryTheory.Subobject B)
(h₁ : CategoryTheory.Subobject.mk f ≤ X)
(h₂ : X ≤ Y)
{Z : C}
(h : CategoryTheory.Subobject.underlying.obj Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f X h₁)
(CategoryTheory.CategoryStruct.comp (X.ofLE Y h₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f Y ⋯) h
@[simp]
theorem
CategoryTheory.Subobject.ofMkLE_comp_ofLE
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
(f : A₁ ⟶ B)
[CategoryTheory.Mono f]
(X : CategoryTheory.Subobject B)
(Y : CategoryTheory.Subobject B)
(h₁ : CategoryTheory.Subobject.mk f ≤ X)
(h₂ : X ≤ Y)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f X h₁) (X.ofLE Y h₂) = CategoryTheory.Subobject.ofMkLE f Y ⋯
@[simp]
theorem
CategoryTheory.Subobject.ofMkLE_comp_ofLEMk_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
(f : A₁ ⟶ B)
[CategoryTheory.Mono f]
(X : CategoryTheory.Subobject B)
(g : A₂ ⟶ B)
[CategoryTheory.Mono g]
(h₁ : CategoryTheory.Subobject.mk f ≤ X)
(h₂ : X ≤ CategoryTheory.Subobject.mk g)
{Z : C}
(h : A₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f X h₁)
(CategoryTheory.CategoryStruct.comp (X.ofLEMk g h₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk f g ⋯) h
@[simp]
theorem
CategoryTheory.Subobject.ofMkLE_comp_ofLEMk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
(f : A₁ ⟶ B)
[CategoryTheory.Mono f]
(X : CategoryTheory.Subobject B)
(g : A₂ ⟶ B)
[CategoryTheory.Mono g]
(h₁ : CategoryTheory.Subobject.mk f ≤ X)
(h₂ : X ≤ CategoryTheory.Subobject.mk g)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f X h₁) (X.ofLEMk g h₂) = CategoryTheory.Subobject.ofMkLEMk f g ⋯
@[simp]
theorem
CategoryTheory.Subobject.ofMkLEMk_comp_ofMkLE_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
(f : A₁ ⟶ B)
[CategoryTheory.Mono f]
(g : A₂ ⟶ B)
[CategoryTheory.Mono g]
(X : CategoryTheory.Subobject B)
(h₁ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g)
(h₂ : CategoryTheory.Subobject.mk g ≤ X)
{Z : C}
(h : CategoryTheory.Subobject.underlying.obj X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Subobject.ofMkLEMk_comp_ofMkLE
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
(f : A₁ ⟶ B)
[CategoryTheory.Mono f]
(g : A₂ ⟶ B)
[CategoryTheory.Mono g]
(X : CategoryTheory.Subobject B)
(h₁ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g)
(h₂ : CategoryTheory.Subobject.mk g ≤ X)
:
@[simp]
theorem
CategoryTheory.Subobject.ofMkLEMk_comp_ofMkLEMk_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
{A₃ : C}
(f : A₁ ⟶ B)
[CategoryTheory.Mono f]
(g : A₂ ⟶ B)
[CategoryTheory.Mono g]
(h : A₃ ⟶ B)
[CategoryTheory.Mono h✝]
(h₁ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g)
(h₂ : CategoryTheory.Subobject.mk g ≤ CategoryTheory.Subobject.mk h✝)
{Z : C}
(h : A₃ ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Subobject.ofMkLEMk_comp_ofMkLEMk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
{A₃ : C}
(f : A₁ ⟶ B)
[CategoryTheory.Mono f]
(g : A₂ ⟶ B)
[CategoryTheory.Mono g]
(h : A₃ ⟶ B)
[CategoryTheory.Mono h]
(h₁ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g)
(h₂ : CategoryTheory.Subobject.mk g ≤ CategoryTheory.Subobject.mk h)
:
@[simp]
theorem
CategoryTheory.Subobject.ofLE_refl
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
(X : CategoryTheory.Subobject B)
:
X.ofLE X ⋯ = CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.obj X)
@[simp]
theorem
CategoryTheory.Subobject.ofMkLEMk_refl
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
(f : A₁ ⟶ B)
[CategoryTheory.Mono f]
:
@[simp]
theorem
CategoryTheory.Subobject.isoOfEq_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
(X : CategoryTheory.Subobject B)
(Y : CategoryTheory.Subobject B)
(h : X = Y)
:
(X.isoOfEq Y h).inv = Y.ofLE X ⋯
@[simp]
theorem
CategoryTheory.Subobject.isoOfEq_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
(X : CategoryTheory.Subobject B)
(Y : CategoryTheory.Subobject B)
(h : X = Y)
:
(X.isoOfEq Y h).hom = X.ofLE Y ⋯
def
CategoryTheory.Subobject.isoOfEq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
(X : CategoryTheory.Subobject B)
(Y : CategoryTheory.Subobject B)
(h : X = Y)
:
CategoryTheory.Subobject.underlying.obj X ≅ CategoryTheory.Subobject.underlying.obj Y
An equality of subobjects gives an isomorphism of the corresponding objects.
(One could use underlying.mapIso (eqToIso h)) here, but this is more readable.)
Equations
- X.isoOfEq Y h = { hom := X.ofLE Y ⋯, inv := Y.ofLE X ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Subobject.isoOfEqMk_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
(X : CategoryTheory.Subobject B)
(f : A ⟶ B)
[CategoryTheory.Mono f]
(h : X = CategoryTheory.Subobject.mk f)
:
(X.isoOfEqMk f h).inv = CategoryTheory.Subobject.ofMkLE f X ⋯
@[simp]
theorem
CategoryTheory.Subobject.isoOfEqMk_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
(X : CategoryTheory.Subobject B)
(f : A ⟶ B)
[CategoryTheory.Mono f]
(h : X = CategoryTheory.Subobject.mk f)
:
(X.isoOfEqMk f h).hom = X.ofLEMk f ⋯
def
CategoryTheory.Subobject.isoOfEqMk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
(X : CategoryTheory.Subobject B)
(f : A ⟶ B)
[CategoryTheory.Mono f]
(h : X = CategoryTheory.Subobject.mk f)
:
CategoryTheory.Subobject.underlying.obj X ≅ A
An equality of subobjects gives an isomorphism of the corresponding objects.
Equations
- X.isoOfEqMk f h = { hom := X.ofLEMk f ⋯, inv := CategoryTheory.Subobject.ofMkLE f X ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Subobject.isoOfMkEq_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
(f : A ⟶ B)
[CategoryTheory.Mono f]
(X : CategoryTheory.Subobject B)
(h : CategoryTheory.Subobject.mk f = X)
:
(CategoryTheory.Subobject.isoOfMkEq f X h).inv = X.ofLEMk f ⋯
@[simp]
theorem
CategoryTheory.Subobject.isoOfMkEq_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
(f : A ⟶ B)
[CategoryTheory.Mono f]
(X : CategoryTheory.Subobject B)
(h : CategoryTheory.Subobject.mk f = X)
:
(CategoryTheory.Subobject.isoOfMkEq f X h).hom = CategoryTheory.Subobject.ofMkLE f X ⋯
def
CategoryTheory.Subobject.isoOfMkEq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A : C}
(f : A ⟶ B)
[CategoryTheory.Mono f]
(X : CategoryTheory.Subobject B)
(h : CategoryTheory.Subobject.mk f = X)
:
A ≅ CategoryTheory.Subobject.underlying.obj X
An equality of subobjects gives an isomorphism of the corresponding objects.
Equations
- CategoryTheory.Subobject.isoOfMkEq f X h = { hom := CategoryTheory.Subobject.ofMkLE f X ⋯, inv := X.ofLEMk f ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Subobject.isoOfMkEqMk_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
(f : A₁ ⟶ B)
(g : A₂ ⟶ B)
[CategoryTheory.Mono f]
[CategoryTheory.Mono g]
(h : CategoryTheory.Subobject.mk f = CategoryTheory.Subobject.mk g)
:
(CategoryTheory.Subobject.isoOfMkEqMk f g h).inv = CategoryTheory.Subobject.ofMkLEMk g f ⋯
@[simp]
theorem
CategoryTheory.Subobject.isoOfMkEqMk_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
(f : A₁ ⟶ B)
(g : A₂ ⟶ B)
[CategoryTheory.Mono f]
[CategoryTheory.Mono g]
(h : CategoryTheory.Subobject.mk f = CategoryTheory.Subobject.mk g)
:
(CategoryTheory.Subobject.isoOfMkEqMk f g h).hom = CategoryTheory.Subobject.ofMkLEMk f g ⋯
def
CategoryTheory.Subobject.isoOfMkEqMk
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{B : C}
{A₁ : C}
{A₂ : C}
(f : A₁ ⟶ B)
(g : A₂ ⟶ B)
[CategoryTheory.Mono f]
[CategoryTheory.Mono g]
(h : CategoryTheory.Subobject.mk f = CategoryTheory.Subobject.mk g)
:
A₁ ≅ A₂
An equality of subobjects gives an isomorphism of the corresponding objects.
Equations
- CategoryTheory.Subobject.isoOfMkEqMk f g h = { hom := CategoryTheory.Subobject.ofMkLEMk f g ⋯, inv := CategoryTheory.Subobject.ofMkLEMk g f ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
def
CategoryTheory.Subobject.lower
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{Y : D}
(F : CategoryTheory.Functor (CategoryTheory.MonoOver X) (CategoryTheory.MonoOver Y))
:
Any functor MonoOver X ⥤ MonoOver Y descends to a functor
Subobject X ⥤ Subobject Y, because MonoOver Y is thin.
Instances For
theorem
CategoryTheory.Subobject.lower_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(F₁ : CategoryTheory.Functor (CategoryTheory.MonoOver X) (CategoryTheory.MonoOver Y))
(F₂ : CategoryTheory.Functor (CategoryTheory.MonoOver X) (CategoryTheory.MonoOver Y))
(h : F₁ ≅ F₂)
:
Isomorphic functors become equal when lowered to Subobject.
(It's not as evil as usual to talk about equality between functors
because the categories are thin and skeletal.)
def
CategoryTheory.Subobject.lower₂
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{Z : C}
(F : CategoryTheory.Functor (CategoryTheory.MonoOver X)
(CategoryTheory.Functor (CategoryTheory.MonoOver Y) (CategoryTheory.MonoOver Z)))
:
A ternary version of Subobject.lower.
Instances For
@[simp]
theorem
CategoryTheory.Subobject.lower_comm
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(F : CategoryTheory.Functor (CategoryTheory.MonoOver Y) (CategoryTheory.MonoOver X))
:
def
CategoryTheory.Subobject.lowerAdjunction
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{A : C}
{B : D}
{L : CategoryTheory.Functor (CategoryTheory.MonoOver A) (CategoryTheory.MonoOver B)}
{R : CategoryTheory.Functor (CategoryTheory.MonoOver B) (CategoryTheory.MonoOver A)}
(h : L ⊣ R)
:
An adjunction between MonoOver A and MonoOver B gives an adjunction
between Subobject A and Subobject B.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Subobject.lowerEquivalence_functor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{A : C}
{B : D}
(e : CategoryTheory.MonoOver A ≌ CategoryTheory.MonoOver B)
:
(CategoryTheory.Subobject.lowerEquivalence e).functor = CategoryTheory.Subobject.lower e.functor
@[simp]
theorem
CategoryTheory.Subobject.lowerEquivalence_unitIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{A : C}
{B : D}
(e : CategoryTheory.MonoOver A ≌ CategoryTheory.MonoOver B)
:
(CategoryTheory.Subobject.lowerEquivalence e).unitIso = CategoryTheory.eqToIso ⋯
@[simp]
theorem
CategoryTheory.Subobject.lowerEquivalence_counitIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{A : C}
{B : D}
(e : CategoryTheory.MonoOver A ≌ CategoryTheory.MonoOver B)
:
(CategoryTheory.Subobject.lowerEquivalence e).counitIso = CategoryTheory.eqToIso ⋯
@[simp]
theorem
CategoryTheory.Subobject.lowerEquivalence_inverse
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{A : C}
{B : D}
(e : CategoryTheory.MonoOver A ≌ CategoryTheory.MonoOver B)
:
(CategoryTheory.Subobject.lowerEquivalence e).inverse = CategoryTheory.Subobject.lower e.inverse
def
CategoryTheory.Subobject.lowerEquivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{A : C}
{B : D}
(e : CategoryTheory.MonoOver A ≌ CategoryTheory.MonoOver B)
:
An equivalence between MonoOver A and MonoOver B gives an equivalence
between Subobject A and Subobject B.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Subobject.pullback
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
(f : X ⟶ Y)
:
When C has pullbacks, a morphism f : X ⟶ Y induces a functor Subobject Y ⥤ Subobject X,
by pulling back a monomorphism along f.
Equations
Instances For
theorem
CategoryTheory.Subobject.pullback_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
[CategoryTheory.Limits.HasPullbacks C]
(x : CategoryTheory.Subobject X)
:
theorem
CategoryTheory.Subobject.pullback_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{Z : C}
[CategoryTheory.Limits.HasPullbacks C]
(f : X ⟶ Y)
(g : Y ⟶ Z)
(x : CategoryTheory.Subobject Z)
:
(CategoryTheory.Subobject.pullback (CategoryTheory.CategoryStruct.comp f g)).obj x = (CategoryTheory.Subobject.pullback f).obj ((CategoryTheory.Subobject.pullback g).obj x)
instance
CategoryTheory.Subobject.instFaithfulPullback
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
(f : X ⟶ Y)
:
(CategoryTheory.Subobject.pullback f).Faithful
Equations
- ⋯ = ⋯
def
CategoryTheory.Subobject.map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
We can map subobjects of X to subobjects of Y
by post-composition with a monomorphism f : X ⟶ Y.
Equations
Instances For
theorem
CategoryTheory.Subobject.map_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(x : CategoryTheory.Subobject X)
:
(CategoryTheory.Subobject.map (CategoryTheory.CategoryStruct.id X)).obj x = x
theorem
CategoryTheory.Subobject.map_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Mono f]
[CategoryTheory.Mono g]
(x : CategoryTheory.Subobject X)
:
(CategoryTheory.Subobject.map (CategoryTheory.CategoryStruct.comp f g)).obj x = (CategoryTheory.Subobject.map g).obj ((CategoryTheory.Subobject.map f).obj x)
def
CategoryTheory.Subobject.mapIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A : C}
{B : C}
(e : A ≅ B)
:
Isomorphic objects have equivalent subobject lattices.
Equations
Instances For
def
CategoryTheory.Subobject.mapIsoToOrderIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(e : X ≅ Y)
:
In fact, there's a type level bijection between the subobjects of isomorphic objects, which preserves the order.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Subobject.mapIsoToOrderIso_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(e : X ≅ Y)
(P : CategoryTheory.Subobject X)
:
(CategoryTheory.Subobject.mapIsoToOrderIso e) P = (CategoryTheory.Subobject.map e.hom).obj P
@[simp]
theorem
CategoryTheory.Subobject.mapIsoToOrderIso_symm_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(e : X ≅ Y)
(Q : CategoryTheory.Subobject Y)
:
(CategoryTheory.Subobject.mapIsoToOrderIso e).symm Q = (CategoryTheory.Subobject.map e.inv).obj Q
def
CategoryTheory.Subobject.mapPullbackAdj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
map f : Subobject X ⥤ Subobject Y is
the left adjoint of pullback f : Subobject Y ⥤ Subobject X.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Subobject.pullback_map_self
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
(f : X ⟶ Y)
[CategoryTheory.Mono f]
(g : CategoryTheory.Subobject X)
:
(CategoryTheory.Subobject.pullback f).obj ((CategoryTheory.Subobject.map f).obj g) = g
theorem
CategoryTheory.Subobject.map_pullback
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
{W : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{h : Y ⟶ W}
{k : Z ⟶ W}
[CategoryTheory.Mono h]
[CategoryTheory.Mono g]
(comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
(t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk f g comm))
(p : CategoryTheory.Subobject Y)
:
(CategoryTheory.Subobject.map g).obj ((CategoryTheory.Subobject.pullback f).obj p) = (CategoryTheory.Subobject.pullback k).obj ((CategoryTheory.Subobject.map h).obj p)
def
CategoryTheory.Subobject.exists
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasImages C]
(f : X ⟶ Y)
:
The functor from subobjects of X to subobjects of Y given by
sending the subobject S to its "image" under f, usually denoted $\exists_f$.
For instance, when C is the category of types,
viewing Subobject X as Set X this is just Set.image f.
This functor is left adjoint to the pullback f functor (shown in existsPullbackAdj)
provided both are defined, and generalises the map f functor, again provided it is defined.
Equations
Instances For
theorem
CategoryTheory.Subobject.exists_iso_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasImages C]
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
When f : X ⟶ Y is a monomorphism, exists f agrees with map f.
def
CategoryTheory.Subobject.existsPullbackAdj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasImages C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasPullbacks C]
:
exists f : Subobject X ⥤ Subobject Y is
left adjoint to pullback f : Subobject Y ⥤ Subobject X.