Documentation

Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap

Structured arrow categories on Comma.map #

We characterize structured arrow categories on arbitrary instances of Comma.map as a comma category itself.

source
@[implicit_reducible]
noncomputable def CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') :
Functor (StructuredArrow X (Comma.map α β)) (Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β)))

The functor establishing the equivalence StructuredArrow.commaMapEquivalence.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_obj_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') (Y : StructuredArrow X (Comma.map α β)) :
    ((commaMapEquivalenceFunctor α β X).obj Y).hom = homMk Y.right.hom ⋯
    source
    @[simp]
    theorem CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_map_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') {Y Z : StructuredArrow X (Comma.map α β)} (f : Y ⟶ Z) :
    ((commaMapEquivalenceFunctor α β X).map f).left = homMk (Hom.right f).left ⋯
    source
    @[simp]
    theorem CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_obj_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') (Y : StructuredArrow X (Comma.map α β)) :
    ((commaMapEquivalenceFunctor α β X).obj Y).right = mk Y.hom.right
    source
    @[simp]
    theorem CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_obj_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') (Y : StructuredArrow X (Comma.map α β)) :
    ((commaMapEquivalenceFunctor α β X).obj Y).left = mk Y.hom.left
    source
    @[simp]
    theorem CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_map_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') {Y Z : StructuredArrow X (Comma.map α β)} (f : Y ⟶ Z) :
    ((commaMapEquivalenceFunctor α β X).map f).right = homMk (Hom.right f).right ⋯
    source
    noncomputable def CategoryTheory.StructuredArrow.commaMapEquivalenceInverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') :
    Functor (Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β))) (StructuredArrow X (Comma.map α β))

    The inverse functor establishing the equivalence StructuredArrow.commaMapEquivalence.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.StructuredArrow.commaMapEquivalenceInverse_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') {Y Z : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β))} (f : Y ⟶ Z) :
      (commaMapEquivalenceInverse α β X).map f = homMk { left := Hom.right f.left, right := Hom.right f.right, w := ⋯ } ⋯
      source
      @[simp]
      theorem CategoryTheory.StructuredArrow.commaMapEquivalenceInverse_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') (Y : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β))) :
      (commaMapEquivalenceInverse α β X).obj Y = mk { left := Y.left.hom, right := Y.right.hom, w := ⋯ }
      source
      noncomputable def CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') :
      Functor.id (StructuredArrow X (Comma.map α β)) ≅ (commaMapEquivalenceFunctor α β X).comp (commaMapEquivalenceInverse α β X)

      The unit establishing the equivalence StructuredArrow.commaMapEquivalence.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_inv_app_right_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') (X✝ : StructuredArrow X (Comma.map α β)) :
        ((commaMapEquivalenceUnitIso α β X).inv.app X✝).right.right = CategoryStruct.id X✝.right.right
        source
        @[simp]
        theorem CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_hom_app_right_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') (X✝ : StructuredArrow X (Comma.map α β)) :
        ((commaMapEquivalenceUnitIso α β X).hom.app X✝).right.right = CategoryStruct.id X✝.right.right
        source
        @[simp]
        theorem CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_hom_app_right_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') (X✝ : StructuredArrow X (Comma.map α β)) :
        ((commaMapEquivalenceUnitIso α β X).hom.app X✝).right.left = CategoryStruct.id X✝.right.left
        source
        @[simp]
        theorem CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_inv_app_right_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') (X✝ : StructuredArrow X (Comma.map α β)) :
        ((commaMapEquivalenceUnitIso α β X).inv.app X✝).right.left = CategoryStruct.id X✝.right.left
        source
        noncomputable def CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') :
        (commaMapEquivalenceInverse α β X).comp (commaMapEquivalenceFunctor α β X) ≅ Functor.id (Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β)))

        The counit functor establishing the equivalence StructuredArrow.commaMapEquivalence.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_hom_app_right_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') (X✝ : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β))) :
          ((commaMapEquivalenceCounitIso α β X).hom.app X✝).right.right = CategoryStruct.id X✝.right.right
          source
          @[simp]
          theorem CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_hom_app_left_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') (X✝ : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β))) :
          ((commaMapEquivalenceCounitIso α β X).hom.app X✝).left.right = CategoryStruct.id X✝.left.right
          source
          @[simp]
          theorem CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_inv_app_right_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') (X✝ : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β))) :
          ((commaMapEquivalenceCounitIso α β X).inv.app X✝).right.right = CategoryStruct.id X✝.right.right
          source
          @[simp]
          theorem CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_inv_app_left_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') (X✝ : Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β))) :
          ((commaMapEquivalenceCounitIso α β X).inv.app X✝).left.right = CategoryStruct.id X✝.left.right
          source
          noncomputable def CategoryTheory.StructuredArrow.commaMapEquivalence {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor C T} {R : Functor D T} {C' : Type u₄} [Category.{v₄, u₄} C'] {D' : Type u₅} [Category.{v₅, u₅} D'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L' : Functor C' T'} {R' : Functor D' T'} {F₁ : Functor C C'} {F₂ : Functor D D'} {F : Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [IsIso β] (X : Comma L' R') :
          StructuredArrow X (Comma.map α β) ≌ Comma (map₂ (CategoryStruct.id (L'.obj X.left)) α) (map₂ X.hom (inv β))

          The structured arrow category on the functor Comma.map α β, with β a natural isomorphism, is equivalent to a comma category on two instances of StructuredArrow.map₂.

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