Loogle!

Result

Found 75 declarations mentioning CategoryTheory.Functor.leftUnitor.

CategoryTheory.Functor.leftUnitor 📋 Mathlib.CategoryTheory.Functor.Category
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : (CategoryTheory.Functor.id C).comp F ≅ F
CategoryTheory.Functor.leftUnitor_hom_app 📋 Mathlib.CategoryTheory.Functor.Category
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.leftUnitor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
CategoryTheory.Functor.leftUnitor_inv_app 📋 Mathlib.CategoryTheory.Functor.Category
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.leftUnitor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
CategoryTheory.Functor.triangleIso 📋 Mathlib.CategoryTheory.Whiskering
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) : F.associator (CategoryTheory.Functor.id B) G ≪≫ F.isoWhiskerLeft G.leftUnitor = CategoryTheory.Functor.isoWhiskerRight F.rightUnitor G
CategoryTheory.Functor.triangleIso_assoc 📋 Mathlib.CategoryTheory.Whiskering
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) {Z : CategoryTheory.Functor A C} (h : F.comp G ≅ Z) : F.associator (CategoryTheory.Functor.id B) G ≪≫ F.isoWhiskerLeft G.leftUnitor ≪≫ h = CategoryTheory.Functor.isoWhiskerRight F.rightUnitor G ≪≫ h
CategoryTheory.Functor.triangle 📋 Mathlib.CategoryTheory.Whiskering
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) : CategoryTheory.CategoryStruct.comp (F.associator (CategoryTheory.Functor.id B) G).hom (F.whiskerLeft G.leftUnitor.hom) = CategoryTheory.Functor.whiskerRight F.rightUnitor.hom G
CategoryTheory.NatIso.unop_leftUnitor 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} : CategoryTheory.NatIso.unop F.leftUnitor = F.unop.leftUnitor.symm ≪≫ CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Functor.unopId C).symm F.unop ≪≫ ((CategoryTheory.Functor.id Cᵒᵖ).unopComp F).symm
CategoryTheory.NatIso.op_leftUnitor 📋 Mathlib.CategoryTheory.Opposites
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} : CategoryTheory.NatIso.op F.leftUnitor = F.op.leftUnitor.symm ≪≫ CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Functor.opId C).symm F.op ≪≫ ((CategoryTheory.Functor.id C).opComp F).symm
CategoryTheory.Pi.equivalenceOfEquiv_counitIso 📋 Mathlib.CategoryTheory.Pi.Basic
{I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (e : J ≃ I) : (CategoryTheory.Pi.equivalenceOfEquiv C e).counitIso = CategoryTheory.NatIso.pi' fun i => ((CategoryTheory.Functor.pi' fun i' => CategoryTheory.Pi.eval C (e i')).associator (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm i)) (CategoryTheory.Pi.eqToEquivalence C ⋯).functor).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Functor.pi'CompEval (fun i' => CategoryTheory.Pi.eval C (e i')) (e.symm i)) (CategoryTheory.Pi.eqToEquivalence C ⋯).functor ≪≫ CategoryTheory.Pi.evalCompEqToEquivalenceFunctor C ⋯ ≪≫ (CategoryTheory.Pi.eval C i).leftUnitor.symm
CategoryTheory.Pi.equivalenceOfEquiv_unitIso 📋 Mathlib.CategoryTheory.Pi.Basic
{I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (e : J ≃ I) : (CategoryTheory.Pi.equivalenceOfEquiv C e).unitIso = CategoryTheory.NatIso.pi' fun i' => (CategoryTheory.Pi.eval (fun i => C (e i)) i').leftUnitor ≪≫ (CategoryTheory.Pi.evalCompEqToEquivalenceFunctor (fun j => C (e j)) ⋯).symm ≪≫ (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))).isoWhiskerLeft (CategoryTheory.Pi.eqToEquivalenceFunctorIso C ⇑e ⋯).symm ≪≫ (CategoryTheory.Functor.pi'CompEval (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))).comp (CategoryTheory.Pi.eqToEquivalence C ⋯).functor).symm ≪≫ (CategoryTheory.Functor.pi' (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))).comp).isoWhiskerLeft (CategoryTheory.Functor.pi'CompEval (CategoryTheory.Pi.eval fun i => C (e i')) (CategoryTheory.Pi.eqToEquivalence C ⋯).functor).symm ≪≫ ((CategoryTheory.Functor.pi' (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))).comp).associator (CategoryTheory.Functor.pi' (CategoryTheory.Pi.eval fun i => C (e i'))) (CategoryTheory.Pi.eval (fun i => C (e i')) (CategoryTheory.Pi.eqToEquivalence C ⋯).functor)).symm
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
{B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {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.Adjunction.left_triangle 📋 Mathlib.CategoryTheory.Adjunction.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight adj.unit F) (CategoryTheory.CategoryStruct.comp (F.associator G F).hom (F.whiskerLeft adj.counit)) = CategoryTheory.CategoryStruct.comp F.leftUnitor.hom F.rightUnitor.inv
CategoryTheory.Adjunction.right_triangle 📋 Mathlib.CategoryTheory.Adjunction.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) : CategoryTheory.CategoryStruct.comp (G.whiskerLeft adj.unit) (CategoryTheory.CategoryStruct.comp (G.associator F G).inv (CategoryTheory.Functor.whiskerRight adj.counit G)) = CategoryTheory.CategoryStruct.comp G.rightUnitor.hom G.leftUnitor.inv
CategoryTheory.Cat.Hom.toNatIso_leftUnitor 📋 Mathlib.CategoryTheory.Category.Cat
{B C : CategoryTheory.Cat} (F : B ⟶ C) : CategoryTheory.Cat.Hom.toNatIso (CategoryTheory.Bicategory.leftUnitor F) = F.toFunctor.leftUnitor
CategoryTheory.Cat.leftUnitor_hom_toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
{B C : CategoryTheory.Cat} (F : B ⟶ C) : (CategoryTheory.Bicategory.leftUnitor F).hom.toNatTrans = F.toFunctor.leftUnitor.hom
CategoryTheory.Cat.leftUnitor_inv_toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
{B C : CategoryTheory.Cat} (F : B ⟶ C) : (CategoryTheory.Bicategory.leftUnitor F).inv.toNatTrans = F.toFunctor.leftUnitor.inv
CategoryTheory.Limits.colimit.pre_id 📋 Mathlib.CategoryTheory.Limits.HasLimits
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.colimit.pre F (CategoryTheory.Functor.id J) = CategoryTheory.Limits.colim.map F.leftUnitor.hom
CategoryTheory.Limits.limit.id_pre 📋 Mathlib.CategoryTheory.Limits.HasLimits
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.limit.pre F (CategoryTheory.Functor.id J) = CategoryTheory.Limits.lim.map F.leftUnitor.inv
CategoryTheory.StructuredArrow.map₂IdIso 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor C D} (T : D) (α : T ⟶ (CategoryTheory.Functor.id D).obj T) (β : R.comp (CategoryTheory.Functor.id D) ⟶ (CategoryTheory.Functor.id C).comp R) (hα : α = CategoryTheory.CategoryStruct.id T := by cat_disch) (hβ : β = CategoryTheory.CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv := by cat_disch) : CategoryTheory.StructuredArrow.map₂ α β ≅ CategoryTheory.Functor.id (CategoryTheory.StructuredArrow T R)
CategoryTheory.CostructuredArrow.map₂IdIso 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} (α : (CategoryTheory.Functor.id C).comp S ⟶ S.comp (CategoryTheory.Functor.id D)) (T : D) (β : (CategoryTheory.Functor.id D).obj T ⟶ T) (hα : α = CategoryTheory.CategoryStruct.comp S.leftUnitor.hom S.rightUnitor.inv := by cat_disch) (hβ : β = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id D).obj T) := by cat_disch) : CategoryTheory.CostructuredArrow.map₂ α β ≅ CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow S T)
CategoryTheory.StructuredArrow.map₂IdIso_hom_app_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor C D} (T : D) (α : T ⟶ (CategoryTheory.Functor.id D).obj T) (β : R.comp (CategoryTheory.Functor.id D) ⟶ (CategoryTheory.Functor.id C).comp R) (hα : α = CategoryTheory.CategoryStruct.id T := by cat_disch) (hβ : β = CategoryTheory.CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv := by cat_disch) (X : CategoryTheory.StructuredArrow T R) : ((CategoryTheory.StructuredArrow.map₂IdIso T α β hα hβ).hom.app X).right = CategoryTheory.CategoryStruct.id X.right
CategoryTheory.StructuredArrow.map₂IdIso_inv_app_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {R : CategoryTheory.Functor C D} (T : D) (α : T ⟶ (CategoryTheory.Functor.id D).obj T) (β : R.comp (CategoryTheory.Functor.id D) ⟶ (CategoryTheory.Functor.id C).comp R) (hα : α = CategoryTheory.CategoryStruct.id T := by cat_disch) (hβ : β = CategoryTheory.CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv := by cat_disch) (X : CategoryTheory.StructuredArrow T R) : ((CategoryTheory.StructuredArrow.map₂IdIso T α β hα hβ).inv.app X).right = CategoryTheory.CategoryStruct.id X.right
CategoryTheory.CostructuredArrow.map₂IdIso_hom_app_left 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} (α : (CategoryTheory.Functor.id C).comp S ⟶ S.comp (CategoryTheory.Functor.id D)) (T : D) (β : (CategoryTheory.Functor.id D).obj T ⟶ T) (hα : α = CategoryTheory.CategoryStruct.comp S.leftUnitor.hom S.rightUnitor.inv := by cat_disch) (hβ : β = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id D).obj T) := by cat_disch) (X : CategoryTheory.CostructuredArrow S T) : ((CategoryTheory.CostructuredArrow.map₂IdIso α T β hα hβ).hom.app X).left = CategoryTheory.CategoryStruct.id X.left
CategoryTheory.CostructuredArrow.map₂IdIso_inv_app_left 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} (α : (CategoryTheory.Functor.id C).comp S ⟶ S.comp (CategoryTheory.Functor.id D)) (T : D) (β : (CategoryTheory.Functor.id D).obj T ⟶ T) (hα : α = CategoryTheory.CategoryStruct.comp S.leftUnitor.hom S.rightUnitor.inv := by cat_disch) (hβ : β = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id D).obj T) := by cat_disch) (X : CategoryTheory.CostructuredArrow S T) : ((CategoryTheory.CostructuredArrow.map₂IdIso α T β hα hβ).inv.app X).left = CategoryTheory.CategoryStruct.id X.left
CategoryTheory.CostructuredArrow.map₂Iso 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : C ≌ A} {G : D ≌ B} (α : F.functor.comp U ⟶ S.comp G.functor) (α' : F.inverse.comp S ⟶ U.comp G.inverse) (hα'α : CategoryTheory.CategoryStruct.comp S.leftUnitor.hom (CategoryTheory.CategoryStruct.comp S.rightUnitor.inv (CategoryTheory.CategoryStruct.comp (S.whiskerLeft G.unitIso.hom) (S.associator G.functor G.inverse).inv)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom S) (CategoryTheory.CategoryStruct.comp (F.functor.associator F.inverse S).hom (CategoryTheory.CategoryStruct.comp (F.functor.whiskerLeft α') (CategoryTheory.CategoryStruct.comp (F.functor.associator U G.inverse).inv (CategoryTheory.Functor.whiskerRight α G.inverse))))) (hαα' : CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft α) (CategoryTheory.CategoryStruct.comp (F.inverse.associator S G.functor).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α' G.functor) (CategoryTheory.CategoryStruct.comp (U.associator G.inverse G.functor).hom (U.whiskerLeft G.counitIso.hom)))) = CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor U).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.counitIso.hom U) (CategoryTheory.CategoryStruct.comp U.leftUnitor.hom U.rightUnitor.inv))) (β : G.functor.obj T ⟶ V) (β' : G.inverse.obj V ⟶ T) (hββ' : CategoryTheory.CategoryStruct.comp (G.inverse.map β) β' = G.unitIso.inv.app T) (hβ'β : CategoryTheory.CategoryStruct.comp (G.functor.map β') β = G.counitIso.hom.app V) : CategoryTheory.CostructuredArrow S T ≌ CategoryTheory.CostructuredArrow U V
CategoryTheory.StructuredArrow.map₂Iso 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : C ≌ A} {G : D ≌ B} (α : L' ⟶ G.functor.obj L) (α' : L ⟶ G.inverse.obj L') (β : R.comp G.functor ⟶ F.functor.comp R') (β' : R'.comp G.inverse ⟶ F.inverse.comp R) (hαα' : CategoryTheory.CategoryStruct.comp α (G.functor.map α') = G.counitIso.inv.app L') (hα'α : CategoryTheory.CategoryStruct.comp α' (G.inverse.map α) = G.unitIso.hom.app L) (hββ' : CategoryTheory.CategoryStruct.comp R.rightUnitor.hom (CategoryTheory.CategoryStruct.comp R.leftUnitor.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom R) (F.functor.associator F.inverse R).hom)) = CategoryTheory.CategoryStruct.comp (R.whiskerLeft G.unitIso.hom) (CategoryTheory.CategoryStruct.comp (R.associator G.functor G.inverse).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G.inverse) (CategoryTheory.CategoryStruct.comp (F.functor.associator R' G.inverse).hom (F.functor.whiskerLeft β'))))) (hβ'β : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β' G.functor) (CategoryTheory.CategoryStruct.comp (F.inverse.associator R G.functor).hom (CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft β) (CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor R').inv (CategoryTheory.Functor.whiskerRight F.counitIso.hom R')))) = CategoryTheory.CategoryStruct.comp (R'.associator G.inverse G.functor).hom (CategoryTheory.CategoryStruct.comp (R'.whiskerLeft G.counitIso.hom) (CategoryTheory.CategoryStruct.comp R'.rightUnitor.hom R'.leftUnitor.inv))) : CategoryTheory.StructuredArrow L R ≌ CategoryTheory.StructuredArrow L' R'
CategoryTheory.CostructuredArrow.map₂Iso_functor 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : C ≌ A} {G : D ≌ B} (α : F.functor.comp U ⟶ S.comp G.functor) (α' : F.inverse.comp S ⟶ U.comp G.inverse) (hα'α : CategoryTheory.CategoryStruct.comp S.leftUnitor.hom (CategoryTheory.CategoryStruct.comp S.rightUnitor.inv (CategoryTheory.CategoryStruct.comp (S.whiskerLeft G.unitIso.hom) (S.associator G.functor G.inverse).inv)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom S) (CategoryTheory.CategoryStruct.comp (F.functor.associator F.inverse S).hom (CategoryTheory.CategoryStruct.comp (F.functor.whiskerLeft α') (CategoryTheory.CategoryStruct.comp (F.functor.associator U G.inverse).inv (CategoryTheory.Functor.whiskerRight α G.inverse))))) (hαα' : CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft α) (CategoryTheory.CategoryStruct.comp (F.inverse.associator S G.functor).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α' G.functor) (CategoryTheory.CategoryStruct.comp (U.associator G.inverse G.functor).hom (U.whiskerLeft G.counitIso.hom)))) = CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor U).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.counitIso.hom U) (CategoryTheory.CategoryStruct.comp U.leftUnitor.hom U.rightUnitor.inv))) (β : G.functor.obj T ⟶ V) (β' : G.inverse.obj V ⟶ T) (hββ' : CategoryTheory.CategoryStruct.comp (G.inverse.map β) β' = G.unitIso.inv.app T) (hβ'β : CategoryTheory.CategoryStruct.comp (G.functor.map β') β = G.counitIso.hom.app V) : (CategoryTheory.CostructuredArrow.map₂Iso α α' hα'α hαα' β β' hββ' hβ'β).functor = CategoryTheory.CostructuredArrow.map₂ α β
CategoryTheory.CostructuredArrow.map₂Iso_inverse 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : C ≌ A} {G : D ≌ B} (α : F.functor.comp U ⟶ S.comp G.functor) (α' : F.inverse.comp S ⟶ U.comp G.inverse) (hα'α : CategoryTheory.CategoryStruct.comp S.leftUnitor.hom (CategoryTheory.CategoryStruct.comp S.rightUnitor.inv (CategoryTheory.CategoryStruct.comp (S.whiskerLeft G.unitIso.hom) (S.associator G.functor G.inverse).inv)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom S) (CategoryTheory.CategoryStruct.comp (F.functor.associator F.inverse S).hom (CategoryTheory.CategoryStruct.comp (F.functor.whiskerLeft α') (CategoryTheory.CategoryStruct.comp (F.functor.associator U G.inverse).inv (CategoryTheory.Functor.whiskerRight α G.inverse))))) (hαα' : CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft α) (CategoryTheory.CategoryStruct.comp (F.inverse.associator S G.functor).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α' G.functor) (CategoryTheory.CategoryStruct.comp (U.associator G.inverse G.functor).hom (U.whiskerLeft G.counitIso.hom)))) = CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor U).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.counitIso.hom U) (CategoryTheory.CategoryStruct.comp U.leftUnitor.hom U.rightUnitor.inv))) (β : G.functor.obj T ⟶ V) (β' : G.inverse.obj V ⟶ T) (hββ' : CategoryTheory.CategoryStruct.comp (G.inverse.map β) β' = G.unitIso.inv.app T) (hβ'β : CategoryTheory.CategoryStruct.comp (G.functor.map β') β = G.counitIso.hom.app V) : (CategoryTheory.CostructuredArrow.map₂Iso α α' hα'α hαα' β β' hββ' hβ'β).inverse = CategoryTheory.CostructuredArrow.map₂ α' β'
CategoryTheory.StructuredArrow.map₂Iso_functor 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : C ≌ A} {G : D ≌ B} (α : L' ⟶ G.functor.obj L) (α' : L ⟶ G.inverse.obj L') (β : R.comp G.functor ⟶ F.functor.comp R') (β' : R'.comp G.inverse ⟶ F.inverse.comp R) (hαα' : CategoryTheory.CategoryStruct.comp α (G.functor.map α') = G.counitIso.inv.app L') (hα'α : CategoryTheory.CategoryStruct.comp α' (G.inverse.map α) = G.unitIso.hom.app L) (hββ' : CategoryTheory.CategoryStruct.comp R.rightUnitor.hom (CategoryTheory.CategoryStruct.comp R.leftUnitor.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom R) (F.functor.associator F.inverse R).hom)) = CategoryTheory.CategoryStruct.comp (R.whiskerLeft G.unitIso.hom) (CategoryTheory.CategoryStruct.comp (R.associator G.functor G.inverse).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G.inverse) (CategoryTheory.CategoryStruct.comp (F.functor.associator R' G.inverse).hom (F.functor.whiskerLeft β'))))) (hβ'β : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β' G.functor) (CategoryTheory.CategoryStruct.comp (F.inverse.associator R G.functor).hom (CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft β) (CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor R').inv (CategoryTheory.Functor.whiskerRight F.counitIso.hom R')))) = CategoryTheory.CategoryStruct.comp (R'.associator G.inverse G.functor).hom (CategoryTheory.CategoryStruct.comp (R'.whiskerLeft G.counitIso.hom) (CategoryTheory.CategoryStruct.comp R'.rightUnitor.hom R'.leftUnitor.inv))) : (CategoryTheory.StructuredArrow.map₂Iso α α' β β' hαα' hα'α hββ' hβ'β).functor = CategoryTheory.StructuredArrow.map₂ α β
CategoryTheory.StructuredArrow.map₂Iso_inverse 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : C ≌ A} {G : D ≌ B} (α : L' ⟶ G.functor.obj L) (α' : L ⟶ G.inverse.obj L') (β : R.comp G.functor ⟶ F.functor.comp R') (β' : R'.comp G.inverse ⟶ F.inverse.comp R) (hαα' : CategoryTheory.CategoryStruct.comp α (G.functor.map α') = G.counitIso.inv.app L') (hα'α : CategoryTheory.CategoryStruct.comp α' (G.inverse.map α) = G.unitIso.hom.app L) (hββ' : CategoryTheory.CategoryStruct.comp R.rightUnitor.hom (CategoryTheory.CategoryStruct.comp R.leftUnitor.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom R) (F.functor.associator F.inverse R).hom)) = CategoryTheory.CategoryStruct.comp (R.whiskerLeft G.unitIso.hom) (CategoryTheory.CategoryStruct.comp (R.associator G.functor G.inverse).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G.inverse) (CategoryTheory.CategoryStruct.comp (F.functor.associator R' G.inverse).hom (F.functor.whiskerLeft β'))))) (hβ'β : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β' G.functor) (CategoryTheory.CategoryStruct.comp (F.inverse.associator R G.functor).hom (CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft β) (CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor R').inv (CategoryTheory.Functor.whiskerRight F.counitIso.hom R')))) = CategoryTheory.CategoryStruct.comp (R'.associator G.inverse G.functor).hom (CategoryTheory.CategoryStruct.comp (R'.whiskerLeft G.counitIso.hom) (CategoryTheory.CategoryStruct.comp R'.rightUnitor.hom R'.leftUnitor.inv))) : (CategoryTheory.StructuredArrow.map₂Iso α α' β β' hαα' hα'α hββ' hβ'β).inverse = CategoryTheory.StructuredArrow.map₂ α' β'
CategoryTheory.StructuredArrow.map₂Iso_counitIso 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : C ≌ A} {G : D ≌ B} (α : L' ⟶ G.functor.obj L) (α' : L ⟶ G.inverse.obj L') (β : R.comp G.functor ⟶ F.functor.comp R') (β' : R'.comp G.inverse ⟶ F.inverse.comp R) (hαα' : CategoryTheory.CategoryStruct.comp α (G.functor.map α') = G.counitIso.inv.app L') (hα'α : CategoryTheory.CategoryStruct.comp α' (G.inverse.map α) = G.unitIso.hom.app L) (hββ' : CategoryTheory.CategoryStruct.comp R.rightUnitor.hom (CategoryTheory.CategoryStruct.comp R.leftUnitor.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom R) (F.functor.associator F.inverse R).hom)) = CategoryTheory.CategoryStruct.comp (R.whiskerLeft G.unitIso.hom) (CategoryTheory.CategoryStruct.comp (R.associator G.functor G.inverse).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G.inverse) (CategoryTheory.CategoryStruct.comp (F.functor.associator R' G.inverse).hom (F.functor.whiskerLeft β'))))) (hβ'β : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β' G.functor) (CategoryTheory.CategoryStruct.comp (F.inverse.associator R G.functor).hom (CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft β) (CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor R').inv (CategoryTheory.Functor.whiskerRight F.counitIso.hom R')))) = CategoryTheory.CategoryStruct.comp (R'.associator G.inverse G.functor).hom (CategoryTheory.CategoryStruct.comp (R'.whiskerLeft G.counitIso.hom) (CategoryTheory.CategoryStruct.comp R'.rightUnitor.hom R'.leftUnitor.inv))) : (CategoryTheory.StructuredArrow.map₂Iso α α' β β' hαα' hα'α hββ' hβ'β).counitIso = CategoryTheory.StructuredArrow.map₂CompMap₂Iso α β α' β' ≪≫ CategoryTheory.StructuredArrow.map₂Congr (CategoryTheory.CategoryStruct.comp α (G.functor.map α')) (CategoryTheory.CategoryStruct.comp (R'.associator G.inverse G.functor).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β' G.functor) (CategoryTheory.CategoryStruct.comp (F.inverse.associator R G.functor).hom (CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft β) (F.inverse.associator F.functor R').inv)))) F.counitIso G.counitIso (CategoryTheory.CategoryStruct.id L') (CategoryTheory.CategoryStruct.comp R'.rightUnitor.hom R'.leftUnitor.inv) ⋯ ⋯ ≪≫ CategoryTheory.StructuredArrow.map₂IdIso L' (CategoryTheory.CategoryStruct.id L') (CategoryTheory.CategoryStruct.comp R'.rightUnitor.hom R'.leftUnitor.inv) ⋯ ⋯
CategoryTheory.CostructuredArrow.map₂Iso_counitIso 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : C ≌ A} {G : D ≌ B} (α : F.functor.comp U ⟶ S.comp G.functor) (α' : F.inverse.comp S ⟶ U.comp G.inverse) (hα'α : CategoryTheory.CategoryStruct.comp S.leftUnitor.hom (CategoryTheory.CategoryStruct.comp S.rightUnitor.inv (CategoryTheory.CategoryStruct.comp (S.whiskerLeft G.unitIso.hom) (S.associator G.functor G.inverse).inv)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom S) (CategoryTheory.CategoryStruct.comp (F.functor.associator F.inverse S).hom (CategoryTheory.CategoryStruct.comp (F.functor.whiskerLeft α') (CategoryTheory.CategoryStruct.comp (F.functor.associator U G.inverse).inv (CategoryTheory.Functor.whiskerRight α G.inverse))))) (hαα' : CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft α) (CategoryTheory.CategoryStruct.comp (F.inverse.associator S G.functor).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α' G.functor) (CategoryTheory.CategoryStruct.comp (U.associator G.inverse G.functor).hom (U.whiskerLeft G.counitIso.hom)))) = CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor U).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.counitIso.hom U) (CategoryTheory.CategoryStruct.comp U.leftUnitor.hom U.rightUnitor.inv))) (β : G.functor.obj T ⟶ V) (β' : G.inverse.obj V ⟶ T) (hββ' : CategoryTheory.CategoryStruct.comp (G.inverse.map β) β' = G.unitIso.inv.app T) (hβ'β : CategoryTheory.CategoryStruct.comp (G.functor.map β') β = G.counitIso.hom.app V) : (CategoryTheory.CostructuredArrow.map₂Iso α α' hα'α hαα' β β' hββ' hβ'β).counitIso = CategoryTheory.CostructuredArrow.map₂CompMap₂Iso α β α' β' ≪≫ CategoryTheory.CostructuredArrow.map₂Congr (CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor U).hom (CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft α) (CategoryTheory.CategoryStruct.comp (F.inverse.associator S G.functor).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α' G.functor) (U.associator G.inverse G.functor).hom)))) (CategoryTheory.CategoryStruct.comp (G.functor.map β') β) F.counitIso G.counitIso (CategoryTheory.CategoryStruct.comp U.leftUnitor.hom U.rightUnitor.inv) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id B).obj V)) ⋯ ⋯ ≪≫ CategoryTheory.CostructuredArrow.map₂IdIso (CategoryTheory.CategoryStruct.comp U.leftUnitor.hom U.rightUnitor.inv) V (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id B).obj V)) ⋯ ⋯
CategoryTheory.StructuredArrow.map₂Iso_unitIso 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B} {R' : CategoryTheory.Functor A B} {F : C ≌ A} {G : D ≌ B} (α : L' ⟶ G.functor.obj L) (α' : L ⟶ G.inverse.obj L') (β : R.comp G.functor ⟶ F.functor.comp R') (β' : R'.comp G.inverse ⟶ F.inverse.comp R) (hαα' : CategoryTheory.CategoryStruct.comp α (G.functor.map α') = G.counitIso.inv.app L') (hα'α : CategoryTheory.CategoryStruct.comp α' (G.inverse.map α) = G.unitIso.hom.app L) (hββ' : CategoryTheory.CategoryStruct.comp R.rightUnitor.hom (CategoryTheory.CategoryStruct.comp R.leftUnitor.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom R) (F.functor.associator F.inverse R).hom)) = CategoryTheory.CategoryStruct.comp (R.whiskerLeft G.unitIso.hom) (CategoryTheory.CategoryStruct.comp (R.associator G.functor G.inverse).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G.inverse) (CategoryTheory.CategoryStruct.comp (F.functor.associator R' G.inverse).hom (F.functor.whiskerLeft β'))))) (hβ'β : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β' G.functor) (CategoryTheory.CategoryStruct.comp (F.inverse.associator R G.functor).hom (CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft β) (CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor R').inv (CategoryTheory.Functor.whiskerRight F.counitIso.hom R')))) = CategoryTheory.CategoryStruct.comp (R'.associator G.inverse G.functor).hom (CategoryTheory.CategoryStruct.comp (R'.whiskerLeft G.counitIso.hom) (CategoryTheory.CategoryStruct.comp R'.rightUnitor.hom R'.leftUnitor.inv))) : (CategoryTheory.StructuredArrow.map₂Iso α α' β β' hαα' hα'α hββ' hβ'β).unitIso = (CategoryTheory.StructuredArrow.map₂IdIso L (CategoryTheory.CategoryStruct.id L) (CategoryTheory.CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv) ⋯ ⋯).symm ≪≫ CategoryTheory.StructuredArrow.map₂Congr (CategoryTheory.CategoryStruct.id L) (CategoryTheory.CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv) F.unitIso G.unitIso (CategoryTheory.CategoryStruct.comp α' (G.inverse.map α)) (CategoryTheory.CategoryStruct.comp (R.associator G.functor G.inverse).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G.inverse) (CategoryTheory.CategoryStruct.comp (F.functor.associator R' G.inverse).hom (CategoryTheory.CategoryStruct.comp (F.functor.whiskerLeft β') (F.functor.associator F.inverse R).inv)))) ⋯ ⋯ ≪≫ (CategoryTheory.StructuredArrow.map₂CompMap₂Iso α' β' α β).symm
CategoryTheory.CostructuredArrow.map₂Iso_unitIso 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : C ≌ A} {G : D ≌ B} (α : F.functor.comp U ⟶ S.comp G.functor) (α' : F.inverse.comp S ⟶ U.comp G.inverse) (hα'α : CategoryTheory.CategoryStruct.comp S.leftUnitor.hom (CategoryTheory.CategoryStruct.comp S.rightUnitor.inv (CategoryTheory.CategoryStruct.comp (S.whiskerLeft G.unitIso.hom) (S.associator G.functor G.inverse).inv)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom S) (CategoryTheory.CategoryStruct.comp (F.functor.associator F.inverse S).hom (CategoryTheory.CategoryStruct.comp (F.functor.whiskerLeft α') (CategoryTheory.CategoryStruct.comp (F.functor.associator U G.inverse).inv (CategoryTheory.Functor.whiskerRight α G.inverse))))) (hαα' : CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft α) (CategoryTheory.CategoryStruct.comp (F.inverse.associator S G.functor).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α' G.functor) (CategoryTheory.CategoryStruct.comp (U.associator G.inverse G.functor).hom (U.whiskerLeft G.counitIso.hom)))) = CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor U).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.counitIso.hom U) (CategoryTheory.CategoryStruct.comp U.leftUnitor.hom U.rightUnitor.inv))) (β : G.functor.obj T ⟶ V) (β' : G.inverse.obj V ⟶ T) (hββ' : CategoryTheory.CategoryStruct.comp (G.inverse.map β) β' = G.unitIso.inv.app T) (hβ'β : CategoryTheory.CategoryStruct.comp (G.functor.map β') β = G.counitIso.hom.app V) : (CategoryTheory.CostructuredArrow.map₂Iso α α' hα'α hαα' β β' hββ' hβ'β).unitIso = (CategoryTheory.CostructuredArrow.map₂IdIso (CategoryTheory.CategoryStruct.comp S.leftUnitor.hom S.rightUnitor.inv) T (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id D).obj T)) ⋯ ⋯).symm ≪≫ CategoryTheory.CostructuredArrow.map₂Congr (CategoryTheory.CategoryStruct.comp S.leftUnitor.hom S.rightUnitor.inv) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id D).obj T)) F.unitIso G.unitIso (CategoryTheory.CategoryStruct.comp (F.functor.associator F.inverse S).hom (CategoryTheory.CategoryStruct.comp (F.functor.whiskerLeft α') (CategoryTheory.CategoryStruct.comp (F.functor.associator U G.inverse).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α G.inverse) (S.associator G.functor G.inverse).hom)))) (CategoryTheory.CategoryStruct.comp (G.inverse.map β) β') ⋯ ⋯ ≪≫ (CategoryTheory.CostructuredArrow.map₂CompMap₂Iso α' β' α β).symm
CategoryTheory.NatTrans.IsMonoidal.instHomFunctorLeftUnitor 📋 Mathlib.CategoryTheory.Monoidal.NaturalTransformation
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) [F.LaxMonoidal] : CategoryTheory.NatTrans.IsMonoidal F.leftUnitor.hom
CategoryTheory.conjugateEquiv_leftUnitor_hom 📋 Mathlib.CategoryTheory.Adjunction.Mates
{A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] {L : CategoryTheory.Functor A B} {R : CategoryTheory.Functor B A} (adj : L ⊣ R) : (CategoryTheory.conjugateEquiv adj (CategoryTheory.Adjunction.id.comp adj)) L.leftUnitor.hom = R.rightUnitor.inv
CategoryTheory.conjugateEquiv_rightUnitor_hom 📋 Mathlib.CategoryTheory.Adjunction.Mates
{A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] {L : CategoryTheory.Functor A B} {R : CategoryTheory.Functor B A} (adj : L ⊣ R) : (CategoryTheory.conjugateEquiv adj (adj.comp CategoryTheory.Adjunction.id)) L.rightUnitor.hom = R.leftUnitor.inv
CategoryTheory.mateEquiv_apply 📋 Mathlib.CategoryTheory.Adjunction.Mates
{C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.Category.{v₄, u₄} F] {G : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D F} {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {L₂ : CategoryTheory.Functor E F} {R₂ : CategoryTheory.Functor F E} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (α : CategoryTheory.TwoSquare G L₁ L₂ H) : (CategoryTheory.mateEquiv adj₁ adj₂) α = CategoryTheory.TwoSquare.mk R₁ H G R₂ (CategoryTheory.CategoryStruct.comp (R₁.comp G).rightUnitor.inv (CategoryTheory.CategoryStruct.comp ((R₁.comp G).whiskerLeft adj₂.unit) (CategoryTheory.CategoryStruct.comp (R₁.associator G (L₂.comp R₂)).hom (CategoryTheory.CategoryStruct.comp (R₁.whiskerLeft (G.associator L₂ R₂).inv) (CategoryTheory.CategoryStruct.comp (R₁.whiskerLeft (CategoryTheory.Functor.whiskerRight α.natTrans R₂)) (CategoryTheory.CategoryStruct.comp (R₁.whiskerLeft (L₁.associator H R₂).hom) (CategoryTheory.CategoryStruct.comp (R₁.associator L₁ (H.comp R₂)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight adj₁.counit (H.comp R₂)) (H.comp R₂).leftUnitor.hom))))))))
CategoryTheory.mateEquiv_symm_apply 📋 Mathlib.CategoryTheory.Adjunction.Mates
{C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.Category.{v₄, u₄} F] {G : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D F} {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {L₂ : CategoryTheory.Functor E F} {R₂ : CategoryTheory.Functor F E} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (β : CategoryTheory.TwoSquare R₁ H G R₂) : (CategoryTheory.mateEquiv adj₁ adj₂).symm β = CategoryTheory.TwoSquare.mk G L₁ L₂ H (CategoryTheory.CategoryStruct.comp (G.comp L₂).leftUnitor.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight adj₁.unit (G.comp L₂)) (CategoryTheory.CategoryStruct.comp ((L₁.comp R₁).associator G L₂).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L₁.associator R₁ G).hom L₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L₁.whiskerLeft β.natTrans) L₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L₁.associator H R₂).inv L₂) (CategoryTheory.CategoryStruct.comp ((L₁.comp H).associator R₂ L₂).hom (CategoryTheory.CategoryStruct.comp ((L₁.comp H).whiskerLeft adj₂.counit) (L₁.comp H).rightUnitor.hom))))))))
ModuleCat.extendScalars_id_comp 📋 Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
{R₁ R₂ : Type u₁} [CommRing R₁] [CommRing R₂] (f₁₂ : R₁ →+* R₂) : CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp (RingHom.id R₁) f₁₂).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (ModuleCat.extendScalarsId R₁).hom (ModuleCat.extendScalars f₁₂)) (ModuleCat.extendScalars f₁₂).leftUnitor.hom) = CategoryTheory.CategoryStruct.id (ModuleCat.extendScalars (f₁₂.comp (RingHom.id R₁)))
ModuleCat.extendScalars_id_comp_assoc 📋 Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
{R₁ R₂ : Type u₁} [CommRing R₁] [CommRing R₂] (f₁₂ : R₁ →+* R₂) {Z : CategoryTheory.Functor (ModuleCat R₁) (ModuleCat R₂)} (h : ModuleCat.extendScalars f₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp (RingHom.id R₁) f₁₂).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (ModuleCat.extendScalarsId R₁).hom (ModuleCat.extendScalars f₁₂)) (CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalars f₁₂).leftUnitor.hom h)) = h
CategoryTheory.Functor.isLeftKanExtensionId 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] (F₀ : CategoryTheory.Functor C H) : F₀.IsLeftKanExtension F₀.leftUnitor.inv
CategoryTheory.Functor.isRightKanExtensionId 📋 Mathlib.CategoryTheory.Functor.KanExtension.Basic
{C : Type u_1} {H : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} H] (F₀ : CategoryTheory.Functor C H) : F₀.IsRightKanExtension F₀.leftUnitor.hom
CategoryTheory.shiftFunctorAdd'_zero_add 📋 Mathlib.CategoryTheory.Shift.Basic
(C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (a : A) : CategoryTheory.shiftFunctorAdd' C 0 a a ⋯ = (CategoryTheory.shiftFunctor C a).leftUnitor.symm ≪≫ CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorZero C A).symm (CategoryTheory.shiftFunctor C a)
CategoryTheory.NatTrans.CommShift.leftUnitor 📋 Mathlib.CategoryTheory.Shift.CommShift
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F₁ : CategoryTheory.Functor C D} (A : Type u_5) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F₁.CommShift A] : CategoryTheory.NatTrans.CommShift F₁.leftUnitor.hom A
CategoryTheory.Functor.shiftIso_zero 📋 Mathlib.CategoryTheory.Shift.ShiftSequence
{C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [AddMonoid M] [CategoryTheory.HasShift C M] [F.ShiftSequence M] (a : M) : F.shiftIso 0 a a ⋯ = CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M) (F.shift a) ≪≫ (F.shift a).leftUnitor
CategoryTheory.Functor.ShiftSequence.shiftIso_zero 📋 Mathlib.CategoryTheory.Shift.ShiftSequence
{C : Type u_1} {A : Type u_3} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Category.{v_3, u_3} A} {F : CategoryTheory.Functor C A} {M : Type u_4} {inst✝² : AddMonoid M} {inst✝³ : CategoryTheory.HasShift C M} [self : F.ShiftSequence M] (a : M) : CategoryTheory.Functor.ShiftSequence.shiftIso 0 a a ⋯ = CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ (CategoryTheory.Functor.ShiftSequence.sequence F a).leftUnitor
CategoryTheory.Functor.ShiftSequence.mk 📋 Mathlib.CategoryTheory.Shift.ShiftSequence
{C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} A] {F : CategoryTheory.Functor C A} {M : Type u_4} [AddMonoid M] [CategoryTheory.HasShift C M] (sequence : M → CategoryTheory.Functor C A) (isoZero : sequence 0 ≅ F) (shiftIso : (n a a' : M) → n + a = a' → ((CategoryTheory.shiftFunctor C n).comp (sequence a) ≅ sequence a')) (shiftIso_zero : ∀ (a : M), shiftIso 0 a a ⋯ = CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M) (sequence a) ≪≫ (sequence a).leftUnitor) (shiftIso_add : ∀ (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a''), shiftIso (m + n) a a'' ⋯ = CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n) (sequence a) ≪≫ (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n) (sequence a) ≪≫ (CategoryTheory.shiftFunctor C m).isoWhiskerLeft (shiftIso n a a' ha') ≪≫ shiftIso m a' a'' ha'') : F.ShiftSequence M
PresheafOfModules.pushforward_id_comp 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R) : PresheafOfModules.pushforwardComp φ (CategoryTheory.CategoryStruct.id R) = CategoryTheory.Functor.isoWhiskerRight (PresheafOfModules.pushforwardId R) (PresheafOfModules.pushforward φ) ≪≫ (PresheafOfModules.pushforward φ).leftUnitor
CategoryTheory.Adjunction.leftAdjointCompIso_comp_id 📋 Mathlib.CategoryTheory.Adjunction.CompositionIso
{C₀ : Type u_1} {C₁ : Type u_2} [CategoryTheory.Category.{v_1, u_1} C₀] [CategoryTheory.Category.{v_2, u_2} C₁] {F₀₁ : CategoryTheory.Functor C₀ C₁} {F₁₁' : CategoryTheory.Functor C₁ C₁} {G₁₀ : CategoryTheory.Functor C₁ C₀} {G₁'₁ : CategoryTheory.Functor C₁ C₁} (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₁' : F₁₁' ⊣ G₁'₁) (e₀₁₁' : G₁'₁.comp G₁₀ ≅ G₁₀) (e₁'₁ : G₁'₁ ≅ CategoryTheory.Functor.id C₁) (h : e₀₁₁' = CategoryTheory.Functor.isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor) : adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ e₀₁₁' = F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor
CategoryTheory.Adjunction.leftAdjointCompIso_id_comp 📋 Mathlib.CategoryTheory.Adjunction.CompositionIso
{C₀ : Type u_1} {C₁ : Type u_2} [CategoryTheory.Category.{v_1, u_1} C₀] [CategoryTheory.Category.{v_2, u_2} C₁] {F₀₀' : CategoryTheory.Functor C₀ C₀} {F₀'₁ : CategoryTheory.Functor C₀ C₁} {G₀'₀ : CategoryTheory.Functor C₀ C₀} {G₁₀' : CategoryTheory.Functor C₁ C₀} (adj₀₀' : F₀₀' ⊣ G₀'₀) (adj₀'₁ : F₀'₁ ⊣ G₁₀') (e₀₀'₁ : G₁₀'.comp G₀'₀ ≅ G₁₀') (e₀'₀ : G₀'₀ ≅ CategoryTheory.Functor.id C₀) (h : e₀₀'₁ = G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor) : adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ e₀₀'₁ = CategoryTheory.Functor.isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor
PresheafOfModules.pullback_id_comp 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat} (φ : S ⟶ F.op.comp R) [(PresheafOfModules.pushforward φ).IsRightAdjoint] : PresheafOfModules.pullbackComp (CategoryTheory.CategoryStruct.id S) φ = CategoryTheory.Functor.isoWhiskerRight (PresheafOfModules.pullbackId S) (PresheafOfModules.pullback φ) ≪≫ (PresheafOfModules.pullback φ).leftUnitor
CategoryTheory.GrothendieckTopology.overMapPullback_comp_id 📋 Mathlib.CategoryTheory.Sites.Over
{C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [CategoryTheory.Category.{v', u'} A] {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (J.overMapPullbackComp A f (CategoryTheory.CategoryStruct.id Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.overMapPullbackId A Y).hom (J.overMapPullback A f)) (J.overMapPullback A f).leftUnitor.hom) = (J.overMapPullbackCongr A ⋯).hom
CategoryTheory.GrothendieckTopology.overMapPullback_comp_id_assoc 📋 Mathlib.CategoryTheory.Sites.Over
{C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [CategoryTheory.Category.{v', u'} A] {X Y : C} (f : X ⟶ Y) {Z : CategoryTheory.Functor (CategoryTheory.Sheaf (J.over Y) A) (CategoryTheory.Sheaf (J.over X) A)} (h : J.overMapPullback A f ⟶ Z) : CategoryTheory.CategoryStruct.comp (J.overMapPullbackComp A f (CategoryTheory.CategoryStruct.id Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.overMapPullbackId A Y).hom (J.overMapPullback A f)) (CategoryTheory.CategoryStruct.comp (J.overMapPullback A f).leftUnitor.hom h)) = CategoryTheory.CategoryStruct.comp (J.overMapPullbackCongr A ⋯).hom h
SheafOfModules.pushforward_id_comp 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) : SheafOfModules.pushforwardComp φ (CategoryTheory.CategoryStruct.id R) = CategoryTheory.Functor.isoWhiskerRight (SheafOfModules.pushforwardId R) (SheafOfModules.pushforward φ) ≪≫ (SheafOfModules.pushforward φ).leftUnitor
SheafOfModules.pullback_id_comp 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) [(SheafOfModules.pushforward φ).IsRightAdjoint] : SheafOfModules.pullbackComp (CategoryTheory.CategoryStruct.id S) φ = CategoryTheory.Functor.isoWhiskerRight (SheafOfModules.pullbackId S) (SheafOfModules.pullback φ) ≪≫ (SheafOfModules.pullback φ).leftUnitor
AlgebraicGeometry.Scheme.Modules.pseudofunctor_left_unitality 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.pullbackComp f (CategoryTheory.CategoryStruct.id Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (AlgebraicGeometry.Scheme.Modules.pullbackId Y).hom (AlgebraicGeometry.Scheme.Modules.pullback f)) (AlgebraicGeometry.Scheme.Modules.pullback f).leftUnitor.hom) = CategoryTheory.eqToHom ⋯
AlgebraicGeometry.Scheme.Modules.pseudofunctor_left_unitality_assoc 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : CategoryTheory.Functor Y.Modules X.Modules} (h : AlgebraicGeometry.Scheme.Modules.pullback f ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.pullbackComp f (CategoryTheory.CategoryStruct.id Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (AlgebraicGeometry.Scheme.Modules.pullbackId Y).hom (AlgebraicGeometry.Scheme.Modules.pullback f)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.pullback f).leftUnitor.hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h
CategoryTheory.Adjunction.Triple.rightToLeft_eq_counits 📋 Mathlib.CategoryTheory.Adjunction.Triple
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [G.Full] [G.Faithful] : t.rightToLeft = CategoryTheory.CategoryStruct.comp H.rightUnitor.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (H.whiskerLeft t.adj₁.counit)) (CategoryTheory.CategoryStruct.comp (H.associator G F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight t.adj₂.counit F) F.leftUnitor.hom)))
CategoryTheory.Adjunction.Triple.rightToLeft_eq_units 📋 Mathlib.CategoryTheory.Adjunction.Triple
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [G.Full] [G.Faithful] : t.rightToLeft = CategoryTheory.CategoryStruct.comp H.leftUnitor.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight t.adj₁.unit H) (CategoryTheory.CategoryStruct.comp (F.associator G H).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.whiskerLeft t.adj₂.unit)) F.rightUnitor.hom)))
CategoryTheory.Adjunction.Triple.leftToRight_eq_counits 📋 Mathlib.CategoryTheory.Adjunction.Triple
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [F.Full] [F.Faithful] [H.Full] [H.Faithful] : t.leftToRight = CategoryTheory.CategoryStruct.comp F.leftUnitor.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Functor.whiskerRight t.adj₂.counit F)) (CategoryTheory.CategoryStruct.comp (H.associator G F).hom (CategoryTheory.CategoryStruct.comp (H.whiskerLeft t.adj₁.counit) H.rightUnitor.hom)))
CategoryTheory.Iso.coreLeftUnitor 📋 Mathlib.CategoryTheory.Core
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} : F.leftUnitor.core = (CategoryTheory.Functor.id C).coreComp F ≪≫ CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Functor.coreId C) F.core ≪≫ F.core.leftUnitor
CategoryTheory.Join.mapWhiskerLeft_leftUnitor_hom 📋 Mathlib.CategoryTheory.Join.Pseudofunctor
(A : Type u_1) {B : Type u_2} {C : Type u_3} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor B C) : CategoryTheory.Join.mapWhiskerLeft (CategoryTheory.Functor.id A) F.leftUnitor.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompRight A (CategoryTheory.Functor.id B) F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight CategoryTheory.Join.mapPairId.hom (CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) F)) (CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) F).leftUnitor.hom)
CategoryTheory.Join.mapWhiskerRight_leftUnitor_hom 📋 Mathlib.CategoryTheory.Join.Pseudofunctor
{A : Type u_1} {B : Type u_2} (C : Type u_3) [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] [CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor A B) : CategoryTheory.Join.mapWhiskerRight F.leftUnitor.hom (CategoryTheory.Functor.id C) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompLeft C (CategoryTheory.Functor.id A) F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight CategoryTheory.Join.mapPairId.hom (CategoryTheory.Join.mapPair F (CategoryTheory.Functor.id C))) (CategoryTheory.Join.mapPair F (CategoryTheory.Functor.id C)).leftUnitor.hom)
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_leftUnitor 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
{A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} [CategoryTheory.Category.{v₄, u₄} X] [CategoryTheory.Category.{v₅, u₅} Y] (U : CategoryTheory.Functor X Y) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).map U.leftUnitor.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G (CategoryTheory.Functor.id X) U).hom (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).whiskerLeft (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F G X).hom) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).rightUnitor.hom)
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_rightUnitor 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
{A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅} [CategoryTheory.Category.{v₄, u₄} X] [CategoryTheory.Category.{v₅, u₅} Y] (U : CategoryTheory.Functor X Y) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).map U.rightUnitor.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp F G U (CategoryTheory.Functor.id Y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F G Y).hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).leftUnitor.hom)
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_leftUnitor 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
{A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) : (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).map ψ.leftUnitor.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X (CategoryTheory.Limits.CatCospanTransform.id F G) ψ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).leftUnitor.hom)
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
{A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {X : Type u₇} {Y : Type u₈} [CategoryTheory.Category.{v₇, u₇} X] [CategoryTheory.Category.{v₈, u₈} Y] (U : CategoryTheory.Functor X Y) (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj (CategoryTheory.Limits.CatCospanTransform.id F G)) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj (CategoryTheory.Limits.CatCospanTransform.id F G))).hom (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).whiskerLeft (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId Y F G).hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).leftUnitor.hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).rightUnitor.inv)
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
{A : Type u₁} {B : Type u₂} {C : Type u₃} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆} [CategoryTheory.Category.{v₄, u₄} A₁] [CategoryTheory.Category.{v₅, u₅} B₁] [CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁} (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (X : Type u₇) [CategoryTheory.Category.{v₇, u₇} X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj (CategoryTheory.Functor.id X)) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ) ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj (CategoryTheory.Functor.id X))).hom (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).whiskerLeft (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F₁ G₁ X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F G X).hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).leftUnitor.hom ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).rightUnitor.inv)
CategoryTheory.toOverIsoToOverUnit_hom_app_left 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.Over
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) : (CategoryTheory.toOverIsoToOverUnit.hom.app X).left = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (((CategoryTheory.mateEquiv (CategoryTheory.forgetAdjToOver (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (CategoryTheory.equivToOverUnit C).toAdjunction) (CategoryTheory.TwoSquare.mk (CategoryTheory.Functor.id (CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) (CategoryTheory.Over.forget (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (CategoryTheory.Over.forget (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (CategoryTheory.Functor.id C) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.forget (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).leftUnitor.hom (CategoryTheory.Over.forget (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).rightUnitor.inv))).natTrans.app X)) (CategoryTheory.CategoryStruct.id X)
CategoryTheory.toOverIsoToOverUnit_inv_app_left 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.Over
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) : (CategoryTheory.toOverIsoToOverUnit.inv.app X).left = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (((CategoryTheory.mateEquiv (CategoryTheory.equivToOverUnit C).toAdjunction (CategoryTheory.forgetAdjToOver (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) (CategoryTheory.TwoSquare.mk (CategoryTheory.Functor.id (CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) (CategoryTheory.Over.forget (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (CategoryTheory.Over.forget (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (CategoryTheory.Functor.id C) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.forget (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).leftUnitor.hom (CategoryTheory.Over.forget (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).rightUnitor.inv))).natTrans.app X)) (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
CategoryTheory.toOverIteratedSliceForwardIsoPullback_hom_app_left 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.Over
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenPullbacks C] {X Y : C} (f : Y ⟶ X) (X✝ : CategoryTheory.Over X) : ((CategoryTheory.toOverIteratedSliceForwardIsoPullback f).hom.app X✝).left = (CategoryTheory.CategoryStruct.comp (((((((CategoryTheory.Over.map f).leftUnitor.symm.homCongr ((CategoryTheory.Over.mk f).iteratedSliceBackward.comp (CategoryTheory.Over.forget (CategoryTheory.Over.mk f))).rightUnitor.symm).trans (CategoryTheory.TwoSquare.equivNatTrans (CategoryTheory.Functor.id (CategoryTheory.Over Y)) ((CategoryTheory.Over.mk f).iteratedSliceBackward.comp (CategoryTheory.Over.forget (CategoryTheory.Over.mk f))) (CategoryTheory.Over.map f) (CategoryTheory.Functor.id (CategoryTheory.Over X))).symm).trans (CategoryTheory.mateEquiv ((CategoryTheory.Over.mk f).iteratedSliceEquiv.symm.toAdjunction.comp (CategoryTheory.forgetAdjToOver (CategoryTheory.Over.mk f))) (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f))).trans (CategoryTheory.TwoSquare.equivNatTrans ((CategoryTheory.toOver (CategoryTheory.Over.mk f)).comp (CategoryTheory.Over.mk f).iteratedSliceForward) (CategoryTheory.Functor.id (CategoryTheory.Over X)) (CategoryTheory.Functor.id (CategoryTheory.Over Y)) (CategoryTheory.ChosenPullbacksAlong.pullback f))) (CategoryTheory.eqToIso ⋯).hom).app X✝) (CategoryTheory.CategoryStruct.id ((CategoryTheory.ChosenPullbacksAlong.pullback f).obj X✝))).left
CategoryTheory.toOverIteratedSliceForwardIsoPullback_inv_app_left 📋 Mathlib.CategoryTheory.LocallyCartesianClosed.Over
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenPullbacks C] {X Y : C} (f : Y ⟶ X) (X✝ : CategoryTheory.Over X) : ((CategoryTheory.toOverIteratedSliceForwardIsoPullback f).inv.app X✝).left = (CategoryTheory.CategoryStruct.comp ((((((((CategoryTheory.Over.mk f).iteratedSliceBackward.comp (CategoryTheory.Over.forget (CategoryTheory.Over.mk f))).leftUnitor.symm.homCongr (CategoryTheory.Over.map f).rightUnitor.symm).trans (CategoryTheory.TwoSquare.equivNatTrans (CategoryTheory.Functor.id (CategoryTheory.Over Y)) (CategoryTheory.Over.map f) ((CategoryTheory.Over.mk f).iteratedSliceBackward.comp (CategoryTheory.Over.forget (CategoryTheory.Over.mk f))) (CategoryTheory.Functor.id (CategoryTheory.Over X))).symm).trans (CategoryTheory.mateEquiv (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f) ((CategoryTheory.Over.mk f).iteratedSliceEquiv.symm.toAdjunction.comp (CategoryTheory.forgetAdjToOver (CategoryTheory.Over.mk f))))).trans (CategoryTheory.TwoSquare.equivNatTrans (CategoryTheory.ChosenPullbacksAlong.pullback f) (CategoryTheory.Functor.id (CategoryTheory.Over X)) (CategoryTheory.Functor.id (CategoryTheory.Over Y)) ((CategoryTheory.toOver (CategoryTheory.Over.mk f)).comp (CategoryTheory.Over.mk f).iteratedSliceForward))) (CategoryTheory.eqToIso ⋯).inv).app X✝) (CategoryTheory.CategoryStruct.id (CategoryTheory.Over.mk (CategoryTheory.Over.Hom.left (CategoryTheory.SemiCartesianMonoidalCategory.snd X✝ (CategoryTheory.Over.mk f)))))).left

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c