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: an iff characterisation of (imageSubobject f).Factors h
theorem
CategoryTheory.Limits.pullback_factors
{C : Type u}
[Category.{v, u} C]
{X Y W : C}
(f : X ⟶ Y)
[HasPullbacks C]
(y : Subobject Y)
(h : W ⟶ X)
(hF : y.Factors (CategoryStruct.comp h f))
:
((Subobject.pullback f).obj y).Factors h
theorem
CategoryTheory.Limits.pullback_factors_iff
{C : Type u}
[Category.{v, u} C]
{X Y W : C}
(f : X ⟶ Y)
[HasPullbacks C]
(y : Subobject Y)
(h : W ⟶ X)
:
((Subobject.pullback f).obj y).Factors h ↔ y.Factors (CategoryStruct.comp h f)
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.equalizerSubobject
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
:
The equalizer of morphisms f g : X ⟶ Y as a Subobject X.
Instances For
noncomputable def
CategoryTheory.Limits.equalizerSubobjectIso
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer 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
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
:
CategoryStruct.comp (equalizerSubobjectIso f g).hom (equalizer.ι f g) = (equalizerSubobject f g).arrow
@[simp]
theorem
CategoryTheory.Limits.equalizerSubobject_arrow_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
{Z : C}
(h : X ⟶ Z)
:
CategoryStruct.comp (equalizerSubobjectIso f g).hom (CategoryStruct.comp (equalizer.ι f g) h) = CategoryStruct.comp (equalizerSubobject f g).arrow h
@[simp]
theorem
CategoryTheory.Limits.equalizerSubobject_arrow'
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
:
CategoryStruct.comp (equalizerSubobjectIso f g).inv (equalizerSubobject f g).arrow = equalizer.ι f g
@[simp]
theorem
CategoryTheory.Limits.equalizerSubobject_arrow'_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
{Z : C}
(h : X ⟶ Z)
:
CategoryStruct.comp (equalizerSubobjectIso f g).inv (CategoryStruct.comp (equalizerSubobject f g).arrow h) = CategoryStruct.comp (equalizer.ι f g) h
theorem
CategoryTheory.Limits.equalizerSubobject_arrow_comp
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
:
CategoryStruct.comp (equalizerSubobject f g).arrow f = CategoryStruct.comp (equalizerSubobject f g).arrow g
theorem
CategoryTheory.Limits.equalizerSubobject_arrow_comp_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
{Z : C}
(h : Y ⟶ Z)
:
CategoryStruct.comp (equalizerSubobject f g).arrow (CategoryStruct.comp f h) = CategoryStruct.comp (equalizerSubobject f g).arrow (CategoryStruct.comp g h)
@[simp]
theorem
CategoryTheory.Limits.equalizerSubobject_of_self
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
equalizerSubobject f f = ⊤
theorem
CategoryTheory.Limits.equalizerSubobject_factors
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
{W : C}
(h : W ⟶ X)
(w : CategoryStruct.comp h f = CategoryStruct.comp h g)
:
(equalizerSubobject f g).Factors h
theorem
CategoryTheory.Limits.equalizerSubobject_factors_iff
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
{W : C}
(h : W ⟶ X)
:
(equalizerSubobject f g).Factors h ↔ CategoryStruct.comp h f = CategoryStruct.comp h g
@[simp]
theorem
CategoryTheory.Limits.pullback_equalizer
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f g : X ⟶ Y)
[HasEqualizer f g]
{W : C}
(h : W ⟶ X)
[HasPullbacks C]
:
(Subobject.pullback h).obj (equalizerSubobject f g) = equalizerSubobject (CategoryStruct.comp h f) (CategoryStruct.comp h g)
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.kernelSubobject
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
:
The kernel of a morphism f : X ⟶ Y as a Subobject X.
Instances For
noncomputable def
CategoryTheory.Limits.kernelSubobjectIso
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel 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
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
:
CategoryStruct.comp (kernelSubobjectIso f).hom (kernel.ι f) = (kernelSubobject f).arrow
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
{Z : C}
(h : X ⟶ Z)
:
CategoryStruct.comp (kernelSubobjectIso f).hom (CategoryStruct.comp (kernel.ι f) h) = CategoryStruct.comp (kernelSubobject f).arrow h
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow_apply
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
{F : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F]
(x : carrier (Subobject.underlying.obj (kernelSubobject f)))
:
(ConcreteCategory.hom (kernel.ι f)) ((ConcreteCategory.hom (kernelSubobjectIso f).hom) x) = (ConcreteCategory.hom (kernelSubobject f).arrow) x
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow'
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
:
CategoryStruct.comp (kernelSubobjectIso f).inv (kernelSubobject f).arrow = kernel.ι f
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow'_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
{Z : C}
(h : X ⟶ Z)
:
CategoryStruct.comp (kernelSubobjectIso f).inv (CategoryStruct.comp (kernelSubobject f).arrow h) = CategoryStruct.comp (kernel.ι f) h
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow'_apply
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
{F : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F]
(x : carrier (kernel f))
:
(ConcreteCategory.hom (kernelSubobject f).arrow) ((ConcreteCategory.hom (kernelSubobjectIso f).inv) x) = (ConcreteCategory.hom (kernel.ι f)) x
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow_comp
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
:
CategoryStruct.comp (kernelSubobject f).arrow f = 0
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow_comp_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
{Z : C}
(h : Y ⟶ Z)
:
CategoryStruct.comp (kernelSubobject f).arrow (CategoryStruct.comp f h) = CategoryStruct.comp 0 h
@[simp]
theorem
CategoryTheory.Limits.kernelSubobject_arrow_comp_apply
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
{F : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F]
(x : carrier (Subobject.underlying.obj (kernelSubobject f)))
:
(ConcreteCategory.hom f) ((ConcreteCategory.hom (kernelSubobject f).arrow) x) = (ConcreteCategory.hom 0) x
theorem
CategoryTheory.Limits.kernelSubobject_factors
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
{W : C}
(h : W ⟶ X)
(w : CategoryStruct.comp h f = 0)
:
(kernelSubobject f).Factors h
theorem
CategoryTheory.Limits.kernelSubobject_factors_iff
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
{W : C}
(h : W ⟶ X)
:
(kernelSubobject f).Factors h ↔ CategoryStruct.comp h f = 0
noncomputable def
CategoryTheory.Limits.factorThruKernelSubobject
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
{W : C}
(h : W ⟶ X)
(w : CategoryStruct.comp h f = 0)
:
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}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
{W : C}
(h : W ⟶ X)
(w : CategoryStruct.comp h f = 0)
:
CategoryStruct.comp (factorThruKernelSubobject f h w) (kernelSubobject f).arrow = h
@[simp]
theorem
CategoryTheory.Limits.factorThruKernelSubobject_comp_kernelSubobjectIso
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
{W : C}
(h : W ⟶ X)
(w : CategoryStruct.comp h f = 0)
:
CategoryStruct.comp (factorThruKernelSubobject f h w) (kernelSubobjectIso f).hom = kernel.lift f h w
noncomputable def
CategoryTheory.Limits.kernelSubobjectMap
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
{f : X ⟶ Y}
[HasKernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[HasKernel f']
(sq : Arrow.mk f ⟶ Arrow.mk f')
:
A commuting square induces a morphism between the kernel subobjects.
Instances For
@[simp]
theorem
CategoryTheory.Limits.kernelSubobjectMap_arrow
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
{f : X ⟶ Y}
[HasKernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[HasKernel f']
(sq : Arrow.mk f ⟶ Arrow.mk f')
:
CategoryStruct.comp (kernelSubobjectMap sq) (kernelSubobject f').arrow = CategoryStruct.comp (kernelSubobject f).arrow sq.left
@[simp]
theorem
CategoryTheory.Limits.kernelSubobjectMap_arrow_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
{f : X ⟶ Y}
[HasKernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[HasKernel f']
(sq : Arrow.mk f ⟶ Arrow.mk f')
{Z : C}
(h : X' ⟶ Z)
:
CategoryStruct.comp (kernelSubobjectMap sq) (CategoryStruct.comp (kernelSubobject f').arrow h) = CategoryStruct.comp (CategoryStruct.comp (kernelSubobject f).arrow sq.left) h
@[simp]
theorem
CategoryTheory.Limits.kernelSubobjectMap_arrow_apply
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
{f : X ⟶ Y}
[HasKernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[HasKernel f']
(sq : Arrow.mk f ⟶ Arrow.mk f')
{F : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F]
(x : carrier (Subobject.underlying.obj (kernelSubobject f)))
:
(ConcreteCategory.hom (kernelSubobject f').arrow) ((ConcreteCategory.hom (kernelSubobjectMap sq)) x) = (ConcreteCategory.hom sq.left) ((ConcreteCategory.hom (kernelSubobject f).arrow) x)
@[simp]
theorem
CategoryTheory.Limits.kernelSubobjectMap_id
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
{f : X ⟶ Y}
[HasKernel f]
:
@[simp]
theorem
CategoryTheory.Limits.kernelSubobjectMap_comp
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
{f : X ⟶ Y}
[HasKernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[HasKernel f']
{X'' Y'' : C}
{f'' : X'' ⟶ Y''}
[HasKernel f'']
(sq : Arrow.mk f ⟶ Arrow.mk f')
(sq' : Arrow.mk f' ⟶ Arrow.mk f'')
:
kernelSubobjectMap (CategoryStruct.comp sq sq') = CategoryStruct.comp (kernelSubobjectMap sq) (kernelSubobjectMap sq')
theorem
CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
{f : X ⟶ Y}
[HasKernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[HasKernel f']
(sq : Arrow.mk f ⟶ Arrow.mk f')
:
CategoryStruct.comp (kernel.map f f' sq.left sq.right ⋯) (kernelSubobjectIso f').inv = CategoryStruct.comp (kernelSubobjectIso f).inv (kernelSubobjectMap sq)
theorem
CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
{f : X ⟶ Y}
[HasKernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[HasKernel f']
(sq : Arrow.mk f ⟶ Arrow.mk f')
{Z : C}
(h : Subobject.underlying.obj (kernelSubobject f') ⟶ Z)
:
CategoryStruct.comp (kernel.map f f' sq.left sq.right ⋯) (CategoryStruct.comp (kernelSubobjectIso f').inv h) = CategoryStruct.comp (kernelSubobjectIso f).inv (CategoryStruct.comp (kernelSubobjectMap sq) h)
theorem
CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
{f : X ⟶ Y}
[HasKernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[HasKernel f']
(sq : Arrow.mk f ⟶ Arrow.mk f')
:
CategoryStruct.comp (kernelSubobjectIso f).hom (kernel.map f f' sq.left sq.right ⋯) = CategoryStruct.comp (kernelSubobjectMap sq) (kernelSubobjectIso f').hom
theorem
CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
{f : X ⟶ Y}
[HasKernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[HasKernel f']
(sq : Arrow.mk f ⟶ Arrow.mk f')
{Z : C}
(h : kernel f' ⟶ Z)
:
CategoryStruct.comp (kernelSubobjectIso f).hom (CategoryStruct.comp (kernel.map f f' sq.left sq.right ⋯) h) = CategoryStruct.comp (kernelSubobjectMap sq) (CategoryStruct.comp (kernelSubobjectIso f').hom h)
theorem
CategoryTheory.Limits.kernelSubobject_zero
{C : Type u}
[Category.{v, u} C]
[HasZeroMorphisms C]
{A B : C}
:
kernelSubobject 0 = ⊤
instance
CategoryTheory.Limits.isIso_kernelSubobject_zero_arrow
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
:
theorem
CategoryTheory.Limits.le_kernelSubobject
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
(A : Subobject X)
(h : CategoryStruct.comp A.arrow f = 0)
:
noncomputable def
CategoryTheory.Limits.kernelSubobjectIsoComp
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
{X' : C}
(f : X' ⟶ X)
[IsIso f]
(g : X ⟶ Y)
[HasKernel 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}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
{X' : C}
(f : X' ⟶ X)
[IsIso f]
(g : X ⟶ Y)
[HasKernel g]
:
@[simp]
theorem
CategoryTheory.Limits.kernelSubobjectIsoComp_inv_arrow
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
{X' : C}
(f : X' ⟶ X)
[IsIso f]
(g : X ⟶ Y)
[HasKernel g]
:
CategoryStruct.comp (kernelSubobjectIsoComp f g).inv (kernelSubobject (CategoryStruct.comp f g)).arrow = CategoryStruct.comp (kernelSubobject g).arrow (inv f)
theorem
CategoryTheory.Limits.kernelSubobject_comp_le
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
{Z : C}
(h : Y ⟶ Z)
[HasKernel (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}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
{Z : C}
(h : Y ⟶ Z)
[Mono h]
:
Postcomposing by a monomorphism does not change the kernel subobject.
instance
CategoryTheory.Limits.kernelSubobject_comp_mono_isIso
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
(f : X ⟶ Y)
[HasKernel f]
{Z : C}
(h : Y ⟶ Z)
[Mono h]
:
IsIso ((kernelSubobject f).ofLE (kernelSubobject (CategoryStruct.comp f h)) ⋯)
noncomputable def
CategoryTheory.Limits.cokernelOrderHom
{C : Type u}
[Category.{v, u} C]
[HasZeroMorphisms C]
[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.cokernelOrderHom_coe
{C : Type u}
[Category.{v, u} C]
[HasZeroMorphisms C]
[HasCokernels C]
(X : C)
(a✝ : Subobject X)
:
(cokernelOrderHom X) a✝ = Subobject.lift (fun (x : C) (f : x ⟶ X) (x_1 : Mono f) => Subobject.mk (cokernel.π f).op) ⋯ a✝
noncomputable def
CategoryTheory.Limits.kernelOrderHom
{C : Type u}
[Category.{v, u} C]
[HasZeroMorphisms C]
[HasKernels C]
(X : C)
:
Taking kernels is an order-reversing map from the quotient objects of X to the subobjects of
X.
Instances For
@[simp]
theorem
CategoryTheory.Limits.kernelOrderHom_coe
{C : Type u}
[Category.{v, u} C]
[HasZeroMorphisms C]
[HasKernels C]
(X : C)
(a✝ : Subobject (Opposite.op X))
:
(kernelOrderHom X) a✝ = Subobject.lift (fun (x : Cᵒᵖ) (f : x ⟶ Opposite.op X) (x_1 : Mono f) => Subobject.mk (kernel.ι f.unop)) ⋯ a✝
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Limits.imageSubobject
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[HasImage f]
:
The image of a morphism f g : X ⟶ Y as a Subobject Y.
Instances For
noncomputable def
CategoryTheory.Limits.imageSubobjectIso
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[HasImage 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
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[HasImage f]
:
CategoryStruct.comp (imageSubobjectIso f).hom (image.ι f) = (imageSubobject f).arrow
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_arrow_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[HasImage f]
{Z : C}
(h : Y ⟶ Z)
:
CategoryStruct.comp (imageSubobjectIso f).hom (CategoryStruct.comp (image.ι f) h) = CategoryStruct.comp (imageSubobject f).arrow h
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_arrow'
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[HasImage f]
:
CategoryStruct.comp (imageSubobjectIso f).inv (imageSubobject f).arrow = image.ι f
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_arrow'_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[HasImage f]
{Z : C}
(h : Y ⟶ Z)
:
CategoryStruct.comp (imageSubobjectIso f).inv (CategoryStruct.comp (imageSubobject f).arrow h) = CategoryStruct.comp (image.ι f) h
noncomputable def
CategoryTheory.Limits.factorThruImageSubobject
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[HasImage f]
:
A factorisation of f : X ⟶ Y through imageSubobject f.
Instances For
instance
CategoryTheory.Limits.instEpiFactorThruImageSubobjectOfHasEqualizers
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[HasImage f]
[HasEqualizers C]
:
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_arrow_comp
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[HasImage f]
:
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_arrow_comp_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[HasImage f]
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_arrow_comp_apply
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[HasImage f]
{F : C → C → Type uF}
{carrier : C → Type w}
{instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
[inst : ConcreteCategory C F]
(x : carrier X)
:
(ConcreteCategory.hom (imageSubobject f).arrow) ((ConcreteCategory.hom (factorThruImageSubobject f)) x) = (ConcreteCategory.hom f) x
theorem
CategoryTheory.Limits.imageSubobject_arrow_comp_eq_zero
{C : Type u}
[Category.{v, u} C]
[HasZeroMorphisms C]
{X Y Z : C}
{f : X ⟶ Y}
{g : Y ⟶ Z}
[HasImage f]
[Epi (factorThruImageSubobject f)]
(h : CategoryStruct.comp f g = 0)
:
CategoryStruct.comp (imageSubobject f).arrow g = 0
theorem
CategoryTheory.Limits.imageSubobject_factors_comp_self
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[HasImage f]
{W : C}
(k : W ⟶ X)
:
(imageSubobject f).Factors (CategoryStruct.comp k f)
@[simp]
theorem
CategoryTheory.Limits.factorThruImageSubobject_comp_self
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[HasImage f]
{W : C}
(k : W ⟶ X)
(h : (imageSubobject f).Factors (CategoryStruct.comp k f))
:
(imageSubobject f).factorThru (CategoryStruct.comp k f) h = CategoryStruct.comp k (factorThruImageSubobject f)
@[simp]
theorem
CategoryTheory.Limits.factorThruImageSubobject_comp_self_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[HasImage f]
{W W' : C}
(k : W ⟶ W')
(k' : W' ⟶ X)
(h : (imageSubobject f).Factors (CategoryStruct.comp k (CategoryStruct.comp k' f)))
:
(imageSubobject f).factorThru (CategoryStruct.comp k (CategoryStruct.comp k' f)) h = CategoryStruct.comp k (CategoryStruct.comp k' (factorThruImageSubobject f))
theorem
CategoryTheory.Limits.imageSubobject_comp_le
{C : Type u}
[Category.{v, u} C]
{X Y X' : C}
(h : X' ⟶ X)
(f : X ⟶ Y)
[HasImage f]
[HasImage (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}
[Category.{v, u} C]
{X Y : C}
[HasZeroMorphisms C]
[HasZeroObject C]
:
(imageSubobject 0).arrow = 0
@[simp]
theorem
CategoryTheory.Limits.imageSubobject_zero
{C : Type u}
[Category.{v, u} C]
[HasZeroMorphisms C]
[HasZeroObject C]
{A B : C}
:
imageSubobject 0 = ⊥
instance
CategoryTheory.Limits.imageSubobject_comp_le_epi_of_epi
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasEqualizers C]
{X' : C}
(h : X' ⟶ X)
[Epi h]
(f : X ⟶ Y)
[HasImage f]
[HasImage (CategoryStruct.comp h f)]
:
Epi ((imageSubobject (CategoryStruct.comp h f)).ofLE (imageSubobject 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.
noncomputable def
CategoryTheory.Limits.imageSubobjectCompIso
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasEqualizers C]
(f : X ⟶ Y)
[HasImage f]
{Y' : C}
(h : Y ⟶ Y')
[IsIso h]
:
Postcomposing by an isomorphism gives an isomorphism between image subobjects.
Instances For
@[simp]
theorem
CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasEqualizers C]
(f : X ⟶ Y)
[HasImage f]
{Y' : C}
(h : Y ⟶ Y')
[IsIso h]
:
CategoryStruct.comp (imageSubobjectCompIso f h).hom (imageSubobject f).arrow = CategoryStruct.comp (imageSubobject (CategoryStruct.comp f h)).arrow (inv h)
@[simp]
theorem
CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasEqualizers C]
(f : X ⟶ Y)
[HasImage f]
{Y' : C}
(h : Y ⟶ Y')
[IsIso h]
{Z : C}
(h✝ : Y ⟶ Z)
:
CategoryStruct.comp (imageSubobjectCompIso f h).hom (CategoryStruct.comp (imageSubobject f).arrow h✝) = CategoryStruct.comp (imageSubobject (CategoryStruct.comp f h)).arrow (CategoryStruct.comp (inv h) h✝)
@[simp]
theorem
CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasEqualizers C]
(f : X ⟶ Y)
[HasImage f]
{Y' : C}
(h : Y ⟶ Y')
[IsIso h]
:
CategoryStruct.comp (imageSubobjectCompIso f h).inv (imageSubobject (CategoryStruct.comp f h)).arrow = CategoryStruct.comp (imageSubobject f).arrow h
@[simp]
theorem
CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow_assoc
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasEqualizers C]
(f : X ⟶ Y)
[HasImage f]
{Y' : C}
(h : Y ⟶ Y')
[IsIso h]
{Z : C}
(h✝ : Y' ⟶ Z)
:
CategoryStruct.comp (imageSubobjectCompIso f h).inv
(CategoryStruct.comp (imageSubobject (CategoryStruct.comp f h)).arrow h✝) = CategoryStruct.comp (imageSubobject f).arrow (CategoryStruct.comp h h✝)
theorem
CategoryTheory.Limits.imageSubobject_mono
{C : Type u}
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
[Mono f]
:
imageSubobject f = Subobject.mk f
theorem
CategoryTheory.Limits.imageSubobject_iso_comp
{C : Type u}
[Category.{v, u} C]
{X Y : C}
[HasEqualizers C]
{X' : C}
(h : X' ⟶ X)
[IsIso h]
(f : X ⟶ Y)
[HasImage f]
:
imageSubobject (CategoryStruct.comp h f) = imageSubobject f
Precomposing by an isomorphism does not change the image subobject.
theorem
CategoryTheory.Limits.imageSubobject_le
{C : Type u}
[Category.{v, u} C]
{A B : C}
{X : Subobject B}
(f : A ⟶ B)
[HasImage f]
(h : A ⟶ Subobject.underlying.obj X)
(w : CategoryStruct.comp h X.arrow = f)
:
theorem
CategoryTheory.Limits.imageSubobject_le_mk
{C : Type u}
[Category.{v, u} C]
{A B X : C}
(g : X ⟶ B)
[Mono g]
(f : A ⟶ B)
[HasImage f]
(h : A ⟶ X)
(w : CategoryStruct.comp h g = f)
:
noncomputable def
CategoryTheory.Limits.imageSubobjectMap
{C : Type u}
[Category.{v, u} C]
{W X Y Z : C}
{f : W ⟶ X}
[HasImage f]
{g : Y ⟶ Z}
[HasImage g]
(sq : Arrow.mk f ⟶ Arrow.mk g)
[HasImageMap sq]
:
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
{C : Type u}
[Category.{v, u} C]
{W X Y Z : C}
{f : W ⟶ X}
[HasImage f]
{g : Y ⟶ Z}
[HasImage g]
(sq : Arrow.mk f ⟶ Arrow.mk g)
[HasImageMap sq]
:
CategoryStruct.comp (imageSubobjectMap sq) (imageSubobject g).arrow = CategoryStruct.comp (imageSubobject f).arrow sq.right
@[simp]
theorem
CategoryTheory.Limits.imageSubobjectMap_arrow_assoc
{C : Type u}
[Category.{v, u} C]
{W X Y Z : C}
{f : W ⟶ X}
[HasImage f]
{g : Y ⟶ Z}
[HasImage g]
(sq : Arrow.mk f ⟶ Arrow.mk g)
[HasImageMap sq]
{Z✝ : C}
(h : Z ⟶ Z✝)
:
CategoryStruct.comp (imageSubobjectMap sq) (CategoryStruct.comp (imageSubobject g).arrow h) = CategoryStruct.comp (CategoryStruct.comp (imageSubobject f).arrow sq.right) h
theorem
CategoryTheory.Limits.image_map_comp_imageSubobjectIso_inv
{C : Type u}
[Category.{v, u} C]
{W X Y Z : C}
{f : W ⟶ X}
[HasImage f]
{g : Y ⟶ Z}
[HasImage g]
(sq : Arrow.mk f ⟶ Arrow.mk g)
[HasImageMap sq]
:
CategoryStruct.comp (image.map sq) (imageSubobjectIso (Arrow.mk g).hom).inv = CategoryStruct.comp (imageSubobjectIso f).inv (imageSubobjectMap sq)
theorem
CategoryTheory.Limits.imageSubobjectIso_comp_image_map
{C : Type u}
[Category.{v, u} C]
{W X Y Z : C}
{f : W ⟶ X}
[HasImage f]
{g : Y ⟶ Z}
[HasImage g]
(sq : Arrow.mk f ⟶ Arrow.mk g)
[HasImageMap sq]
:
CategoryStruct.comp (imageSubobjectIso (Arrow.mk f).hom).hom (image.map sq) = CategoryStruct.comp (imageSubobjectMap sq) (imageSubobjectIso g).hom