Specific subobjects #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define equalizer_subobject, kernel_subobject and image_subobject, 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 (image_subobject f).factors h
@[reducible]
noncomputable
def
category_theory.limits.equalizer_subobject
{C : Type u}
[category_theory.category C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_equalizer f g] :
The equalizer of morphisms f g : X ⟶ Y as a subobject X.
noncomputable
def
category_theory.limits.equalizer_subobject_iso
{C : Type u}
[category_theory.category C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_equalizer f g] :
The underlying object of equalizer_subobject f g is (up to isomorphism!)
the same as the chosen object equalizer f g.
@[simp]
theorem
category_theory.limits.equalizer_subobject_arrow_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_equalizer f g]
{X' : C}
(f' : X ⟶ X') :
@[simp]
theorem
category_theory.limits.equalizer_subobject_arrow
{C : Type u}
[category_theory.category C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_equalizer f g] :
@[simp]
theorem
category_theory.limits.equalizer_subobject_arrow'_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_equalizer f g]
{X' : C}
(f' : X ⟶ X') :
@[simp]
theorem
category_theory.limits.equalizer_subobject_arrow'
{C : Type u}
[category_theory.category C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_equalizer f g] :
theorem
category_theory.limits.equalizer_subobject_arrow_comp_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_equalizer f g]
{X' : C}
(f' : Y ⟶ X') :
(category_theory.limits.equalizer_subobject f g).arrow ≫ f ≫ f' = (category_theory.limits.equalizer_subobject f g).arrow ≫ g ≫ f'
theorem
category_theory.limits.equalizer_subobject_arrow_comp
{C : Type u}
[category_theory.category C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_equalizer f g] :
theorem
category_theory.limits.equalizer_subobject_factors
{C : Type u}
[category_theory.category C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_equalizer f g]
{W : C}
(h : W ⟶ X)
(w : h ≫ f = h ≫ g) :
theorem
category_theory.limits.equalizer_subobject_factors_iff
{C : Type u}
[category_theory.category C]
{X Y : C}
(f g : X ⟶ Y)
[category_theory.limits.has_equalizer f g]
{W : C}
(h : W ⟶ X) :
@[reducible]
noncomputable
def
category_theory.limits.kernel_subobject
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f] :
The kernel of a morphism f : X ⟶ Y as a subobject X.
noncomputable
def
category_theory.limits.kernel_subobject_iso
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f] :
The underlying object of kernel_subobject f is (up to isomorphism!)
the same as the chosen object kernel f.
@[simp]
theorem
category_theory.limits.kernel_subobject_arrow_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{X' : C}
(f' : X ⟶ X') :
@[simp]
theorem
category_theory.limits.kernel_subobject_arrow_apply
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
[I : category_theory.concrete_category C]
(x : ↥↑(category_theory.limits.kernel_subobject f)) :
@[simp]
theorem
category_theory.limits.kernel_subobject_arrow
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f] :
@[simp]
theorem
category_theory.limits.kernel_subobject_arrow'_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{X' : C}
(f' : X ⟶ X') :
@[simp]
theorem
category_theory.limits.kernel_subobject_arrow'_apply
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
[I : category_theory.concrete_category C]
(x : ↥(category_theory.limits.kernel f)) :
@[simp]
theorem
category_theory.limits.kernel_subobject_arrow'
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f] :
@[simp]
theorem
category_theory.limits.kernel_subobject_arrow_comp_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{X' : C}
(f' : Y ⟶ X') :
@[simp]
theorem
category_theory.limits.kernel_subobject_arrow_comp
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f] :
@[simp]
theorem
category_theory.limits.kernel_subobject_arrow_comp_apply
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
[I : category_theory.concrete_category C]
(x : ↥↑(category_theory.limits.kernel_subobject f)) :
theorem
category_theory.limits.kernel_subobject_factors
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{W : C}
(h : W ⟶ X)
(w : h ≫ f = 0) :
theorem
category_theory.limits.kernel_subobject_factors_iff
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{W : C}
(h : W ⟶ X) :
(category_theory.limits.kernel_subobject f).factors h ↔ h ≫ f = 0
noncomputable
def
category_theory.limits.factor_thru_kernel_subobject
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{W : C}
(h : W ⟶ X)
(w : h ≫ f = 0) :
A factorisation of h : W ⟶ X through kernel_subobject f, assuming h ≫ f = 0.
Equations
Instances for category_theory.limits.factor_thru_kernel_subobject
@[simp]
theorem
category_theory.limits.factor_thru_kernel_subobject_comp_arrow
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{W : C}
(h : W ⟶ X)
(w : h ≫ f = 0) :
@[simp]
theorem
category_theory.limits.factor_thru_kernel_subobject_comp_kernel_subobject_iso
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{W : C}
(h : W ⟶ X)
(w : h ≫ f = 0) :
noncomputable
def
category_theory.limits.kernel_subobject_map
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
{f : X ⟶ Y}
[category_theory.limits.has_kernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[category_theory.limits.has_kernel f']
(sq : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f') :
A commuting square induces a morphism between the kernel subobjects.
Equations
@[simp]
theorem
category_theory.limits.kernel_subobject_map_arrow_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
{f : X ⟶ Y}
[category_theory.limits.has_kernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[category_theory.limits.has_kernel f']
(sq : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f')
{X'_1 : C}
(f'_1 : X' ⟶ X'_1) :
category_theory.limits.kernel_subobject_map sq ≫ (category_theory.limits.kernel_subobject f').arrow ≫ f'_1 = (category_theory.limits.kernel_subobject f).arrow ≫ sq.left ≫ f'_1
@[simp]
theorem
category_theory.limits.kernel_subobject_map_arrow_apply
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
{f : X ⟶ Y}
[category_theory.limits.has_kernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[category_theory.limits.has_kernel f']
(sq : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f')
[I : category_theory.concrete_category C]
(x : ↥↑(category_theory.limits.kernel_subobject f)) :
⇑((category_theory.limits.kernel_subobject f').arrow) (⇑(category_theory.limits.kernel_subobject_map sq) x) = ⇑(sq.left) (⇑((category_theory.limits.kernel_subobject f).arrow) x)
@[simp]
theorem
category_theory.limits.kernel_subobject_map_arrow
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
{f : X ⟶ Y}
[category_theory.limits.has_kernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[category_theory.limits.has_kernel f']
(sq : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f') :
@[simp]
theorem
category_theory.limits.kernel_subobject_map_id
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
{f : X ⟶ Y}
[category_theory.limits.has_kernel f] :
@[simp]
theorem
category_theory.limits.kernel_subobject_map_comp
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
{f : X ⟶ Y}
[category_theory.limits.has_kernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[category_theory.limits.has_kernel f']
{X'' Y'' : C}
{f'' : X'' ⟶ Y''}
[category_theory.limits.has_kernel f'']
(sq : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f')
(sq' : category_theory.arrow.mk f' ⟶ category_theory.arrow.mk f'') :
theorem
category_theory.limits.kernel_map_comp_kernel_subobject_iso_inv_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
{f : X ⟶ Y}
[category_theory.limits.has_kernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[category_theory.limits.has_kernel f']
(sq : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f')
{X'_1 : C}
(f'_1 : ↑(category_theory.limits.kernel_subobject f') ⟶ X'_1) :
category_theory.limits.kernel.map f f' sq.left sq.right _ ≫ (category_theory.limits.kernel_subobject_iso f').inv ≫ f'_1 = (category_theory.limits.kernel_subobject_iso f).inv ≫ category_theory.limits.kernel_subobject_map sq ≫ f'_1
theorem
category_theory.limits.kernel_map_comp_kernel_subobject_iso_inv
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
{f : X ⟶ Y}
[category_theory.limits.has_kernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[category_theory.limits.has_kernel f']
(sq : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f') :
theorem
category_theory.limits.kernel_subobject_iso_comp_kernel_map_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
{f : X ⟶ Y}
[category_theory.limits.has_kernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[category_theory.limits.has_kernel f']
(sq : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f')
{X'_1 : C}
(f'_1 : category_theory.limits.kernel f' ⟶ X'_1) :
(category_theory.limits.kernel_subobject_iso f).hom ≫ category_theory.limits.kernel.map f f' sq.left sq.right _ ≫ f'_1 = category_theory.limits.kernel_subobject_map sq ≫ (category_theory.limits.kernel_subobject_iso f').hom ≫ f'_1
theorem
category_theory.limits.kernel_subobject_iso_comp_kernel_map
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
{f : X ⟶ Y}
[category_theory.limits.has_kernel f]
{X' Y' : C}
{f' : X' ⟶ Y'}
[category_theory.limits.has_kernel f']
(sq : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f') :
@[simp]
theorem
category_theory.limits.kernel_subobject_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{A B : C} :
@[protected, instance]
theorem
category_theory.limits.le_kernel_subobject
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
(A : category_theory.subobject X)
(h : A.arrow ≫ f = 0) :
noncomputable
def
category_theory.limits.kernel_subobject_iso_comp
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
{X' : C}
(f : X' ⟶ X)
[category_theory.is_iso f]
(g : X ⟶ Y)
[category_theory.limits.has_kernel g] :
The isomorphism between the kernel of f ≫ g and the kernel of g,
when f is an isomorphism.
@[simp]
theorem
category_theory.limits.kernel_subobject_iso_comp_hom_arrow
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
{X' : C}
(f : X' ⟶ X)
[category_theory.is_iso f]
(g : X ⟶ Y)
[category_theory.limits.has_kernel g] :
@[simp]
theorem
category_theory.limits.kernel_subobject_iso_comp_inv_arrow
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
{X' : C}
(f : X' ⟶ X)
[category_theory.is_iso f]
(g : X ⟶ Y)
[category_theory.limits.has_kernel g] :
theorem
category_theory.limits.kernel_subobject_comp_le
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{Z : C}
(h : Y ⟶ Z)
[category_theory.limits.has_kernel (f ≫ h)] :
The kernel of f is always a smaller subobject than the kernel of f ≫ h.
@[simp]
theorem
category_theory.limits.kernel_subobject_comp_mono
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{Z : C}
(h : Y ⟶ Z)
[category_theory.mono h] :
Postcomposing by an monomorphism does not change the kernel subobject.
@[protected, instance]
def
category_theory.limits.kernel_subobject_comp_mono_is_iso
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{Z : C}
(h : Y ⟶ Z)
[category_theory.mono h] :
noncomputable
def
category_theory.limits.cokernel_order_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_cokernels C]
(X : C) :
Taking cokernels is an order-reversing map from the subobjects of X to the quotient objects
of X.
Equations
- category_theory.limits.cokernel_order_hom X = {to_fun := category_theory.subobject.lift (λ (A : C) (f : A ⟶ X) (hf : category_theory.mono f), category_theory.subobject.mk (category_theory.limits.cokernel.π f).op) _, monotone' := _}
@[simp]
theorem
category_theory.limits.cokernel_order_hom_coe
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_cokernels C]
(X : C)
(ᾰ : category_theory.subobject X) :
⇑(category_theory.limits.cokernel_order_hom X) ᾰ = category_theory.subobject.lift (λ (A : C) (f : A ⟶ X) (hf : category_theory.mono f), category_theory.subobject.mk (category_theory.limits.cokernel.π f).op) _ ᾰ
noncomputable
def
category_theory.limits.kernel_order_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_kernels C]
(X : C) :
Taking kernels is an order-reversing map from the quotient objects of X to the subobjects of
X.
Equations
- category_theory.limits.kernel_order_hom X = {to_fun := category_theory.subobject.lift (λ (A : Cᵒᵖ) (f : A ⟶ opposite.op X) (hf : category_theory.mono f), category_theory.subobject.mk (category_theory.limits.kernel.ι f.unop)) _, monotone' := _}
@[simp]
theorem
category_theory.limits.kernel_order_hom_coe
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_kernels C]
(X : C)
(ᾰ : category_theory.subobject (opposite.op X)) :
⇑(category_theory.limits.kernel_order_hom X) ᾰ = category_theory.subobject.lift (λ (A : Cᵒᵖ) (f : A ⟶ opposite.op X) (hf : category_theory.mono f), category_theory.subobject.mk (category_theory.limits.kernel.ι f.unop)) _ ᾰ
@[reducible]
noncomputable
def
category_theory.limits.image_subobject
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f] :
The image of a morphism f g : X ⟶ Y as a subobject Y.
noncomputable
def
category_theory.limits.image_subobject_iso
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f] :
The underlying object of image_subobject f is (up to isomorphism!)
the same as the chosen object image f.
@[simp]
theorem
category_theory.limits.image_subobject_arrow_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f]
{X' : C}
(f' : Y ⟶ X') :
@[simp]
theorem
category_theory.limits.image_subobject_arrow
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f] :
@[simp]
theorem
category_theory.limits.image_subobject_arrow'_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f]
{X' : C}
(f' : Y ⟶ X') :
@[simp]
theorem
category_theory.limits.image_subobject_arrow'
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f] :
noncomputable
def
category_theory.limits.factor_thru_image_subobject
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f] :
A factorisation of f : X ⟶ Y through image_subobject f.
Equations
Instances for category_theory.limits.factor_thru_image_subobject
@[protected, instance]
@[simp]
theorem
category_theory.limits.image_subobject_arrow_comp
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f] :
@[simp]
theorem
category_theory.limits.image_subobject_arrow_comp_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f]
{X' : C}
(f' : Y ⟶ X') :
@[simp]
theorem
category_theory.limits.image_subobject_arrow_comp_apply
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f]
[I : category_theory.concrete_category C]
(x : ↥X) :
theorem
category_theory.limits.image_subobject_arrow_comp_eq_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
{f : X ⟶ Y}
{g : Y ⟶ Z}
[category_theory.limits.has_image f]
[category_theory.epi (category_theory.limits.factor_thru_image_subobject f)]
(h : f ≫ g = 0) :
theorem
category_theory.limits.image_subobject_factors_comp_self
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f]
{W : C}
(k : W ⟶ X) :
(category_theory.limits.image_subobject f).factors (k ≫ f)
@[simp]
theorem
category_theory.limits.factor_thru_image_subobject_comp_self
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f]
{W : C}
(k : W ⟶ X)
(h : (category_theory.limits.image_subobject f).factors (k ≫ f)) :
@[simp]
theorem
category_theory.limits.factor_thru_image_subobject_comp_self_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f]
{W W' : C}
(k : W ⟶ W')
(k' : W' ⟶ X)
(h : (category_theory.limits.image_subobject f).factors (k ≫ k' ≫ f)) :
(category_theory.limits.image_subobject f).factor_thru (k ≫ k' ≫ f) h = k ≫ k' ≫ category_theory.limits.factor_thru_image_subobject f
theorem
category_theory.limits.image_subobject_comp_le
{C : Type u}
[category_theory.category C]
{X Y X' : C}
(h : X' ⟶ X)
(f : X ⟶ Y)
[category_theory.limits.has_image f]
[category_theory.limits.has_image (h ≫ f)] :
The image of h ≫ f is always a smaller subobject than the image of f.
@[simp]
theorem
category_theory.limits.image_subobject_zero_arrow
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C] :
@[simp]
theorem
category_theory.limits.image_subobject_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
{A B : C} :
@[protected, instance]
def
category_theory.limits.image_subobject_comp_le_epi_of_epi
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_equalizers C]
{X' : C}
(h : X' ⟶ X)
[category_theory.epi h]
(f : X ⟶ Y)
[category_theory.limits.has_image f]
[category_theory.limits.has_image (h ≫ f)] :
The morphism image_subobject (h ≫ f) ⟶ image_subobject f
is an epimorphism when h is an epimorphism.
In general this does not imply that image_subobject (h ≫ f) = image_subobject f,
although it will when the ambient category is abelian.
noncomputable
def
category_theory.limits.image_subobject_comp_iso
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_equalizers C]
(f : X ⟶ Y)
[category_theory.limits.has_image f]
{Y' : C}
(h : Y ⟶ Y')
[category_theory.is_iso h] :
Postcomposing by an isomorphism gives an isomorphism between image subobjects.
@[simp]
theorem
category_theory.limits.image_subobject_comp_iso_hom_arrow_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_equalizers C]
(f : X ⟶ Y)
[category_theory.limits.has_image f]
{Y' : C}
(h : Y ⟶ Y')
[category_theory.is_iso h]
{X' : C}
(f' : Y ⟶ X') :
@[simp]
theorem
category_theory.limits.image_subobject_comp_iso_hom_arrow
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_equalizers C]
(f : X ⟶ Y)
[category_theory.limits.has_image f]
{Y' : C}
(h : Y ⟶ Y')
[category_theory.is_iso h] :
@[simp]
theorem
category_theory.limits.image_subobject_comp_iso_inv_arrow
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_equalizers C]
(f : X ⟶ Y)
[category_theory.limits.has_image f]
{Y' : C}
(h : Y ⟶ Y')
[category_theory.is_iso h] :
@[simp]
theorem
category_theory.limits.image_subobject_comp_iso_inv_arrow_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_equalizers C]
(f : X ⟶ Y)
[category_theory.limits.has_image f]
{Y' : C}
(h : Y ⟶ Y')
[category_theory.is_iso h]
{X' : C}
(f' : Y' ⟶ X') :
(category_theory.limits.image_subobject_comp_iso f h).inv ≫ (category_theory.limits.image_subobject (f ≫ h)).arrow ≫ f' = (category_theory.limits.image_subobject f).arrow ≫ h ≫ f'
theorem
category_theory.limits.image_subobject_mono
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f] :
theorem
category_theory.limits.image_subobject_iso_comp
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_equalizers C]
{X' : C}
(h : X' ⟶ X)
[category_theory.is_iso h]
(f : X ⟶ Y)
[category_theory.limits.has_image f] :
Precomposing by an isomorphism does not change the image subobject.
theorem
category_theory.limits.image_subobject_le
{C : Type u}
[category_theory.category C]
{A B : C}
{X : category_theory.subobject B}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(h : A ⟶ ↑X)
(w : h ≫ X.arrow = f) :
theorem
category_theory.limits.image_subobject_le_mk
{C : Type u}
[category_theory.category C]
{A B X : C}
(g : X ⟶ B)
[category_theory.mono g]
(f : A ⟶ B)
[category_theory.limits.has_image f]
(h : A ⟶ X)
(w : h ≫ g = f) :
noncomputable
def
category_theory.limits.image_subobject_map
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
[category_theory.limits.has_image f]
{g : Y ⟶ Z}
[category_theory.limits.has_image g]
(sq : category_theory.arrow.mk f ⟶ category_theory.arrow.mk g)
[category_theory.limits.has_image_map sq] :
Given a commutative square between morphisms f and g,
we have a morphism in the category from image_subobject f to image_subobject g.
@[simp]
theorem
category_theory.limits.image_subobject_map_arrow
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
[category_theory.limits.has_image f]
{g : Y ⟶ Z}
[category_theory.limits.has_image g]
(sq : category_theory.arrow.mk f ⟶ category_theory.arrow.mk g)
[category_theory.limits.has_image_map sq] :
@[simp]
theorem
category_theory.limits.image_subobject_map_arrow_assoc
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
[category_theory.limits.has_image f]
{g : Y ⟶ Z}
[category_theory.limits.has_image g]
(sq : category_theory.arrow.mk f ⟶ category_theory.arrow.mk g)
[category_theory.limits.has_image_map sq]
{X' : C}
(f' : Z ⟶ X') :
theorem
category_theory.limits.image_map_comp_image_subobject_iso_inv
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
[category_theory.limits.has_image f]
{g : Y ⟶ Z}
[category_theory.limits.has_image g]
(sq : category_theory.arrow.mk f ⟶ category_theory.arrow.mk g)
[category_theory.limits.has_image_map sq] :
theorem
category_theory.limits.image_subobject_iso_comp_image_map
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
{f : W ⟶ X}
[category_theory.limits.has_image f]
{g : Y ⟶ Z}
[category_theory.limits.has_image g]
(sq : category_theory.arrow.mk f ⟶ category_theory.arrow.mk g)
[category_theory.limits.has_image_map sq] :