Specific subobjects #
We define equalizerSubobject, kernelSubobject and imageSubobject, which are the subobjects
represented by the equalizer, kernel and image of (a pair of) morphism(s) and provide conditions
for P.factors f, where P is one of these special subobjects.
TODO: Add conditions for when P is a pullback subobject.
TODO: an iff characterisation of (imageSubobject f).Factors h
@[inline, reducible]
abbrev
CategoryTheory.Limits.equalizerSubobject
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
:
The equalizer of morphisms f g : X ⟶ Y as a Subobject X.
Instances For
def
CategoryTheory.Limits.equalizerSubobjectIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
:
CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.equalizerSubobject f g) ≅ CategoryTheory.Limits.equalizer f g
The underlying object of equalizerSubobject f g is (up to isomorphism!)
the same as the chosen object equalizer f g.
Instances For
@[simp]
theorem
CategoryTheory.Limits.equalizerSubobject_arrow_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.equalizerSubobject_arrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
:
@[simp]
theorem
CategoryTheory.Limits.equalizerSubobject_arrow'_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.equalizerSubobject_arrow'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
:
theorem
CategoryTheory.Limits.equalizerSubobject_arrow_comp_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (CategoryTheory.Limits.equalizerSubobject f g))
(CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (CategoryTheory.Limits.equalizerSubobject f g))
(CategoryTheory.CategoryStruct.comp g h)
theorem
CategoryTheory.Limits.equalizerSubobject_arrow_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
:
theorem
CategoryTheory.Limits.equalizerSubobject_factors
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
{W : C}
(h : W ⟶ X)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g)
:
theorem
CategoryTheory.Limits.equalizerSubobject_factors_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasEqualizer f g]
{W : C}
(h : W ⟶ X)
:
@[inline, reducible]
abbrev
CategoryTheory.Limits.kernelSubobject
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
:
The kernel of a morphism f : X ⟶ Y as a Subobject X.
Instances For
def
CategoryTheory.Limits.kernelSubobjectIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
:
CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f) ≅ CategoryTheory.Limits.kernel f
The underlying object of kernelSubobject f is (up to isomorphism!)
the same as the chosen object kernel f.
Instances For
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).obj
(CategoryTheory.Subobject.underlying.obj (CategoryTheory.Subobject.mk (CategoryTheory.Limits.kernel.ι f))))
:
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
:
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow'_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow'_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.kernel f))
:
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
:
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow_comp_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow_comp_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f)))
:
↑f (↑(CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject f)) x) = ↑0 x
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
:
theorem
CategoryTheory.Limits.kernelSubobject_factors
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{W : C}
(h : W ⟶ X)
(w : CategoryTheory.CategoryStruct.comp h f = 0)
:
theorem
CategoryTheory.Limits.kernelSubobject_factors_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{W : C}
(h : W ⟶ X)
:
def
CategoryTheory.Limits.factorThruKernelSubobject
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{W : C}
(h : W ⟶ X)
(w : CategoryTheory.CategoryStruct.comp h f = 0)
:
W ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f)
A factorisation of h : W ⟶ X through kernelSubobject f, assuming h ≫ f = 0.
Instances For
@[simp]
theorem
CategoryTheory.Limits.factorThruKernelSubobject_comp_arrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{W : C}
(h : W ⟶ X)
(w : CategoryTheory.CategoryStruct.comp h f = 0)
:
@[simp]
theorem
CategoryTheory.Limits.factorThruKernelSubobject_comp_kernelSubobjectIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{W : C}
(h : W ⟶ X)
(w : CategoryTheory.CategoryStruct.comp h f = 0)
:
def
CategoryTheory.Limits.kernelSubobjectMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
{f : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
{X' : C}
{Y' : C}
{f' : X' ⟶ Y'}
[CategoryTheory.Limits.HasKernel f']
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
:
CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f) ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f')
A commuting square induces a morphism between the kernel subobjects.
Instances For
@[simp]
theorem
CategoryTheory.Limits.kernelSubobjectMap_arrow_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
{f : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
{X' : C}
{Y' : C}
{f' : X' ⟶ Y'}
[CategoryTheory.Limits.HasKernel f']
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
{Z : C}
(h : X' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject f')) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject f))
(CategoryTheory.CategoryStruct.comp sq.left h)
@[simp]
theorem
CategoryTheory.Limits.kernelSubobjectMap_arrow_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
{f : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
{X' : C}
{Y' : C}
{f' : X' ⟶ Y'}
[CategoryTheory.Limits.HasKernel f']
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f)))
:
↑(CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject f'))
(↑(CategoryTheory.Subobject.factorThru (CategoryTheory.Limits.kernelSubobject f')
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject f))
sq.left)
(_ :
CategoryTheory.Subobject.Factors (CategoryTheory.Limits.kernelSubobject f')
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject f)) sq.left)))
x) = ↑sq.left (↑(CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject f)) x)
@[simp]
theorem
CategoryTheory.Limits.kernelSubobjectMap_arrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
{f : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
{X' : C}
{Y' : C}
{f' : X' ⟶ Y'}
[CategoryTheory.Limits.HasKernel f']
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
:
@[simp]
theorem
CategoryTheory.Limits.kernelSubobjectMap_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
{f : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
:
CategoryTheory.Limits.kernelSubobjectMap (CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk f)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f))
@[simp]
theorem
CategoryTheory.Limits.kernelSubobjectMap_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
{f : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
{X' : C}
{Y' : C}
{f' : X' ⟶ Y'}
[CategoryTheory.Limits.HasKernel f']
{X'' : C}
{Y'' : C}
{f'' : X'' ⟶ Y''}
[CategoryTheory.Limits.HasKernel f'']
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
(sq' : CategoryTheory.Arrow.mk f' ⟶ CategoryTheory.Arrow.mk f'')
:
theorem
CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
{f : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
{X' : C}
{Y' : C}
{f' : X' ⟶ Y'}
[CategoryTheory.Limits.HasKernel f']
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
{Z : C}
(h : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f') ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.kernel.map f f' sq.left sq.right
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.mk f).hom
((CategoryTheory.Functor.id C).map sq.right) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id C).map sq.left)
(CategoryTheory.Arrow.mk f').hom))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f').inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq) h)
theorem
CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
{f : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
{X' : C}
{Y' : C}
{f' : X' ⟶ Y'}
[CategoryTheory.Limits.HasKernel f']
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.kernel.map f f' sq.left sq.right
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.mk f).hom
((CategoryTheory.Functor.id C).map sq.right) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id C).map sq.left)
(CategoryTheory.Arrow.mk f').hom))
(CategoryTheory.Limits.kernelSubobjectIso f').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).inv
(CategoryTheory.Limits.kernelSubobjectMap sq)
theorem
CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
{f : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
{X' : C}
{Y' : C}
{f' : X' ⟶ Y'}
[CategoryTheory.Limits.HasKernel f']
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
{Z : C}
(h : CategoryTheory.Limits.kernel f' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.kernel.map f f' sq.left sq.right
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.mk f).hom
((CategoryTheory.Functor.id C).map sq.right) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id C).map sq.left)
(CategoryTheory.Arrow.mk f').hom))
h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f').hom h)
theorem
CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
{f : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
{X' : C}
{Y' : C}
{f' : X' ⟶ Y'}
[CategoryTheory.Limits.HasKernel f']
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).hom
(CategoryTheory.Limits.kernel.map f f' sq.left sq.right
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.mk f).hom
((CategoryTheory.Functor.id C).map sq.right) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id C).map sq.left)
(CategoryTheory.Arrow.mk f').hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq)
(CategoryTheory.Limits.kernelSubobjectIso f').hom
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{A : C}
{B : C}
:
theorem
CategoryTheory.Limits.le_kernelSubobject
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
(A : CategoryTheory.Subobject X)
(h : CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow A) f = 0)
:
def
CategoryTheory.Limits.kernelSubobjectIsoComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
{X' : C}
(f : X' ⟶ X)
[CategoryTheory.IsIso f]
(g : X ⟶ Y)
[CategoryTheory.Limits.HasKernel g]
:
CategoryTheory.Subobject.underlying.obj
(CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f g)) ≅ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g)
The isomorphism between the kernel of f ≫ g and the kernel of g,
when f is an isomorphism.
Instances For
@[simp]
theorem
CategoryTheory.Limits.kernelSubobjectIsoComp_hom_arrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
{X' : C}
(f : X' ⟶ X)
[CategoryTheory.IsIso f]
(g : X ⟶ Y)
[CategoryTheory.Limits.HasKernel g]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIsoComp f g).hom
(CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject g)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f g))) f
@[simp]
theorem
CategoryTheory.Limits.kernelSubobjectIsoComp_inv_arrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
{X' : C}
(f : X' ⟶ X)
[CategoryTheory.IsIso f]
(g : X ⟶ Y)
[CategoryTheory.Limits.HasKernel g]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIsoComp f g).inv
(CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f g))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject g))
(CategoryTheory.inv f)
theorem
CategoryTheory.Limits.kernelSubobject_comp_le
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{Z : C}
(h : Y ⟶ Z)
[CategoryTheory.Limits.HasKernel (CategoryTheory.CategoryStruct.comp f h)]
:
The kernel of f is always a smaller subobject than the kernel of f ≫ h.
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_comp_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{Z : C}
(h : Y ⟶ Z)
[CategoryTheory.Mono h]
:
Postcomposing by a monomorphism does not change the kernel subobject.
instance
CategoryTheory.Limits.kernelSubobject_comp_mono_isIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{Z : C}
(h : Y ⟶ Z)
[CategoryTheory.Mono h]
:
CategoryTheory.IsIso
(CategoryTheory.Subobject.ofLE (CategoryTheory.Limits.kernelSubobject f)
(CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f h))
(_ :
CategoryTheory.Limits.kernelSubobject f ≤ CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f h)))
@[simp]
theorem
CategoryTheory.Limits.cokernelOrderHom_coe
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasCokernels C]
(X : C)
:
∀ (a : CategoryTheory.Subobject X),
↑(CategoryTheory.Limits.cokernelOrderHom X) a = CategoryTheory.Subobject.lift (fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.cokernel.π f).op)
(_ :
∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [hf : CategoryTheory.Mono f] [hg : CategoryTheory.Mono g] (i : A ≅ B),
CategoryTheory.CategoryStruct.comp i.hom g = f →
(fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.cokernel.π f).op) A f hf = (fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.cokernel.π f).op) B g hg)
a
def
CategoryTheory.Limits.cokernelOrderHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasCokernels C]
(X : C)
:
Taking cokernels is an order-reversing map from the subobjects of X to the quotient objects
of X.
Instances For
@[simp]
theorem
CategoryTheory.Limits.kernelOrderHom_coe
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasKernels C]
(X : C)
:
∀ (a : CategoryTheory.Subobject (Opposite.op X)),
↑(CategoryTheory.Limits.kernelOrderHom X) a = CategoryTheory.Subobject.lift (fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.kernel.ι f.unop))
(_ :
∀ ⦃A B : Cᵒᵖ⦄ (f : A ⟶ Opposite.op X) (g : B ⟶ Opposite.op X) [hf : CategoryTheory.Mono f]
[hg : CategoryTheory.Mono g] (i : A ≅ B),
CategoryTheory.CategoryStruct.comp i.hom g = f →
(fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.kernel.ι f.unop)) A f hf = (fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.kernel.ι f.unop)) B g hg)
a
def
CategoryTheory.Limits.kernelOrderHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasKernels C]
(X : C)
:
Taking kernels is an order-reversing map from the quotient objects of X to the subobjects of
X.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.imageSubobject
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
The image of a morphism f g : X ⟶ Y as a Subobject Y.
Instances For
def
CategoryTheory.Limits.imageSubobjectIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ≅ CategoryTheory.Limits.image f
The underlying object of imageSubobject f is (up to isomorphism!)
the same as the chosen object image f.
Instances For
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_arrow_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_arrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_arrow'_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_arrow'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
def
CategoryTheory.Limits.factorThruImageSubobject
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
X ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f)
A factorisation of f : X ⟶ Y through imageSubobject f.
Instances For
instance
CategoryTheory.Limits.instEpiObjSubobjectToQuiverToCategoryStructSmallCategoryToPreorderInstPartialOrderSubobjectToQuiverToCategoryStructToPrefunctorUnderlyingImageSubobjectFactorThruImageSubobject
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.Limits.HasEqualizers C]
:
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_arrow_comp_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_arrow_comp_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).obj X)
:
↑(CategoryTheory.Subobject.arrow (CategoryTheory.Limits.imageSubobject f))
(↑(CategoryTheory.Limits.imageSubobjectIso f).inv (↑(CategoryTheory.Limits.factorThruImage f) x)) = ↑f x
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_arrow_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
theorem
CategoryTheory.Limits.imageSubobject_arrow_comp_eq_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.Epi (CategoryTheory.Limits.factorThruImageSubobject f)]
(h : CategoryTheory.CategoryStruct.comp f g = 0)
:
theorem
CategoryTheory.Limits.imageSubobject_factors_comp_self
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
{W : C}
(k : W ⟶ X)
:
@[simp]
theorem
CategoryTheory.Limits.factorThruImageSubobject_comp_self
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.Subobject.Factors (CategoryTheory.Limits.imageSubobject f) (CategoryTheory.CategoryStruct.comp k f))
:
@[simp]
theorem
CategoryTheory.Limits.factorThruImageSubobject_comp_self_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
{W : C}
{W' : C}
(k : W ⟶ W')
(k' : W' ⟶ X)
(h : CategoryTheory.Subobject.Factors (CategoryTheory.Limits.imageSubobject f)
(CategoryTheory.CategoryStruct.comp k (CategoryTheory.CategoryStruct.comp k' f)))
:
theorem
CategoryTheory.Limits.imageSubobject_comp_le
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{X' : C}
(h : X' ⟶ X)
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp h f)]
:
The image of h ≫ f is always a smaller subobject than the image of f.
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_zero_arrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
:
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{A : C}
{B : C}
:
instance
CategoryTheory.Limits.imageSubobject_comp_le_epi_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasEqualizers C]
{X' : C}
(h : X' ⟶ X)
[CategoryTheory.Epi h]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp h f)]
:
The morphism imageSubobject (h ≫ f) ⟶ imageSubobject f
is an epimorphism when h is an epimorphism.
In general this does not imply that imageSubobject (h ≫ f) = imageSubobject f,
although it will when the ambient category is abelian.
def
CategoryTheory.Limits.imageSubobjectCompIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasEqualizers C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
{Y' : C}
(h : Y ⟶ Y')
[CategoryTheory.IsIso h]
:
CategoryTheory.Subobject.underlying.obj
(CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)) ≅ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f)
Postcomposing by an isomorphism gives an isomorphism between image subobjects.
Instances For
@[simp]
theorem
CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasEqualizers C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
{Y' : C}
(h : Y ⟶ Y')
[CategoryTheory.IsIso h]
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (CategoryTheory.Limits.imageSubobject f)) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Subobject.arrow (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.inv h) h)
@[simp]
theorem
CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasEqualizers C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
{Y' : C}
(h : Y ⟶ Y')
[CategoryTheory.IsIso h]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).hom
(CategoryTheory.Subobject.arrow (CategoryTheory.Limits.imageSubobject f)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Subobject.arrow (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)))
(CategoryTheory.inv h)
@[simp]
theorem
CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasEqualizers C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
{Y' : C}
(h : Y ⟶ Y')
[CategoryTheory.IsIso h]
{Z : C}
(h : Y' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Subobject.arrow (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)))
h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (CategoryTheory.Limits.imageSubobject f))
(CategoryTheory.CategoryStruct.comp h h)
@[simp]
theorem
CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasEqualizers C]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
{Y' : C}
(h : Y ⟶ Y')
[CategoryTheory.IsIso h]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).inv
(CategoryTheory.Subobject.arrow (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (CategoryTheory.Limits.imageSubobject f)) h
theorem
CategoryTheory.Limits.imageSubobject_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
theorem
CategoryTheory.Limits.imageSubobject_iso_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasEqualizers C]
{X' : C}
(h : X' ⟶ X)
[CategoryTheory.IsIso h]
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
:
Precomposing by an isomorphism does not change the image subobject.
theorem
CategoryTheory.Limits.imageSubobject_le
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
{X : CategoryTheory.Subobject B}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(h : A ⟶ CategoryTheory.Subobject.underlying.obj X)
(w : CategoryTheory.CategoryStruct.comp h (CategoryTheory.Subobject.arrow X) = f)
:
theorem
CategoryTheory.Limits.imageSubobject_le_mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : C}
{B : C}
{X : C}
(g : X ⟶ B)
[CategoryTheory.Mono g]
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(h : A ⟶ X)
(w : CategoryTheory.CategoryStruct.comp h g = f)
:
def
CategoryTheory.Limits.imageSubobjectMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : W ⟶ X}
[CategoryTheory.Limits.HasImage f]
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasImage g]
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g)
[CategoryTheory.Limits.HasImageMap sq]
:
CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject g)
Given a commutative square between morphisms f and g,
we have a morphism in the category from imageSubobject f to imageSubobject g.
Instances For
@[simp]
theorem
CategoryTheory.Limits.imageSubobjectMap_arrow_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : W ⟶ X}
[CategoryTheory.Limits.HasImage f]
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasImage g]
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g)
[CategoryTheory.Limits.HasImageMap sq]
{Z : C}
(h : Z ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectMap sq)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (CategoryTheory.Limits.imageSubobject g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow (CategoryTheory.Limits.imageSubobject f))
(CategoryTheory.CategoryStruct.comp sq.right h)
@[simp]
theorem
CategoryTheory.Limits.imageSubobjectMap_arrow
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : W ⟶ X}
[CategoryTheory.Limits.HasImage f]
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasImage g]
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g)
[CategoryTheory.Limits.HasImageMap sq]
:
theorem
CategoryTheory.Limits.image_map_comp_imageSubobjectIso_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : W ⟶ X}
[CategoryTheory.Limits.HasImage f]
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasImage g]
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g)
[CategoryTheory.Limits.HasImageMap sq]
:
theorem
CategoryTheory.Limits.imageSubobjectIso_comp_image_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : W ⟶ X}
[CategoryTheory.Limits.HasImage f]
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasImage g]
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g)
[CategoryTheory.Limits.HasImageMap sq]
: