15.4. ForMathlib: CategoryTheory.ObjectProperty.FullSubcategoryLimits🔗

15.4.1. homMk_eq_zero🔗

In a full subcategory, homMk f = 0 if and only if f = 0 in the ambient category.

Proof: Both directions follow from the fact that .hom is injective on morphisms in the full subcategory.

theorem

CategoryTheory.ObjectProperty.FullSubcategory.homMk_eq_zero.{v, u}
  {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms C]
  {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory}
  (f : X.obj ⟶ Y.obj) :
  CategoryTheory.ObjectProperty.homMk f = 0 ↔ f = 0
CategoryTheory.ObjectProperty.FullSubcategory.homMk_eq_zero.{v,
    u}
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms
      C]
  {P : CategoryTheory.ObjectProperty C}
  {X Y : P.FullSubcategory}
  (f : X.obj ⟶ Y.obj) :
  CategoryTheory.ObjectProperty.homMk f =
      0 ↔
    f = 0

Something wrong, better idea? Suggest a change

15.4.2. kernel_condition_hom🔗

In a full subcategory, the kernel condition \iota \circ f = 0 holds at the level of underlying morphisms: (\ker(f).\iota).\mathrm{hom} \circ f.\mathrm{hom} = 0.

Proof: Apply congr_arg (·.hom) to kernel.condition f.

theorem

CategoryTheory.ObjectProperty.FullSubcategory.kernel_condition_hom.{v,
    u}
  {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms C]
  {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory}
  (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.kernel.ι f).hom f.hom =
    0
CategoryTheory.ObjectProperty.FullSubcategory.kernel_condition_hom.{v,
    u}
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms
      C]
  {P : CategoryTheory.ObjectProperty C}
  {X Y : P.FullSubcategory} (f : X ⟶ Y)
  [CategoryTheory.Limits.HasKernel f] :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.kernel.ι
          f).hom
      f.hom =
    0

Something wrong, better idea? Suggest a change

15.4.3. kernel_lift_ι_hom🔗

In a full subcategory, the kernel universal property at the level of underlying morphisms: (\operatorname{lift}(f, g, h)).\mathrm{hom} \circ (\ker(f).\iota).\mathrm{hom} = g.\mathrm{hom}.

Proof: Apply congr_arg (·.hom) to kernel.lift_ι f g h.

theorem

CategoryTheory.ObjectProperty.FullSubcategory.kernel_lift_ι_hom.{v, u}
  {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms C]
  {P : CategoryTheory.ObjectProperty C} {X Y W : P.FullSubcategory}
  (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f] (g : W ⟶ X)
  (h : CategoryTheory.CategoryStruct.comp g f = 0) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.kernel.lift f g h).hom
      (CategoryTheory.Limits.kernel.ι f).hom =
    g.hom
CategoryTheory.ObjectProperty.FullSubcategory.kernel_lift_ι_hom.{v,
    u}
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms
      C]
  {P : CategoryTheory.ObjectProperty C}
  {X Y W : P.FullSubcategory} (f : X ⟶ Y)
  [CategoryTheory.Limits.HasKernel f]
  (g : W ⟶ X)
  (h :
    CategoryTheory.CategoryStruct.comp g
        f =
      0) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.kernel.lift f
          g h).hom
      (CategoryTheory.Limits.kernel.ι
          f).hom =
    g.hom

Something wrong, better idea? Suggest a change

15.4.4. cokernel_condition_hom🔗

In a full subcategory, the cokernel condition f \circ \pi = 0 holds at the level of underlying morphisms: f.\mathrm{hom} \circ (\operatorname{coker}(f).\pi).\mathrm{hom} = 0.

Proof: Apply congr_arg (·.hom) to cokernel.condition f.

theorem

CategoryTheory.ObjectProperty.FullSubcategory.cokernel_condition_hom.{v,
    u}
  {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms C]
  {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory}
  (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] :
  CategoryTheory.CategoryStruct.comp f.hom
      (CategoryTheory.Limits.cokernel.π f).hom =
    0
CategoryTheory.ObjectProperty.FullSubcategory.cokernel_condition_hom.{v,
    u}
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms
      C]
  {P : CategoryTheory.ObjectProperty C}
  {X Y : P.FullSubcategory} (f : X ⟶ Y)
  [CategoryTheory.Limits.HasCokernel f] :
  CategoryTheory.CategoryStruct.comp f.hom
      (CategoryTheory.Limits.cokernel.π
          f).hom =
    0

Something wrong, better idea? Suggest a change

15.4.5. cokernel_π_desc_hom🔗

In a full subcategory, the cokernel universal property at the level of underlying morphisms: (\operatorname{coker}(f).\pi).\mathrm{hom} \circ (\operatorname{desc}(f, g, h)).\mathrm{hom} = g.\mathrm{hom}.

Proof: Apply congr_arg (·.hom) to cokernel.π_desc f g h.

theorem

CategoryTheory.ObjectProperty.FullSubcategory.cokernel_π_desc_hom.{v, u}
  {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms C]
  {P : CategoryTheory.ObjectProperty C} {X Y W : P.FullSubcategory}
  (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] (g : Y ⟶ W)
  (h : CategoryTheory.CategoryStruct.comp f g = 0) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.cokernel.π f).hom
      (CategoryTheory.Limits.cokernel.desc f g h).hom =
    g.hom
CategoryTheory.ObjectProperty.FullSubcategory.cokernel_π_desc_hom.{v,
    u}
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms
      C]
  {P : CategoryTheory.ObjectProperty C}
  {X Y W : P.FullSubcategory} (f : X ⟶ Y)
  [CategoryTheory.Limits.HasCokernel f]
  (g : Y ⟶ W)
  (h :
    CategoryTheory.CategoryStruct.comp f
        g =
      0) :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.cokernel.π
          f).hom
      (CategoryTheory.Limits.cokernel.desc
          f g h).hom =
    g.hom

Something wrong, better idea? Suggest a change

15.4.6. kernel_condition_homMk🔗

Variant of kernel_condition_hom for the post-simp normal form: if the morphism is homMk g, then (\ker(\operatorname{homMk}\ g).\iota).\mathrm{hom} \circ g = 0.

Proof: Reduces to kernel_condition_hom (ObjectProperty.homMk g).

theorem

CategoryTheory.ObjectProperty.FullSubcategory.kernel_condition_homMk.{v,
    u}
  {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms C]
  {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory}
  (g : X.obj ⟶ Y.obj)
  [CategoryTheory.Limits.HasKernel
      (CategoryTheory.ObjectProperty.homMk g)] :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.kernel.ι
          (CategoryTheory.ObjectProperty.homMk g)).hom
      g =
    0
CategoryTheory.ObjectProperty.FullSubcategory.kernel_condition_homMk.{v,
    u}
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms
      C]
  {P : CategoryTheory.ObjectProperty C}
  {X Y : P.FullSubcategory}
  (g : X.obj ⟶ Y.obj)
  [CategoryTheory.Limits.HasKernel
      (CategoryTheory.ObjectProperty.homMk
        g)] :
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.kernel.ι
          (CategoryTheory.ObjectProperty.homMk
            g)).hom
      g =
    0

Something wrong, better idea? Suggest a change

15.4.7. cokernel_condition_homMk🔗

Variant of cokernel_condition_hom for the post-simp normal form: if the morphism is presented as homMk g, then g \circ (\operatorname{coker}(\operatorname{homMk}\ g).\pi).\mathrm{hom} = 0.

Proof: Reduces to cokernel_condition_hom (ObjectProperty.homMk g).

theorem

CategoryTheory.ObjectProperty.FullSubcategory.cokernel_condition_homMk.{v,
    u}
  {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms C]
  {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory}
  (g : X.obj ⟶ Y.obj)
  [CategoryTheory.Limits.HasCokernel
      (CategoryTheory.ObjectProperty.homMk g)] :
  CategoryTheory.CategoryStruct.comp g
      (CategoryTheory.Limits.cokernel.π
          (CategoryTheory.ObjectProperty.homMk g)).hom =
    0
CategoryTheory.ObjectProperty.FullSubcategory.cokernel_condition_homMk.{v,
    u}
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroMorphisms
      C]
  {P : CategoryTheory.ObjectProperty C}
  {X Y : P.FullSubcategory}
  (g : X.obj ⟶ Y.obj)
  [CategoryTheory.Limits.HasCokernel
      (CategoryTheory.ObjectProperty.homMk
        g)] :
  CategoryTheory.CategoryStruct.comp g
      (CategoryTheory.Limits.cokernel.π
          (CategoryTheory.ObjectProperty.homMk
            g)).hom =
    0

Something wrong, better idea? Suggest a change