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

@[reducible, inline]

abbrev CategoryTheory.Limits.equalizerSubobject {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] : Subobject X

The equalizer of morphisms f g : X ⟶ Y as a Subobject X.

Equations

• CategoryTheory.Limits.equalizerSubobject f g = CategoryTheory.Subobject.mk (CategoryTheory.Limits.equalizer.ι f g)

def CategoryTheory.Limits.equalizerSubobjectIso {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] : Subobject.underlying.obj (equalizerSubobject f g) ≅ equalizer f g

The underlying object of equalizerSubobject f g is (up to isomorphism!) the same as the chosen object equalizer f g.

Equations

• CategoryTheory.Limits.equalizerSubobjectIso f g = CategoryTheory.Subobject.underlyingIso (CategoryTheory.Limits.equalizer.ι f g)

@[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)

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

@[reducible, inline]

abbrev CategoryTheory.Limits.kernelSubobject {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] : Subobject X

The kernel of a morphism f : X ⟶ Y as a Subobject X.

Equations

• CategoryTheory.Limits.kernelSubobject f = CategoryTheory.Subobject.mk (CategoryTheory.Limits.kernel.ι f)

def CategoryTheory.Limits.kernelSubobjectIso {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] : Subobject.underlying.obj (kernelSubobject f) ≅ kernel f

The underlying object of kernelSubobject f is (up to isomorphism!) the same as the chosen object kernel f.

Equations

• CategoryTheory.Limits.kernelSubobjectIso f = CategoryTheory.Subobject.underlyingIso (CategoryTheory.Limits.kernel.ι f)

@[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 : ToType (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 : ToType (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 : ToType (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

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) : W ⟶ Subobject.underlying.obj (kernelSubobject f)

A factorisation of h : W ⟶ X through kernelSubobject f, assuming h ≫ f = 0.

Equations

• CategoryTheory.Limits.factorThruKernelSubobject f h w = (CategoryTheory.Limits.kernelSubobject f).factorThru h ⋯

@[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

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') : Subobject.underlying.obj (kernelSubobject f) ⟶ Subobject.underlying.obj (kernelSubobject f')

A commuting square induces a morphism between the kernel subobjects.

Equations

• One or more equations did not get rendered due to their size.

@[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 (kernelSubobject f).arrow (CategoryStruct.comp 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 : ToType (Subobject.underlying.obj (kernelSubobject f))) : (ConcreteCategory.hom (kernelSubobject f').arrow) ((ConcreteCategory.hom (kernelSubobjectMap sq)) x) = (CategoryStruct.comp (kernelSubobject f).arrow sq.left) x

@[simp]

theorem CategoryTheory.Limits.kernelSubobjectMap_id {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] {f : X ⟶ Y} [HasKernel f] : kernelSubobjectMap (CategoryStruct.id (Arrow.mk f)) = CategoryStruct.id (Subobject.underlying.obj (kernelSubobject 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)

@[simp]

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] : IsIso (kernelSubobject 0).arrow

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) : A ≤ kernelSubobject f

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] : Subobject.underlying.obj (kernelSubobject (CategoryStruct.comp f g)) ≅ Subobject.underlying.obj (kernelSubobject g)

The isomorphism between the kernel of f ≫ g and the kernel of g, when f is an isomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[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] : CategoryStruct.comp (kernelSubobjectIsoComp f g).hom (kernelSubobject g).arrow = CategoryStruct.comp (kernelSubobject (CategoryStruct.comp f g)).arrow f

@[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)] : kernelSubobject f ≤ kernelSubobject (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] : kernelSubobject (CategoryStruct.comp f h) = kernelSubobject f

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)) ⋯)

def CategoryTheory.Limits.cokernelOrderHom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasCokernels C] (X : C) : Subobject X →o (Subobject (Opposite.op X))ᵒᵈ

Taking cokernels is an order-reversing map from the subobjects of X to the quotient objects of X.

Equations

• One or more equations did not get rendered due to their size.

@[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✝

def CategoryTheory.Limits.kernelOrderHom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasKernels C] (X : C) : (Subobject (Opposite.op X))ᵒᵈ →o Subobject X

Taking kernels is an order-reversing map from the quotient objects of X to the subobjects of X.

Equations

• One or more equations did not get rendered due to their size.

@[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]

abbrev CategoryTheory.Limits.imageSubobject {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] : Subobject Y

The image of a morphism f g : X ⟶ Y as a Subobject Y.

Equations

• CategoryTheory.Limits.imageSubobject f = CategoryTheory.Subobject.mk (CategoryTheory.Limits.image.ι f)

def CategoryTheory.Limits.imageSubobjectIso {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] : Subobject.underlying.obj (imageSubobject f) ≅ image f

The underlying object of imageSubobject f is (up to isomorphism!) the same as the chosen object image f.

Equations

• CategoryTheory.Limits.imageSubobjectIso f = CategoryTheory.Subobject.underlyingIso (CategoryTheory.Limits.image.ι f)

@[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

def CategoryTheory.Limits.factorThruImageSubobject {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] : X ⟶ Subobject.underlying.obj (imageSubobject f)

A factorisation of f : X ⟶ Y through imageSubobject f.

Equations

• CategoryTheory.Limits.factorThruImageSubobject f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) (CategoryTheory.Limits.imageSubobjectIso f).inv

instance CategoryTheory.Limits.instEpiFactorThruImageSubobjectOfHasEqualizers {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] [HasEqualizers C] : Epi (factorThruImageSubobject f)

@[simp]

theorem CategoryTheory.Limits.imageSubobject_arrow_comp {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] : CategoryStruct.comp (factorThruImageSubobject f) (imageSubobject f).arrow = 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) : CategoryStruct.comp (factorThruImageSubobject f) (CategoryStruct.comp (imageSubobject f).arrow h) = CategoryStruct.comp f h

@[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 : ToType 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)] : imageSubobject (CategoryStruct.comp h f) ≤ imageSubobject 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.

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] : Subobject.underlying.obj (imageSubobject (CategoryStruct.comp f h)) ≅ Subobject.underlying.obj (imageSubobject f)

Postcomposing by an isomorphism gives an isomorphism between image subobjects.

Equations

• One or more equations did not get rendered due to their size.

@[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) : imageSubobject f ≤ X

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) : imageSubobject f ≤ Subobject.mk g

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] : Subobject.underlying.obj (imageSubobject f) ⟶ Subobject.underlying.obj (imageSubobject g)

Given a commutative square between morphisms f and g, we have a morphism in the category from imageSubobject f to imageSubobject g.

Equations

• One or more equations did not get rendered due to their size.

@[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 (imageSubobject f).arrow (CategoryStruct.comp 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