Loogle!

Result

Found 42 declarations mentioning CategoryTheory.Comma.map.

• CategoryTheory.Comma.map 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') : CategoryTheory.Functor (CategoryTheory.Comma L R) (CategoryTheory.Comma L' R')
• CategoryTheory.Comma.faithful_map 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F₁.Faithful] [F₂.Faithful] : (CategoryTheory.Comma.map α β).Faithful
• CategoryTheory.Comma.map_fst 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') : (CategoryTheory.Comma.map α β).comp (CategoryTheory.Comma.fst L' R') = (CategoryTheory.Comma.fst L R).comp F₁
• CategoryTheory.Comma.map_snd 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') : (CategoryTheory.Comma.map α β).comp (CategoryTheory.Comma.snd L' R') = (CategoryTheory.Comma.snd L R).comp F₂
• CategoryTheory.Comma.essSurj_map 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F₁.EssSurj] [F₂.EssSurj] [F.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] : (CategoryTheory.Comma.map α β).EssSurj
• CategoryTheory.Comma.full_map 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F.Faithful] [F₁.Full] [F₂.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] : (CategoryTheory.Comma.map α β).Full
• CategoryTheory.Comma.isEquivalenceMap 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [F₁.IsEquivalence] [F₂.IsEquivalence] [F.Faithful] [F.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] : (CategoryTheory.Comma.map α β).IsEquivalence
• CategoryTheory.Comma.mapFst 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') : (CategoryTheory.Comma.map α β).comp (CategoryTheory.Comma.fst L' R') ≅ (CategoryTheory.Comma.fst L R).comp F₁
• CategoryTheory.Comma.mapSnd 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') : (CategoryTheory.Comma.map α β).comp (CategoryTheory.Comma.snd L' R') ≅ (CategoryTheory.Comma.snd L R).comp F₂
• CategoryTheory.Comma.map_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.map α β).obj X).left = F₁.obj X.left
• CategoryTheory.Comma.map_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.map α β).obj X).right = F₂.obj X.right
• CategoryTheory.Comma.postIso 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (F : CategoryTheory.Functor T C) : CategoryTheory.Comma.post L R F ≅ CategoryTheory.Comma.map (L.comp F).leftUnitor.hom (R.comp F).leftUnitor.inv
• CategoryTheory.Comma.preLeftIso 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) : CategoryTheory.Comma.preLeft F L R ≅ CategoryTheory.Comma.map (F.comp L).rightUnitor.inv (CategoryTheory.CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv)
• CategoryTheory.Comma.preRightIso 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄} [CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (F : CategoryTheory.Functor C B) (R : CategoryTheory.Functor B T) : CategoryTheory.Comma.preRight L F R ≅ CategoryTheory.Comma.map (CategoryTheory.CategoryStruct.comp L.leftUnitor.hom L.rightUnitor.inv) (F.comp R).rightUnitor.hom
• CategoryTheory.Comma.mapFst_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.mapFst α β).hom.app X = CategoryTheory.CategoryStruct.id (F₁.obj X.left)
• CategoryTheory.Comma.mapFst_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.mapFst α β).inv.app X = CategoryTheory.CategoryStruct.id (F₁.obj X.left)
• CategoryTheory.Comma.mapSnd_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.mapSnd α β).hom.app X = CategoryTheory.CategoryStruct.id (F₂.obj X.right)
• CategoryTheory.Comma.mapSnd_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : (CategoryTheory.Comma.mapSnd α β).inv.app X = CategoryTheory.CategoryStruct.id (F₂.obj X.right)
• CategoryTheory.Comma.map_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.map α β).obj X).hom = CategoryTheory.CategoryStruct.comp (α.app X.left) (CategoryTheory.CategoryStruct.comp (F.map X.hom) (β.app X.right))
• CategoryTheory.Comma.map_map_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') {X Y : CategoryTheory.Comma L R} (φ : X ⟶ Y) : ((CategoryTheory.Comma.map α β).map φ).left = F₁.map φ.left
• CategoryTheory.Comma.map_map_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') {X Y : CategoryTheory.Comma L R} (φ : X ⟶ Y) : ((CategoryTheory.Comma.map α β).map φ).right = F₂.map φ.right
• CategoryTheory.StructuredArrow.commaMapEquivalence 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β) ≌ CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α) (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))
• CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') : CategoryTheory.Functor (CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)) (CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α) (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β)))
• CategoryTheory.StructuredArrow.commaMapEquivalenceInverse 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') : CategoryTheory.Functor (CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α) (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))) (CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β))
• CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') : CategoryTheory.Functor.id (CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)) ≅ (CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X).comp (CategoryTheory.StructuredArrow.commaMapEquivalenceInverse α β X)
• CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_obj_left 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)) : ((CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X).obj Y).left = CategoryTheory.StructuredArrow.mk Y.hom.left
• CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_obj_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)) : ((CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X).obj Y).right = CategoryTheory.StructuredArrow.mk Y.hom.right
• CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') : (CategoryTheory.StructuredArrow.commaMapEquivalenceInverse α β X).comp (CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X) ≅ CategoryTheory.Functor.id (CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α) (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β)))
• CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_obj_hom 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)) : ((CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X).obj Y).hom = CategoryTheory.StructuredArrow.homMk Y.right.hom ⋯
• CategoryTheory.StructuredArrow.commaMapEquivalenceInverse_obj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') (Y : CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α) (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))) : (CategoryTheory.StructuredArrow.commaMapEquivalenceInverse α β X).obj Y = CategoryTheory.StructuredArrow.mk { left := Y.left.hom, right := Y.right.hom, w := ⋯ }
• CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_hom_app_right_left 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') (X✝ : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)) : ((CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso α β X).hom.app X✝).right.left = CategoryTheory.CategoryStruct.id X✝.right.left
• CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_hom_app_right_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') (X✝ : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)) : ((CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso α β X).hom.app X✝).right.right = CategoryTheory.CategoryStruct.id X✝.right.right
• CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_inv_app_right_left 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') (X✝ : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)) : ((CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso α β X).inv.app X✝).right.left = CategoryTheory.CategoryStruct.id X✝.right.left
• CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_inv_app_right_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') (X✝ : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)) : ((CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso α β X).inv.app X✝).right.right = CategoryTheory.CategoryStruct.id X✝.right.right
• CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_map_left 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') {Y Z : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)} (f : Y ⟶ Z) : ((CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X).map f).left = CategoryTheory.StructuredArrow.homMk f.right.left ⋯
• CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor_map_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') {Y Z : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)} (f : Y ⟶ Z) : ((CategoryTheory.StructuredArrow.commaMapEquivalenceFunctor α β X).map f).right = CategoryTheory.StructuredArrow.homMk f.right.right ⋯
• CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_hom_app_left_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') (X✝ : CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α) (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))) : ((CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso α β X).hom.app X✝).left.right = CategoryTheory.CategoryStruct.id X✝.left.right
• CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_hom_app_right_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') (X✝ : CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α) (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))) : ((CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso α β X).hom.app X✝).right.right = CategoryTheory.CategoryStruct.id X✝.right.right
• CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_inv_app_left_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') (X✝ : CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α) (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))) : ((CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso α β X).inv.app X✝).left.right = CategoryTheory.CategoryStruct.id X✝.left.right
• CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_inv_app_right_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') (X✝ : CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α) (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))) : ((CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso α β X).inv.app X✝).right.right = CategoryTheory.CategoryStruct.id X✝.right.right
• CategoryTheory.StructuredArrow.commaMapEquivalenceInverse_map 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T} {R : CategoryTheory.Functor D T} {C' : Type u₄} [CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅} [CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'} {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') [CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R') {Y Z : CategoryTheory.Comma (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id (L'.obj X.left)) α) (CategoryTheory.StructuredArrow.map₂ X.hom (CategoryTheory.inv β))} (f : Y ⟶ Z) : (CategoryTheory.StructuredArrow.commaMapEquivalenceInverse α β X).map f = CategoryTheory.StructuredArrow.homMk { left := f.left.right, right := f.right.right, w := ⋯ } ⋯
• CategoryTheory.Comma.map_final 📋 Mathlib.CategoryTheory.Comma.Final
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {A' : Type u₄} [CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [CategoryTheory.Category.{v₅, u₅} B'] {T' : Type u₆} [CategoryTheory.Category.{v₆, u₆} T'] {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F : CategoryTheory.Functor A A'} {G : CategoryTheory.Functor B B'} {H : CategoryTheory.Functor T T'} (iL : F.comp L' ≅ L.comp H) (iR : G.comp R' ≅ R.comp H) [CategoryTheory.IsFiltered B] [R.Final] [R'.Final] [F.Final] [G.Final] : (CategoryTheory.Comma.map iL.hom iR.inv).Final

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision 40fea08