Theorems · Definition · category theory

CategoryTheory.DifferentialObject.HomSubtype

(S : Type u_1) →
  [inst : AddMonoidWithOne S] →
    (C : Type (u + 1)) →
      [inst_1 : CategoryTheory.LargeCategory C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          {FC : C → C → Type u_2} →
            {CC : C → Type u_3} →
              [inst_3 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
                [CategoryTheory.ConcreteCategory C FC] →
                  [inst_5 : CategoryTheory.HasShift C S] →
                    CategoryTheory.DifferentialObject S C → CategoryTheory.DifferentialObject S C → Type (max 0 u_2)

The type of C-morphisms that can be lifted back to morphisms in the category DifferentialObject.

Defined in

Mathlib.CategoryTheory.DifferentialObject

Cited by

0 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddMonoidWithOneCategoryTheory.LargeCategoryCategoryTheory.Limits.HasZeroMorphismsFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.HasShift