Documentation

Poly.ForMathlib.CategoryTheory.Comma.Over.Basic

source
@[simp]
theorem CategoryTheory.Over.mk_eta {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (U : Over X) :
mk U.hom = U
source
@[simp]
theorem CategoryTheory.Over.homMk_comp' {T : Type u₁} [Category.{v₁, u₁} T] {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp : CategoryStruct.comp (CategoryStruct.comp f g) (mk h).hom = (mk (CategoryStruct.comp f (CategoryStruct.comp g h))).hom) :
homMk (CategoryStruct.comp f g) fgh_comp = CategoryStruct.comp (homMk f ⋯) (homMk g ⋯)

A variant of homMk_comp that can trigger in simp.

source
@[simp]
theorem CategoryTheory.Over.homMk_comp'_assoc {T : Type u₁} [Category.{v₁, u₁} T] {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp : CategoryStruct.comp (CategoryStruct.comp f g) (mk h).hom = (mk (CategoryStruct.comp (CategoryStruct.comp f g) h)).hom) :
homMk (CategoryStruct.comp f g) fgh_comp = CategoryStruct.comp (homMk f ⋯) (homMk g ⋯)
source
@[simp]
theorem CategoryTheory.Over.homMk_id {T : Type u₁} [Category.{v₁, u₁} T] {X B : T} (f : X ⟶ B) (h : CategoryStruct.comp (CategoryStruct.id X) f = f) :
homMk (CategoryStruct.id X) h = CategoryStruct.id (mk f)
source
@[simp]
theorem CategoryTheory.Over.mkIdTerminal_from_left {T : Type u₁} [Category.{v₁, u₁} T] {B : T} (U : Over B) :
(mkIdTerminal.from U).left = U.hom
source
@[reducible, inline]
abbrev CategoryTheory.Over.Sigma {T : Type u₁} [Category.{v₁, u₁} T] {X : T} (Y : Over X) (U : Over Y.left) :
Over X

Over.Sigma Y U is a shorthand for (Over.map Y.hom).obj U. This is a category-theoretic analogue of Sigma for types.

Equations
Instances For
    source
    theorem CategoryTheory.Over.Sigma.hom {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {Y : Over X} (Z : Over Y.left) :
    (Y.Sigma Z).hom = CategoryStruct.comp Z.hom Y.hom
    source
    def CategoryTheory.Over.Sigma.map {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {Y : Over X} {Z Z' : Over Y.left} (g : Z ⟶ Z') :
    Y.Sigma Z ⟶ Y.Sigma Z'

    Σ_ is functorial in the second argument.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Over.Sigma.map_left {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {Y : Over X} {Z Z' : Over Y.left} {g : Z ⟶ Z'} :
      ((Over.map Y.hom).map g).left = g.left
      source
      theorem CategoryTheory.Over.Sigma.map_homMk_left {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {Y : Over X} {Z Z' : Over Y.left} {g : Z ⟶ Z'} :
      map g = homMk g.left ⋯
      source
      def CategoryTheory.Over.Sigma.fst {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {Y : Over X} (Z : Over Y.left) :
      Y.Sigma Z ⟶ Y

      The first projection of the sigma object.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Over.Sigma.fst_left {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {Y : Over X} (Z : Over Y.left) :
        (fst Z).left = Z.hom
        source
        @[simp]
        theorem CategoryTheory.Over.Sigma.map_comp_fst {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {Y : Over X} {Z Z' : Over Y.left} (g : Z ⟶ Z') :
        CategoryStruct.comp ((Over.map Y.hom).map g) (fst Z') = fst Z
        source
        def CategoryTheory.Over.Sigma.overHomMk {T : Type u₁} [Category.{v₁, u₁} T] {X : T} {Y : Over X} {Z Z' : Over Y.left} (g : Y.Sigma Z ⟶ Y.Sigma Z') (w : CategoryStruct.comp g (fst Z') = fst Z := by aesop_cat) :
        Z ⟶ Z'

        Promoting a morphism g : Σ_Y Z ⟶ Σ_Y Z' in Over X with g ≫ fst Z' = fst Z to a morphism Z ⟶ Z' in Over (Y.left).

        Equations
        Instances For