Loogle!

Result

Found 100 declarations mentioning CategoryTheory.Limits.IsInitial.to.

• CategoryTheory.Limits.IsInitial.to 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsInitial X) (Y : C) : X ⟶ Y
• CategoryTheory.Limits.InitialMonoClass.isInitial_mono_from 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} [self : CategoryTheory.Limits.InitialMonoClass C] {I : C} (X : C) (hI : CategoryTheory.Limits.IsInitial I) : CategoryTheory.Mono (hI.to X)
• CategoryTheory.Limits.InitialMonoClass.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (isInitial_mono_from : ∀ {I : C} (X : C) (hI : CategoryTheory.Limits.IsInitial I), CategoryTheory.Mono (hI.to X)) : CategoryTheory.Limits.InitialMonoClass C
• CategoryTheory.Limits.InitialMonoClass.of_isInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : C} (hI : CategoryTheory.Limits.IsInitial I) (h : ∀ (X : C), CategoryTheory.Mono (hI.to X)) : CategoryTheory.Limits.InitialMonoClass C
• CategoryTheory.Limits.InitialMonoClass.of_isTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I T : C} (hI : CategoryTheory.Limits.IsInitial I) (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Mono (hI.to T) → CategoryTheory.Limits.InitialMonoClass C
• CategoryTheory.Limits.IsInitial.to_self 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsInitial X) : t.to X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.IsInitial.uniqueUpToIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T T' : C} (hT : CategoryTheory.Limits.IsInitial T) (hT' : CategoryTheory.Limits.IsInitial T') : (hT.uniqueUpToIso hT').hom = hT.to T'
• CategoryTheory.Limits.IsInitial.uniqueUpToIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T T' : C} (hT : CategoryTheory.Limits.IsInitial T) (hT' : CategoryTheory.Limits.IsInitial T') : (hT.uniqueUpToIso hT').inv = hT'.to T
• CategoryTheory.Limits.IsInitial.to_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z : C} (t : CategoryTheory.Limits.IsInitial Z) {X Y : C} (f : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (t.to Y) f = t.to X
• CategoryTheory.Limits.coneOfDiagramInitial_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (tX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C) (j : J) : (CategoryTheory.Limits.coneOfDiagramInitial tX F).π.app j = F.map (tX.to j)
• CategoryTheory.Functor.isInitialConst_to_app 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {X : D} (hX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor C D) (Y : C) : ((CategoryTheory.Functor.isInitialConst C hX).to F).app Y = hX.to (F.obj Y)
• CategoryTheory.Limits.coconeOfDiagramInitial_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {X : J} (hX : CategoryTheory.Limits.IsInitial X) (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : j ⟶ i), CategoryTheory.IsIso (F.map f)] (x✝ : J) : (CategoryTheory.Limits.coconeOfDiagramInitial hX F).ι.app x✝ = CategoryTheory.inv (F.map (hX.to x✝))
• CategoryTheory.StructuredArrow.IsUniversal.uniq 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {f g : CategoryTheory.StructuredArrow S T} (h : f.IsUniversal) (η : f ⟶ g) : η = CategoryTheory.Limits.IsInitial.to h g
• CategoryTheory.Under.equivalenceOfIsInitial_inverse_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) (Y : T) : (CategoryTheory.Under.equivalenceOfIsInitial hX).inverse.obj Y = CategoryTheory.Under.mk (hX.to Y)
• CategoryTheory.Under.mkIdInitial_to_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (Y : CategoryTheory.Under X) : CategoryTheory.Under.Hom.right (CategoryTheory.Under.mkIdInitial.to Y) = Y.hom
• CategoryTheory.Under.equivalenceOfIsInitial_inverse_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) {X✝ Y✝ : T} (f : X✝ ⟶ Y✝) : (CategoryTheory.Under.equivalenceOfIsInitial hX).inverse.map f = CategoryTheory.Under.homMk f ⋯
• CategoryTheory.Under.equivalenceOfIsInitial_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.Under.equivalenceOfIsInitial hX).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (({ obj := fun Y => CategoryTheory.Under.mk (hX.to Y), map := fun {X_1 Y} f => CategoryTheory.Under.homMk f ⋯, map_id := ⋯, map_comp := ⋯ }.comp (CategoryTheory.Under.forget X)).obj x)) ⋯
• CategoryTheory.Under.equivalenceOfIsInitial_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) : (CategoryTheory.Under.equivalenceOfIsInitial hX).unitIso = CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.Under.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Under X)).obj Y).right) ⋯) ⋯
• CategoryTheory.Limits.initialIsoIsInitial_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] {P : C} (t : CategoryTheory.Limits.IsInitial P) : (CategoryTheory.Limits.initialIsoIsInitial t).inv = t.to (⊥_ C)
• CategoryTheory.Limits.initialIsoIsInitial_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C] {P : C} (t : CategoryTheory.Limits.IsInitial P) : (CategoryTheory.Limits.initialIsoIsInitial t).hom = CategoryTheory.Limits.initialIsInitial.to P
• CategoryTheory.Limits.isInitialMul_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (X : C) [CategoryTheory.Limits.HasBinaryProduct I X] (hI : CategoryTheory.Limits.IsInitial I) : (CategoryTheory.Limits.isInitialMul X hI).inv = hI.to (I ⨯ X)
• CategoryTheory.Limits.mulIsInitial_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictInitialObjects C] {I : C} (X : C) [CategoryTheory.Limits.HasBinaryProduct X I] (hI : CategoryTheory.Limits.IsInitial I) : (CategoryTheory.Limits.mulIsInitial X hI).inv = hI.to (X ⨯ I)
• CategoryTheory.IsPushout.of_is_coproduct' 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {inl : X ⟶ P} {inr : Y ⟶ P} (h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk inl inr)) (t : CategoryTheory.Limits.IsInitial Z) : CategoryTheory.IsPushout (t.to X) (t.to Y) inl inr
• CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) {I : C} (hI : CategoryTheory.Limits.IsInitial I) : CategoryTheory.IsPushout (hI.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) (hI.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) c.inr c.inl
• CategoryTheory.IsPushout.of_is_coproduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit c) (t : CategoryTheory.Limits.IsInitial Z) : CategoryTheory.IsPushout (t.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (t.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) c.inl c.inr
• CategoryTheory.Under.forgetMapInitial 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {I : C} (hI : CategoryTheory.Limits.IsInitial I) : CategoryTheory.Under.forget X ≅ (CategoryTheory.Under.map (hI.to X)).comp (CategoryTheory.Under.equivalenceOfIsInitial hI).functor
• CategoryTheory.Under.forgetMapInitial_hom_app 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {I : C} (hI : CategoryTheory.Limits.IsInitial I) (X✝ : CategoryTheory.Under X) : (CategoryTheory.Under.forgetMapInitial X hI).hom.app X✝ = CategoryTheory.CategoryStruct.id X✝.right
• CategoryTheory.Under.forgetMapInitial_inv_app 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {I : C} (hI : CategoryTheory.Limits.IsInitial I) (X✝ : CategoryTheory.Under X) : (CategoryTheory.Under.forgetMapInitial X hI).inv.app X✝ = CategoryTheory.CategoryStruct.id X✝.right
• CategoryTheory.Limits.IsColimit.descCoconeMorphism_eq_isInitial_to 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cocone F) : hc.descCoconeMorphism s = (c.isColimitEquivIsInitial hc).to s
• CategoryTheory.Limits.IsInitial.to_eq_descCoconeMorphism 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsInitial c) (s : CategoryTheory.Limits.Cocone F) : hc.to s = (c.isColimitEquivIsInitial.symm hc).descCoconeMorphism s
• CategoryTheory.WithInitial.starIsoInitial_hom 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.WithInitial.starIsoInitial.hom = CategoryTheory.WithInitial.starInitial.to (⊥_ CategoryTheory.WithInitial C)
• CategoryTheory.WithInitial.starIsoInitial_inv 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.WithInitial.starIsoInitial.inv = CategoryTheory.Limits.initialIsInitial.to CategoryTheory.WithInitial.star
• CategoryTheory.WithInitial.inclLiftToInitial_inv_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (x✝ : C) : (CategoryTheory.WithInitial.inclLiftToInitial F hZ).inv.app x✝ = CategoryTheory.CategoryStruct.id (F.obj x✝)
• CategoryTheory.WithInitial.mkCommaObject_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (x : C) : (CategoryTheory.WithInitial.mkCommaObject F).hom.app x = F.map (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of x))
• CategoryTheory.WithInitial.inclLiftToInitial_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (x✝ : C) : (CategoryTheory.WithInitial.inclLiftToInitial F hZ).hom.app x✝ = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithInitial.incl.obj x✝ with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z)
• CategoryTheory.WithInitial.liftToInitial_map 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) {X Y : CategoryTheory.WithInitial C} (f : X ⟶ Y) : (CategoryTheory.WithInitial.liftToInitial F hZ).map f = match X, Y, f with | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => F.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => hZ.to (F.obj a) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id Z
• CategoryTheory.WithInitial.liftToInitialUnique_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.WithInitial.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.liftToInitialUnique F hZ G h hG).hom.app X = (match X with | CategoryTheory.WithInitial.of x => h.app x | CategoryTheory.WithInitial.star => hG).hom
• CategoryTheory.WithInitial.liftToInitialUnique_inv_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.WithInitial.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.liftToInitialUnique F hZ G h hG).inv.app X = (match X with | CategoryTheory.WithInitial.of x => h.app x | CategoryTheory.WithInitial.star => hG).inv
• CategoryTheory.WithInitial.liftStar_lift_map 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) (x : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.WithInitial.liftStar F M hM).hom ((CategoryTheory.WithInitial.lift F M hM).map (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.incl.obj x))) = CategoryTheory.CategoryStruct.comp (M x) ((CategoryTheory.WithInitial.inclLift F M hM).hom.app x)
• CategoryTheory.WithInitial.opEquiv_inverse_map 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] {x y : CategoryTheory.WithTerminal Cᵒᵖ} (f : x ⟶ y) : (CategoryTheory.WithInitial.opEquiv C).inverse.map f = match x, y, f with | CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f => CategoryTheory.WithInitial.down f | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x => Opposite.op (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of unop)) | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id (Opposite.op CategoryTheory.WithInitial.star)
• CategoryTheory.WithInitial.equivComma_functor_obj_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (x : C) : (CategoryTheory.WithInitial.equivComma.functor.obj F).hom.app x = F.map (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of x))
• CategoryTheory.WithInitial.liftUnique 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.WithInitial.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) (hh : ∀ (x : C), CategoryTheory.CategoryStruct.comp hG.symm.hom (G.map (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.incl.obj x))) = CategoryTheory.CategoryStruct.comp (M x) (h.symm.hom.app x)) : G ≅ CategoryTheory.WithInitial.lift F M hM
• CategoryTheory.WithTerminal.opEquiv_functor_map 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] {x y : (CategoryTheory.WithTerminal C)ᵒᵖ} (x✝ : x ⟶ y) : (CategoryTheory.WithTerminal.opEquiv C).functor.map x✝ = match x✝ with | Opposite.op f => match x, y, f, x✝ with | Opposite.op (CategoryTheory.WithTerminal.of x), Opposite.op (CategoryTheory.WithTerminal.of y), f, x_1 => (CategoryTheory.WithTerminal.down f).op | Opposite.op CategoryTheory.WithTerminal.star, Opposite.op (CategoryTheory.WithTerminal.of a), x, x_1 => CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of (Opposite.op a)) | Opposite.op CategoryTheory.WithTerminal.star, Opposite.op CategoryTheory.WithTerminal.star, x, x_1 => CategoryTheory.CategoryStruct.id CategoryTheory.WithInitial.star
• CategoryTheory.WithInitial.equivComma_unitIso_hom_app_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (X : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (X✝ : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.equivComma.unitIso.hom.app X).app X✝ = (match X✝ with | CategoryTheory.WithInitial.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithInitial.incl.comp X)).app x | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithInitial.star)).hom
• CategoryTheory.WithInitial.equivComma_unitIso_inv_app_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (X : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (X✝ : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.equivComma.unitIso.inv.app X).app X✝ = (match X✝ with | CategoryTheory.WithInitial.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithInitial.incl.comp X)).app x | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithInitial.star)).inv
• CategoryTheory.WithInitial.opEquiv_counitIso_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.WithTerminal Cᵒᵖ) : (CategoryTheory.WithInitial.opEquiv C).counitIso.hom.app X = (match X with | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of x) | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).hom
• CategoryTheory.WithInitial.opEquiv_counitIso_inv_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.WithTerminal Cᵒᵖ) : (CategoryTheory.WithInitial.opEquiv C).counitIso.inv.app X = (match X with | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of x) | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).inv
• CategoryTheory.WithTerminal.opEquiv_counitIso_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.WithInitial Cᵒᵖ) : (CategoryTheory.WithTerminal.opEquiv C).counitIso.hom.app X = (match X with | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of x) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).hom
• CategoryTheory.WithTerminal.opEquiv_counitIso_inv_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.WithInitial Cᵒᵖ) : (CategoryTheory.WithTerminal.opEquiv C).counitIso.inv.app X = (match X with | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of x) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).inv
• CategoryTheory.WithInitial.opEquiv_unitIso_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.WithInitial C)ᵒᵖ) : (CategoryTheory.WithInitial.opEquiv C).unitIso.hom.app X = (match Opposite.unop X with | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithInitial.of x)) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithInitial.star)).hom
• CategoryTheory.WithInitial.opEquiv_unitIso_inv_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.WithInitial C)ᵒᵖ) : (CategoryTheory.WithInitial.opEquiv C).unitIso.inv.app X = (match Opposite.unop X with | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithInitial.of x)) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithInitial.star)).inv
• CategoryTheory.WithTerminal.opEquiv_unitIso_hom_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.WithTerminal C)ᵒᵖ) : (CategoryTheory.WithTerminal.opEquiv C).unitIso.hom.app X = (match Opposite.unop X with | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithTerminal.of x)) | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithTerminal.star)).hom
• CategoryTheory.WithTerminal.opEquiv_unitIso_inv_app 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.WithTerminal C)ᵒᵖ) : (CategoryTheory.WithTerminal.opEquiv C).unitIso.inv.app X = (match Opposite.unop X with | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithTerminal.of x)) | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithTerminal.star)).inv
• CategoryTheory.initial_mono 📋 Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {I : C} (B : C) (t : CategoryTheory.Limits.IsInitial I) [CategoryTheory.MonoidalClosed C] : CategoryTheory.Mono (t.to B)
• CategoryTheory.zeroMul_inv 📋 Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} [CategoryTheory.Closed A] {I : C} (t : CategoryTheory.Limits.IsInitial I) : (CategoryTheory.zeroMul t).inv = t.to (CategoryTheory.MonoidalCategoryStruct.tensorObj A I)
• TopCat.IsInducing.empty 📋 Mathlib.Topology.Category.TopCat.Limits.Basic
  (X : TopCat) : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.isInitialPEmpty.to X))
• CategoryTheory.Limits.CoproductDisjoint.isPullback_of_isInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CategoryTheory.Limits.CoproductDisjoint X] {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) {Y : C} (hY : CategoryTheory.Limits.IsInitial Y) {i j : ι} [CategoryTheory.Limits.HasPullback (c.inj i) (c.inj j)] (hij : i ≠ j) : CategoryTheory.IsPullback (hY.to (X i)) (hY.to (X j)) (c.inj i) (c.inj j)
• CategoryTheory.CosimplicialObject.augmentOfIsInitial_hom_app 📋 Mathlib.AlgebraicTopology.SimplicialObject.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {T : C} (hT : CategoryTheory.Limits.IsInitial T) (x✝ : SimplexCategory) : (X.augmentOfIsInitial hT).hom.app x✝ = hT.to (X.obj x✝)
• AlgebraicGeometry.emptyIsInitial_to 📋 Mathlib.AlgebraicGeometry.Limits
  : AlgebraicGeometry.emptyIsInitial.to = AlgebraicGeometry.Scheme.emptyTo
• TopPair.inclAdjProj₁_counit_app 📋 Mathlib.Topology.Category.TopPair
  (X : TopPair) : TopPair.inclAdjProj₁.counit.app X = TopPair.ofHom (CategoryTheory.CategoryStruct.id TopPair.fst) (TopCat.isInitialPEmpty.to TopPair.snd) ⋯
• AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_hom_app 📋 Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C) (x : SimplexCategory) : (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.functor.obj F).hom.app x = F.map (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of x))
• AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_left_map 📋 Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C) {X✝ Y✝ : SimplexCategoryᵒᵖ} (f : X✝ ⟶ Y✝) : (AugmentedSimplexCategory.equivAugmentedSimplicialObject.functor.obj X).left.map f = X.map (match CategoryTheory.WithTerminal.incl.obj X✝, CategoryTheory.WithTerminal.incl.obj Y✝, CategoryTheory.WithTerminal.incl.map f with | CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f => CategoryTheory.WithInitial.down f | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x => Opposite.op (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of unop)) | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id (Opposite.op CategoryTheory.WithInitial.star))
• AugmentedSimplexCategory.equivAugmentedSimplicialObject_functor_obj_hom_app 📋 Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C) (x : SimplexCategoryᵒᵖ) : (AugmentedSimplexCategory.equivAugmentedSimplicialObject.functor.obj X).hom.app x = X.map (match CategoryTheory.WithTerminal.incl.obj x, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.of x) with | CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f => CategoryTheory.WithInitial.down f | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x => Opposite.op (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of unop)) | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id (Opposite.op CategoryTheory.WithInitial.star))
• AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app 📋 Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C) (X✝ : CategoryTheory.WithInitial SimplexCategory) : (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.unitIso.hom.app X).app X✝ = (match X✝ with | CategoryTheory.WithInitial.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithInitial.incl.comp X)).app x | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithInitial.star)).hom
• AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app 📋 Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C) (X✝ : CategoryTheory.WithInitial SimplexCategory) : (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.unitIso.inv.app X).app X✝ = (match X✝ with | CategoryTheory.WithInitial.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithInitial.incl.comp X)).app x | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithInitial.star)).inv
• CategoryTheory.Functor.PushoutObjObj.ofIsInitialRight_inl 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
  {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₃, u₃} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.obj X₁)] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.obj Y₁)] (h : CategoryTheory.Limits.IsInitial X₂) : (CategoryTheory.Functor.PushoutObjObj.ofIsInitialRight F f₁ f₂ h).inl = (CategoryTheory.Limits.IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂)
• CategoryTheory.Functor.PushoutObjObj.ofIsInitialLeft_inr 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
  {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₃, u₃} C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.flip.obj X₂)] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.flip.obj Y₂)] (h : CategoryTheory.Limits.IsInitial X₁) : (CategoryTheory.Functor.PushoutObjObj.ofIsInitialLeft F f₁ f₂ h).inr = (CategoryTheory.Limits.IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h).to ((F.obj Y₁).obj X₂)
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C} (t : CategoryTheory.Limits.IsTerminal T) : (X □ CategoryTheory.Arrow.mk (i.to T)) ≅ X
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C} : (X □ CategoryTheory.Arrow.mk (i.to W)) ≅ CategoryTheory.Arrow.mk (CategoryTheory.MonoidalCategoryStruct.whiskerRight X.hom W)
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso' 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C} : (CategoryTheory.Arrow.mk (i.to W) □ X) ≅ CategoryTheory.Arrow.mk (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W X.hom)
• CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C} : (Opposite.op (CategoryTheory.Arrow.mk (i.to W)) ⋔ X) ≅ CategoryTheory.Arrow.mk ((CategoryTheory.ihom W).map X.hom)
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso_inv_right 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C} (t : CategoryTheory.Limits.IsTerminal T) : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso X i t).inv.right = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.right).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.right (t.from (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso_hom_right 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C} (t : CategoryTheory.Limits.IsTerminal T) : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso X i t).hom.right = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.right (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from T)) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.right).hom
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso_hom_right 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso X i).hom.right = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.right W)
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso_inv_right 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso X i).inv.right = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.right W)
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso_hom_left 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C} (t : CategoryTheory.Limits.IsTerminal T) : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso X i t).hom.left = CategoryTheory.CategoryStruct.comp ⋯.isoPushout.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from T)) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.left).hom)
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso'_hom_right 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso' X i).hom.right = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj W X.right)
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso'_inv_right 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso' X i).inv.right = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj W X.right)
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso_inv_left 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C} (t : CategoryTheory.Limits.IsTerminal T) : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso X i t).inv.left = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.left).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left (t.from (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) ⋯.isoPushout.hom)
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso_hom_left 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso X i).hom.left = ⋯.isoPushout.inv
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso_inv_left 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso X i).inv.left = ⋯.isoPushout.hom
• CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso_hom_left 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso X i).hom.left = CategoryTheory.CategoryStruct.id (W ⟹ X.left)
• CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso_inv_left 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso X i).inv.left = CategoryTheory.CategoryStruct.id (W ⟹ X.left)
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso'_hom_left 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso' X i).hom.left = ⋯.isoPushout.inv
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso'_inv_left 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso' X i).inv.left = ⋯.isoPushout.hom
• CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso_hom_right 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso X i).hom.right = ⋯.isoPullback.inv
• CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso_inv_right 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso X i).inv.right = ⋯.isoPullback.hom
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso'_hom_left 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C} (t : CategoryTheory.Limits.IsTerminal T) : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso' X i t).hom.left = CategoryTheory.CategoryStruct.comp (⋯.desc (CategoryTheory.Limits.pushout.inl (CategoryTheory.MonoidalCategoryStruct.whiskerRight X.hom I) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left (i.to T))) (CategoryTheory.Limits.pushout.inr (CategoryTheory.MonoidalCategoryStruct.whiskerRight X.hom I) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left (i.to T))) ⋯) (CategoryTheory.CategoryStruct.comp ⋯.isoPushout.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from T)) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.left).hom))
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso'_inv_left 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C} (t : CategoryTheory.Limits.IsTerminal T) : (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso' X i t).inv.left = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.left).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left (t.from (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) (CategoryTheory.CategoryStruct.comp ⋯.isoPushout.hom (⋯.desc (CategoryTheory.Limits.pushout.inl (CategoryTheory.MonoidalCategoryStruct.whiskerRight X.hom I) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left (t.from I))) (CategoryTheory.Limits.pushout.inr (CategoryTheory.MonoidalCategoryStruct.whiskerRight X.hom I) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left (t.from I))) ⋯)))
• SSet.RelativeMorphism.botEquiv 📋 Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
  {X Y : SSet} : SSet.RelativeMorphism ⊥ ⊥ (SSet.Subcomplex.isInitialBot.to ⊥.toSSet) ≃ (X ⟶ Y)
• SSet.RelativeMorphism.botEquiv_symm_apply_map 📋 Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
  {X Y : SSet} (f : X ⟶ Y) : (SSet.RelativeMorphism.botEquiv.symm f).map = f
• SSet.RelativeMorphism.botEquiv_apply 📋 Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
  {X Y : SSet} (f : SSet.RelativeMorphism ⊥ ⊥ (SSet.Subcomplex.isInitialBot.to ⊥.toSSet)) : SSet.RelativeMorphism.botEquiv f = f.map
• SSet.Homotopy.h₀ 📋 Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
  {X Y : SSet} {f g : X ⟶ Y} (H : SSet.Homotopy f g) : CategoryTheory.CategoryStruct.comp SSet.ι₀ H.h = f
• SSet.Homotopy.h₁ 📋 Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
  {X Y : SSet} {f g : X ⟶ Y} (H : SSet.Homotopy f g) : CategoryTheory.CategoryStruct.comp SSet.ι₁ H.h = g
• SSet.Homotopy.h₀_assoc 📋 Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
  {X Y : SSet} {f g : X ⟶ Y} (H : SSet.Homotopy f g) {Z : SSet} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp SSet.ι₀ (CategoryTheory.CategoryStruct.comp H.h h) = CategoryTheory.CategoryStruct.comp f h
• SSet.Homotopy.h₁_assoc 📋 Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
  {X Y : SSet} {f g : X ⟶ Y} (H : SSet.Homotopy f g) {Z : SSet} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp SSet.ι₁ (CategoryTheory.CategoryStruct.comp H.h h) = CategoryTheory.CategoryStruct.comp g h
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_isTerminal_iff 📋 Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] {A B K L X Y : C} {g : K ⟶ L} (i : CategoryTheory.Limits.IsInitial A) (t : CategoryTheory.Limits.IsTerminal Y) : CategoryTheory.HasLiftingProperty (CategoryTheory.Arrow.mk (i.to B) □ CategoryTheory.Arrow.mk g).hom (t.from X) ↔ CategoryTheory.HasLiftingProperty g (t.from (B ⟹ X))
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_isTerminal_iff' 📋 Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] {A B K L X Y : C} {f : A ⟶ B} (i : CategoryTheory.Limits.IsInitial K) (t : CategoryTheory.Limits.IsTerminal Y) : CategoryTheory.HasLiftingProperty (CategoryTheory.Arrow.mk f □ CategoryTheory.Arrow.mk (i.to L)).hom (t.from X) ↔ CategoryTheory.HasLiftingProperty f (t.from (L ⟹ X))
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff 📋 Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] {A B K L X Y : C} {g : K ⟶ L} {h : X ⟶ Y} (i : CategoryTheory.Limits.IsInitial A) : CategoryTheory.HasLiftingProperty (CategoryTheory.Arrow.mk (i.to B) □ CategoryTheory.Arrow.mk g).hom h ↔ CategoryTheory.HasLiftingProperty g ((CategoryTheory.ihom B).map h)
• CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isInitial_iff' 📋 Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.MonoidalClosed C] [CategoryTheory.BraidedCategory C] {A B K L X Y : C} {f : A ⟶ B} {h : X ⟶ Y} (i : CategoryTheory.Limits.IsInitial K) : CategoryTheory.HasLiftingProperty (CategoryTheory.Arrow.mk f □ CategoryTheory.Arrow.mk (i.to L)).hom h ↔ CategoryTheory.HasLiftingProperty f ((CategoryTheory.ihom L).map h)

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:

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.

5. 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 69fae59