Loogle!

Result

Found 123 declarations mentioning CategoryTheory.Limits.IsTerminal.from.

CategoryTheory.Limits.IsTerminal.from 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsTerminal X) (Y : C) : Y ⟶ X
CategoryTheory.Limits.IsTerminal.from_self 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (t : CategoryTheory.Limits.IsTerminal X) : t.from X = CategoryTheory.CategoryStruct.id X
CategoryTheory.Limits.IsTerminal.uniqueUpToIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T T' : C} (hT : CategoryTheory.Limits.IsTerminal T) (hT' : CategoryTheory.Limits.IsTerminal T') : (hT.uniqueUpToIso hT').hom = hT'.from T
CategoryTheory.Limits.IsTerminal.uniqueUpToIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T T' : C} (hT : CategoryTheory.Limits.IsTerminal T) (hT' : CategoryTheory.Limits.IsTerminal T') : (hT.uniqueUpToIso hT').inv = hT.from T'
CategoryTheory.Limits.IsTerminal.comp_from 📋 Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z : C} (t : CategoryTheory.Limits.IsTerminal Z) {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f (t.from Y) = t.from X
CategoryTheory.Limits.coconeOfDiagramTerminal_ι_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.IsTerminal X) (F : CategoryTheory.Functor J C) (j : J) : (CategoryTheory.Limits.coconeOfDiagramTerminal tX F).ι.app j = F.map (tX.from j)
CategoryTheory.Functor.isTerminalConst_from_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.IsTerminal X) (F : CategoryTheory.Functor C D) (Y : C) : ((CategoryTheory.Functor.isTerminalConst C hX).from F).app Y = hX.from (F.obj Y)
CategoryTheory.Limits.coneOfDiagramTerminal_π_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.IsTerminal X) (F : CategoryTheory.Functor J C) [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] (x✝ : J) : (CategoryTheory.Limits.coneOfDiagramTerminal hX F).π.app x✝ = CategoryTheory.inv (F.map (hX.from x✝))
CategoryTheory.CostructuredArrow.IsUniversal.uniq 📋 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} {f g : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal) (η : g ⟶ f) : η = CategoryTheory.Limits.IsTerminal.from h g
CategoryTheory.Over.equivalenceOfIsTerminal_inverse_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X) (Y : T) : (CategoryTheory.Over.equivalenceOfIsTerminal hX).inverse.obj Y = CategoryTheory.Over.mk (hX.from Y)
CategoryTheory.Over.mkIdTerminal_from_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (Y : CategoryTheory.Over X) : CategoryTheory.Over.Hom.left (CategoryTheory.Over.mkIdTerminal.from Y) = Y.hom
CategoryTheory.Over.equivalenceOfIsTerminal_inverse_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X) {X✝ Y✝ : T} (f : X✝ ⟶ Y✝) : (CategoryTheory.Over.equivalenceOfIsTerminal hX).inverse.map f = CategoryTheory.Over.homMk f ⋯
CategoryTheory.Over.equivalenceOfIsTerminal_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.Over.equivalenceOfIsTerminal hX).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (({ obj := fun Y => CategoryTheory.Over.mk (hX.from Y), map := fun {X_1 Y} f => CategoryTheory.Over.homMk f ⋯, map_id := ⋯, map_comp := ⋯ }.comp (CategoryTheory.Over.forget X)).obj x)) ⋯
CategoryTheory.Over.equivalenceOfIsTerminal_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.Over.equivalenceOfIsTerminal hX).unitIso = CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Over X)).obj Y).left) ⋯) ⋯
CategoryTheory.Limits.terminalIsoIsTerminal_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P : C} (t : CategoryTheory.Limits.IsTerminal P) : (CategoryTheory.Limits.terminalIsoIsTerminal t).hom = t.from (⊤_ C)
CategoryTheory.Limits.terminalIsoIsTerminal_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Terminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasTerminal C] {P : C} (t : CategoryTheory.Limits.IsTerminal P) : (CategoryTheory.Limits.terminalIsoIsTerminal t).inv = CategoryTheory.Limits.terminalIsTerminal.from P
CategoryTheory.instEpiFromTerminalIsTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (A : C) [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Epi (CategoryTheory.Limits.terminalIsTerminal.from A)
CategoryTheory.IsPullback.of_is_product' 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} (h : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk fst snd)) (t : CategoryTheory.Limits.IsTerminal Z) : CategoryTheory.IsPullback fst snd (t.from X) (t.from Y)
CategoryTheory.IsPullback.of_isLimit_binaryFan_of_isTerminal 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {c : CategoryTheory.Limits.BinaryFan X Y} (hc : CategoryTheory.Limits.IsLimit c) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.IsPullback c.fst c.snd (hT.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (hT.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
CategoryTheory.IsPullback.of_is_product 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {c : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit c) (t : CategoryTheory.Limits.IsTerminal Z) : CategoryTheory.IsPullback c.fst c.snd (t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
CategoryTheory.Over.forgetMapTerminal 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Over.forget X ≅ (CategoryTheory.Over.map (hT.from X)).comp (CategoryTheory.Over.equivalenceOfIsTerminal hT).functor
CategoryTheory.Over.forgetMapTerminal_hom_app 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (X✝ : CategoryTheory.Over X) : (CategoryTheory.Over.forgetMapTerminal X hT).hom.app X✝ = CategoryTheory.CategoryStruct.id X✝.left
CategoryTheory.Over.forgetMapTerminal_inv_app 📋 Mathlib.CategoryTheory.Comma.Over.Pullback
{C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (X✝ : CategoryTheory.Over X) : (CategoryTheory.Over.forgetMapTerminal X hT).inv.app X✝ = CategoryTheory.CategoryStruct.id X✝.left
CategoryTheory.Limits.IsLimit.liftConeMorphism_eq_isTerminal_from 📋 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.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone F) : hc.liftConeMorphism s = (c.isLimitEquivIsTerminal hc).from s
CategoryTheory.Limits.IsTerminal.from_eq_liftConeMorphism 📋 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.Cone F} (hc : CategoryTheory.Limits.IsTerminal c) (s : CategoryTheory.Limits.Cone F) : hc.from s = (c.isLimitEquivIsTerminal.symm hc).liftConeMorphism s
CategoryTheory.WithTerminal.starIsoTerminal_inv 📋 Mathlib.CategoryTheory.WithTerminal.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.WithTerminal.starIsoTerminal.inv = CategoryTheory.WithTerminal.starTerminal.from (⊤_ CategoryTheory.WithTerminal C)
CategoryTheory.WithTerminal.starIsoTerminal_hom 📋 Mathlib.CategoryTheory.WithTerminal.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.WithTerminal.starIsoTerminal.hom = CategoryTheory.Limits.terminalIsTerminal.from CategoryTheory.WithTerminal.star
CategoryTheory.WithTerminal.inclLiftToTerminal_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.IsTerminal Z) (x✝ : C) : (CategoryTheory.WithTerminal.inclLiftToTerminal F hZ).inv.app x✝ = CategoryTheory.CategoryStruct.id (F.obj x✝)
CategoryTheory.WithTerminal.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.WithTerminal C) D) (x : C) : (CategoryTheory.WithTerminal.mkCommaObject F).hom.app x = F.map (CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.of x))
CategoryTheory.WithTerminal.inclLiftToTerminal_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.IsTerminal Z) (x✝ : C) : (CategoryTheory.WithTerminal.inclLiftToTerminal F hZ).hom.app x✝ = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithTerminal.incl.obj x✝ with | CategoryTheory.WithTerminal.of x => F.obj x | CategoryTheory.WithTerminal.star => Z)
CategoryTheory.WithTerminal.liftToTerminal_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.IsTerminal Z) {X Y : CategoryTheory.WithTerminal C} (f : X ⟶ Y) : (CategoryTheory.WithTerminal.liftToTerminal F hZ).map f = match X, Y, f with | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => F.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => hZ.from (F.obj x) | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id Z
CategoryTheory.WithTerminal.liftToTerminalUnique_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.IsTerminal Z) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.WithTerminal.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) (X : CategoryTheory.WithTerminal C) : (CategoryTheory.WithTerminal.liftToTerminalUnique F hZ G h hG).hom.app X = (match X with | CategoryTheory.WithTerminal.of x => h.app x | CategoryTheory.WithTerminal.star => hG).hom
CategoryTheory.WithTerminal.liftToTerminalUnique_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.IsTerminal Z) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.WithTerminal.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) (X : CategoryTheory.WithTerminal C) : (CategoryTheory.WithTerminal.liftToTerminalUnique F hZ G h hG).inv.app X = (match X with | CategoryTheory.WithTerminal.of x => h.app x | CategoryTheory.WithTerminal.star => hG).inv
CategoryTheory.WithTerminal.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) → F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.WithTerminal.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) (hh : ∀ (x : C), CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.incl.obj x))) hG.hom = CategoryTheory.CategoryStruct.comp (h.hom.app x) (M x)) : G ≅ CategoryTheory.WithTerminal.lift F M hM
CategoryTheory.WithTerminal.lift_map_liftStar 📋 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) → F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) (x : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.WithTerminal.lift F M hM).map (CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.incl.obj x))) (CategoryTheory.WithTerminal.liftStar F M hM).hom = CategoryTheory.CategoryStruct.comp ((CategoryTheory.WithTerminal.inclLift F M hM).hom.app x) (M x)
CategoryTheory.WithTerminal.opEquiv_inverse_map 📋 Mathlib.CategoryTheory.WithTerminal.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] {x y : CategoryTheory.WithInitial Cᵒᵖ} (f : x ⟶ y) : (CategoryTheory.WithTerminal.opEquiv C).inverse.map f = match x, y, f with | CategoryTheory.WithInitial.of (Opposite.op x), CategoryTheory.WithInitial.of (Opposite.op y), f => CategoryTheory.WithInitial.down f | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of (Opposite.op unop), x => Opposite.op (CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.of unop)) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id (Opposite.op CategoryTheory.WithTerminal.star)
CategoryTheory.WithTerminal.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.WithTerminal C) D) (x : C) : (CategoryTheory.WithTerminal.equivComma.functor.obj F).hom.app x = F.map (CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.of x))
CategoryTheory.WithInitial.opEquiv_functor_map 📋 Mathlib.CategoryTheory.WithTerminal.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] {x y : (CategoryTheory.WithInitial C)ᵒᵖ} (x✝ : x ⟶ y) : (CategoryTheory.WithInitial.opEquiv C).functor.map x✝ = match x✝ with | Opposite.op f => match x, y, f, x✝ with | Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_1 => (CategoryTheory.WithTerminal.down f).op | Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_1 => CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.of (Opposite.op a)) | Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_1 => CategoryTheory.CategoryStruct.id CategoryTheory.WithTerminal.star
CategoryTheory.WithTerminal.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.WithTerminal C) D) (X✝ : CategoryTheory.WithTerminal C) : (CategoryTheory.WithTerminal.equivComma.unitIso.hom.app X).app X✝ = (match X✝ with | CategoryTheory.WithTerminal.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.incl.comp X)).app x | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithTerminal.star)).hom
CategoryTheory.WithTerminal.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.WithTerminal C) D) (X✝ : CategoryTheory.WithTerminal C) : (CategoryTheory.WithTerminal.equivComma.unitIso.inv.app X).app X✝ = (match X✝ with | CategoryTheory.WithTerminal.of x => (CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.incl.comp X)).app x | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl (X.obj CategoryTheory.WithTerminal.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.Limits.Types.isTerminalPUnit_from_apply 📋 Mathlib.CategoryTheory.Limits.Types.Products
{X : Type u} (x : X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.isTerminalPUnit.from X)) x = PUnit.unit
CategoryTheory.SemiCartesianMonoidalCategory.fst_def 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.SemiCartesianMonoidalCategory C] (X Y : C) : CategoryTheory.SemiCartesianMonoidalCategory.fst X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from Y)) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
CategoryTheory.SemiCartesianMonoidalCategory.snd_def 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.SemiCartesianMonoidalCategory C] (X Y : C) : CategoryTheory.SemiCartesianMonoidalCategory.snd X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from X) Y) (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom
CategoryTheory.SemiCartesianMonoidalCategory.mk 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [toMonoidalCategory : CategoryTheory.MonoidalCategory C] (isTerminalTensorUnit : CategoryTheory.Limits.IsTerminal (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (fst : (X Y : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ X) (snd : (X Y : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Y) (fst_def : ∀ (X Y : C), fst X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (isTerminalTensorUnit.from Y)) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom := by cat_disch) (snd_def : ∀ (X Y : C), snd X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (isTerminalTensorUnit.from X) Y) (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom := by cat_disch) : CategoryTheory.SemiCartesianMonoidalCategory C
CategoryTheory.Sheaf.isTerminalTerminal_from_hom 📋 Mathlib.CategoryTheory.Sites.Sheaf
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {X : A} (hX : CategoryTheory.Limits.IsTerminal X) (G : CategoryTheory.Sheaf J A) : ((CategoryTheory.Sheaf.isTerminalTerminal J hX).from G).hom = (CategoryTheory.Functor.isTerminalConst Cᵒᵖ hX).from G.obj
CategoryTheory.SimplicialObject.augmentOfIsTerminal_hom_app 📋 Mathlib.AlgebraicTopology.SimplicialObject.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (x✝ : SimplexCategoryᵒᵖ) : (X.augmentOfIsTerminal hT).hom.app x✝ = hT.from (X.obj x✝)
AlgebraicGeometry.Scheme.emptyTo_c_app 📋 Mathlib.AlgebraicGeometry.Limits
(X : AlgebraicGeometry.Scheme) (x✝ : (TopologicalSpace.Opens ↥X)ᵒᵖ) : X.emptyTo.c.app x✝ = CommRingCat.punitIsTerminal.from (X.presheaf.obj x✝)
CategoryTheory.constantPresheafAdj_counit_app_app 📋 Mathlib.CategoryTheory.Sites.ConstantSheaf
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2) [CategoryTheory.Category.{v_2, u_2} D] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (F : CategoryTheory.Functor Cᵒᵖ D) (x✝ : Cᵒᵖ) : ((CategoryTheory.constantPresheafAdj D hT).counit.app F).app x✝ = F.map (hT.from (Opposite.unop x✝)).op
CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
{C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} (G : CategoryTheory.ComposableArrows C n) (j : Fin (n + 1)) : (CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows G).incl.app j = G.map ((Fin.isTerminalLast n).from j)
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app 📋 Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
{C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {n : ℕ} (F : CategoryTheory.ComposableArrows C n) (hF : ∀ (i : Fin n), W (F.map (CategoryTheory.homOfLE ⋯))) (j : Fin (n + 1)) : (CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows W F hF).incl.app j = F.map ((Fin.isTerminalLast n).from j)
SSet.quasicategory_of_hasLiftingProperty 📋 Mathlib.AlgebraicTopology.Quasicategory.Basic
(S : SSet) {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) (h : ∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → CategoryTheory.HasLiftingProperty (SSet.horn n i).ι (t.from S)) : S.Quasicategory
SSet.Quasicategory.hasLiftingProperty 📋 Mathlib.AlgebraicTopology.Quasicategory.Basic
(S : SSet) [S.Quasicategory] {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) {n : ℕ} {i : Fin (n + 1)} (h0 : 0 < i) (hn : i < Fin.last n) : CategoryTheory.HasLiftingProperty (SSet.horn n i).ι (t.from S)
SSet.quasicategory_iff_hasLiftingProperty 📋 Mathlib.AlgebraicTopology.Quasicategory.Basic
(S : SSet) {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) : S.Quasicategory ↔ ∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → CategoryTheory.HasLiftingProperty (SSet.horn n i).ι (t.from S)
SSet.quasicategory_of_from_innerFibrations 📋 Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
(S : SSet) {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) (h : SSet.innerFibrations (t.from S)) : S.Quasicategory
SSet.Quasicategory.from_innerFibrations 📋 Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
(S : SSet) [S.Quasicategory] {X : SSet} (t : CategoryTheory.Limits.IsTerminal X) : SSet.innerFibrations (t.from S)
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.equivAugmentedSimplicialObject_inverse_obj_map 📋 Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C) {X✝ Y✝ : (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ} (f : X✝ ⟶ Y✝) : (AugmentedSimplexCategory.equivAugmentedSimplicialObject.inverse.obj X).map f = match match Opposite.unop X✝ with | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x) | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star, match Opposite.unop Y✝ with | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x) | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star, match f with | Opposite.op f_1 => match X✝, Y✝, f_1, f with | Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_1 => (CategoryTheory.WithTerminal.down f).op | Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_1 => CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.of (Opposite.op a)) | Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_1 => CategoryTheory.CategoryStruct.id CategoryTheory.WithTerminal.star with | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => X.left.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => X.hom.app x | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id X.right
CategoryTheory.Functor.PullbackObjObj.ofIsTerminal_snd 📋 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₃] (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op X₁))] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op Y₁))] (h : CategoryTheory.Limits.IsTerminal Y₃) : (CategoryTheory.Functor.PullbackObjObj.ofIsTerminal G f₁ f₃ h).snd = (CategoryTheory.Limits.IsTerminal.isTerminalObj (G.obj (Opposite.op Y₁)) Y₃ h).from ((G.obj (Opposite.op X₁)).obj X₃)
CategoryTheory.Functor.PullbackObjObj.ofIsInitial_fst 📋 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₃] (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃} (f₃ : X₃ ⟶ Y₃) [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.flip.obj X₃)] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.flip.obj Y₃)] (h : CategoryTheory.Limits.IsInitial X₁) : (CategoryTheory.Functor.PullbackObjObj.ofIsInitial G f₁ f₃ h).fst = (CategoryTheory.Limits.IsTerminal.isTerminalObj (G.flip.obj X₃) (Opposite.op X₁) (CategoryTheory.Limits.IsInitial.op C₁ h)).from ((G.obj (Opposite.op Y₁)).obj Y₃)
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 (t.from I)) ≅ X
CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {T : C} (t : CategoryTheory.Limits.IsTerminal T) {W : C} : (Opposite.op X ⋔ CategoryTheory.Arrow.mk (t.from W)) ≅ CategoryTheory.Arrow.mk ((CategoryTheory.MonoidalClosed.pre X.hom).app W)
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_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.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.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.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.PullbackHom.isTerminalIso_hom_left 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {T : C} (t : CategoryTheory.Limits.IsTerminal T) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso X t).hom.left = CategoryTheory.CategoryStruct.id (X.right ⟹ W)
CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso_inv_left 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {T : C} (t : CategoryTheory.Limits.IsTerminal T) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso X t).inv.left = CategoryTheory.CategoryStruct.id (X.right ⟹ W)
CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso_hom_right 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {T : C} (t : CategoryTheory.Limits.IsTerminal T) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso X t).hom.right = ⋯.isoPullback.inv
CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso_inv_right 📋 Mathlib.CategoryTheory.Monoidal.PushoutProduct
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C) {T : C} (t : CategoryTheory.Limits.IsTerminal T) {W : C} : (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso X t).inv.right = ⋯.isoPullback.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))) ⋯)))
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isTerminal_iff 📋 Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] {A B K L X Y : C} {f : A ⟶ B} {g : K ⟶ L} (t : CategoryTheory.Limits.IsTerminal Y) : CategoryTheory.HasLiftingProperty (CategoryTheory.Arrow.mk f □ CategoryTheory.Arrow.mk g).hom (t.from X) ↔ CategoryTheory.HasLiftingProperty g ((CategoryTheory.MonoidalClosed.pre f).app 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} {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.Limits.FormalCoproduct.cechIsoCechNerve 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : U.cech ≅ (CategoryTheory.Arrow.mk ((CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U)).cechNerve
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (n : SimplexCategoryᵒᵖ) : U.cech.obj n ≅ (CategoryTheory.Arrow.mk ((CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U)).cechNerve.obj n
CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : U.cech.augmentOfIsTerminal (CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT) ≅ (CategoryTheory.Arrow.mk ((CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U)).augmentedCechNerve
CategoryTheory.Limits.FormalCoproduct.instHasWidePullbackFinHAddNatOfNatRightMkFromIsTerminalInclLeftHom 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (n : ℕ) : CategoryTheory.Limits.HasWidePullback (CategoryTheory.Arrow.mk ((CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U)).right (fun x => (CategoryTheory.Arrow.mk ((CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U)).left) fun x => (CategoryTheory.Arrow.mk ((CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U)).hom
CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve_hom_right 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : (U.cechIsoAugmentedCechNerve hT).hom.right = CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.FormalCoproduct.incl C).obj T)
CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve_hom_left 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : (U.cechIsoAugmentedCechNerve hT).hom.left = (U.cechIsoCechNerve hT).hom
CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve_inv_left 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : (U.cechIsoAugmentedCechNerve hT).inv.left = (U.cechIsoCechNerve hT).inv
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerve_hom_app 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (X : SimplexCategoryᵒᵖ) : (U.cechIsoCechNerve hT).hom.app X = (U.cechIsoCechNerveApp hT X).hom
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerve_inv_app 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (X : SimplexCategoryᵒᵖ) : (U.cechIsoCechNerve hT).inv.app X = (U.cechIsoCechNerveApp hT X).inv
CategoryTheory.Limits.FormalCoproduct.instHasLimitWidePullbackShapeToTypeSimplexCategoryOrderHomFinHAddNatLenOfNatWideCospanObjInclFromIsTerminalIncl 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (n : SimplexCategory) : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.WidePullbackShape.wideCospan ((CategoryTheory.Limits.FormalCoproduct.incl C).obj T) (fun x => U) fun x => (CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U)
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_hom_π 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (n : SimplexCategoryᵒᵖ) (i : CategoryTheory.ToType (Opposite.unop n)) : CategoryTheory.CategoryStruct.comp (U.cechIsoCechNerveApp hT n).hom (CategoryTheory.Limits.WidePullback.π (fun x => (CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U) i) = U.powerπ i
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_hom_π_assoc 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (n : SimplexCategoryᵒᵖ) (i : CategoryTheory.ToType (Opposite.unop n)) {Z : CategoryTheory.Limits.FormalCoproduct C} (h : U ⟶ Z) : CategoryTheory.CategoryStruct.comp (U.cechIsoCechNerveApp hT n).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => (CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U) i) h) = CategoryTheory.CategoryStruct.comp (U.powerπ i) h
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_inv_π 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (n : SimplexCategoryᵒᵖ) (i : CategoryTheory.ToType (Opposite.unop n)) : CategoryTheory.CategoryStruct.comp (U.cechIsoCechNerveApp hT n).inv (U.powerπ i) = CategoryTheory.Limits.WidePullback.π (fun x => (CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U) i
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_inv_π_assoc 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (n : SimplexCategoryᵒᵖ) (i : CategoryTheory.ToType (Opposite.unop n)) {Z : CategoryTheory.Limits.FormalCoproduct C} (h : U ⟶ Z) : CategoryTheory.CategoryStruct.comp (U.cechIsoCechNerveApp hT n).inv (CategoryTheory.CategoryStruct.comp (U.powerπ i) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => (CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U) i) h
CategoryTheory.isSubterminal_of_mono_isTerminal_from 📋 Mathlib.CategoryTheory.Subterminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A T : C} (hT : CategoryTheory.Limits.IsTerminal T) [CategoryTheory.Mono (hT.from A)] : CategoryTheory.IsSubterminal A
CategoryTheory.IsSubterminal.mono_isTerminal_from 📋 Mathlib.CategoryTheory.Subterminal
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} (hA : CategoryTheory.IsSubterminal A) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) : CategoryTheory.Mono (hT.from A)
CategoryTheory.Classifier.isTerminalFrom_eq_χ₀ 📋 Mathlib.CategoryTheory.Subobject.Classifier.Defs
{C : Type u} [CategoryTheory.Category.{v, u} C] (c : CategoryTheory.Subobject.Classifier C) : CategoryTheory.Subobject.Classifier.isTerminalΩ₀.from = c.χ₀
CategoryTheory.Subobject.Classifier.isTerminalFrom_eq_χ₀ 📋 Mathlib.CategoryTheory.Subobject.Classifier.Defs
{C : Type u} [CategoryTheory.Category.{v, u} C] (c : CategoryTheory.Subobject.Classifier C) : CategoryTheory.Subobject.Classifier.isTerminalΩ₀.from = c.χ₀
CategoryTheory.Classifier.mkOfTerminalΩ₀ 📋 Mathlib.CategoryTheory.Subobject.Classifier.Defs
{C : Type u} [CategoryTheory.Category.{v, u} C] (Ω₀ : C) (t : CategoryTheory.Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω) (isPullback : ∀ {U X : C} (m : U ⟶ X) [inst : CategoryTheory.Mono m], CategoryTheory.IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U ⟶ X) [inst : CategoryTheory.Mono m] (χ' : X ⟶ Ω), CategoryTheory.IsPullback m (t.from U) χ' truth → χ' = χ m) : CategoryTheory.Subobject.Classifier C
CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀ 📋 Mathlib.CategoryTheory.Subobject.Classifier.Defs
{C : Type u} [CategoryTheory.Category.{v, u} C] (Ω₀ : C) (t : CategoryTheory.Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω) (isPullback : ∀ {U X : C} (m : U ⟶ X) [inst : CategoryTheory.Mono m], CategoryTheory.IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U ⟶ X) [inst : CategoryTheory.Mono m] (χ' : X ⟶ Ω), CategoryTheory.IsPullback m (t.from U) χ' truth → χ' = χ m) : CategoryTheory.Subobject.Classifier C
CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_Ω 📋 Mathlib.CategoryTheory.Subobject.Classifier.Defs
{C : Type u} [CategoryTheory.Category.{v, u} C] (Ω₀ : C) (t : CategoryTheory.Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω) (isPullback : ∀ {U X : C} (m : U ⟶ X) [inst : CategoryTheory.Mono m], CategoryTheory.IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U ⟶ X) [inst : CategoryTheory.Mono m] (χ' : X ⟶ Ω), CategoryTheory.IsPullback m (t.from U) χ' truth → χ' = χ m) : (CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).Ω = Ω
CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_Ω₀ 📋 Mathlib.CategoryTheory.Subobject.Classifier.Defs
{C : Type u} [CategoryTheory.Category.{v, u} C] (Ω₀ : C) (t : CategoryTheory.Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω) (isPullback : ∀ {U X : C} (m : U ⟶ X) [inst : CategoryTheory.Mono m], CategoryTheory.IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U ⟶ X) [inst : CategoryTheory.Mono m] (χ' : X ⟶ Ω), CategoryTheory.IsPullback m (t.from U) χ' truth → χ' = χ m) : (CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).Ω₀ = Ω₀
CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_truth 📋 Mathlib.CategoryTheory.Subobject.Classifier.Defs
{C : Type u} [CategoryTheory.Category.{v, u} C] (Ω₀ : C) (t : CategoryTheory.Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω) (isPullback : ∀ {U X : C} (m : U ⟶ X) [inst : CategoryTheory.Mono m], CategoryTheory.IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U ⟶ X) [inst : CategoryTheory.Mono m] (χ' : X ⟶ Ω), CategoryTheory.IsPullback m (t.from U) χ' truth → χ' = χ m) : (CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).truth = truth
CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_χ₀ 📋 Mathlib.CategoryTheory.Subobject.Classifier.Defs
{C : Type u} [CategoryTheory.Category.{v, u} C] (Ω₀ : C) (t : CategoryTheory.Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω) (isPullback : ∀ {U X : C} (m : U ⟶ X) [inst : CategoryTheory.Mono m], CategoryTheory.IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U ⟶ X) [inst : CategoryTheory.Mono m] (χ' : X ⟶ Ω), CategoryTheory.IsPullback m (t.from U) χ' truth → χ' = χ m) (Y : C) : (CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).χ₀ Y = t.from Y
CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀_χ 📋 Mathlib.CategoryTheory.Subobject.Classifier.Defs
{C : Type u} [CategoryTheory.Category.{v, u} C] (Ω₀ : C) (t : CategoryTheory.Limits.IsTerminal Ω₀) (Ω : C) (truth : Ω₀ ⟶ Ω) (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω) (isPullback : ∀ {U X : C} (m : U ⟶ X) [inst : CategoryTheory.Mono m], CategoryTheory.IsPullback m (t.from U) (χ m) truth) (uniq : ∀ {U X : C} (m : U ⟶ X) [inst : CategoryTheory.Mono m] (χ' : X ⟶ Ω), CategoryTheory.IsPullback m (t.from U) χ' truth → χ' = χ m) {U✝ X✝ : C} (m : U✝ ⟶ X✝) (x✝ : CategoryTheory.Mono m) : (CategoryTheory.Subobject.Classifier.mkOfTerminalΩ₀ Ω₀ t Ω truth χ isPullback uniq).χ m = χ m
CategoryTheory.Sheaf.classifier_χ₀ 📋 Mathlib.CategoryTheory.Topos.Sheaf
{C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (Y : CategoryTheory.Sheaf J (Type (max u v))) : (CategoryTheory.Sheaf.classifier J).χ₀ Y = (CategoryTheory.Sheaf.isTerminalTerminal J CategoryTheory.Limits.Types.isTerminalPUnit).from Y
CategoryTheory.Presheaf.classifier_χ₀ 📋 Mathlib.CategoryTheory.Topos.Sheaf
(C : Type u) [CategoryTheory.Category.{v, u} C] (Y : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) : (CategoryTheory.Presheaf.classifier C).χ₀ Y = (CategoryTheory.Functor.isTerminalConst Cᵒᵖ CategoryTheory.Limits.Types.isTerminalPUnit).from Y
CategoryTheory.Presheaf.isPullback_χ_truth 📋 Mathlib.CategoryTheory.Topos.Sheaf
{C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor Cᵒᵖ (Type (max u v))} (m : F ⟶ G) [CategoryTheory.Mono m] : CategoryTheory.IsPullback m ((CategoryTheory.Functor.isTerminalConst Cᵒᵖ CategoryTheory.Limits.Types.isTerminalPUnit).from F) (CategoryTheory.Presheaf.χ m) (CategoryTheory.Presheaf.truth C)
CategoryTheory.Sheaf.isPullback_χ_truth 📋 Mathlib.CategoryTheory.Topos.Sheaf
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F G : CategoryTheory.Sheaf J (Type (max u v))} (m : F ⟶ G) [CategoryTheory.Mono m] : CategoryTheory.IsPullback m ((CategoryTheory.Sheaf.isTerminalTerminal J CategoryTheory.Limits.Types.isTerminalPUnit).from F) (CategoryTheory.Sheaf.χ m) (CategoryTheory.Sheaf.truth J)
CategoryTheory.Presheaf.comp_χ_eq 📋 Mathlib.CategoryTheory.Topos.Sheaf
{C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor Cᵒᵖ (Type (max u v))} (m : F ⟶ G) : CategoryTheory.CategoryStruct.comp m (CategoryTheory.Presheaf.χ m) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.isTerminalConst Cᵒᵖ CategoryTheory.Limits.Types.isTerminalPUnit).from F) (CategoryTheory.Presheaf.truth C)
CategoryTheory.Presheaf.χ_unique 📋 Mathlib.CategoryTheory.Topos.Sheaf
{C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor Cᵒᵖ (Type (max u v))} (m : F ⟶ G) (χ' : G ⟶ CategoryTheory.Functor.sieves C) (hχ' : CategoryTheory.IsPullback m ((CategoryTheory.Functor.isTerminalConst Cᵒᵖ CategoryTheory.Limits.Types.isTerminalPUnit).from F) χ' (CategoryTheory.Presheaf.truth C)) : χ' = CategoryTheory.Presheaf.χ m
CategoryTheory.Sheaf.χ_unique 📋 Mathlib.CategoryTheory.Topos.Sheaf
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F G : CategoryTheory.Sheaf J (Type (max u v))} (m : F ⟶ G) [CategoryTheory.Mono m] (χ' : G ⟶ CategoryTheory.Sheaf.Ω J) (hχ' : CategoryTheory.IsPullback m ((CategoryTheory.Sheaf.isTerminalTerminal J CategoryTheory.Limits.Types.isTerminalPUnit).from F) χ' (CategoryTheory.Sheaf.truth J)) : χ' = CategoryTheory.Sheaf.χ m
skyscraperPresheaf_map 📋 Mathlib.Topology.Sheaves.Skyscraper
{X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] (A : C) {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V) : (skyscraperPresheaf p₀ A).map i = if h : p₀ ∈ Opposite.unop V then CategoryTheory.eqToHom ⋯ else (⋯ ▸ CategoryTheory.Limits.terminalIsTerminal).from (if p₀ ∈ Opposite.unop U then A else ⊤_ C)
StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app 📋 Mathlib.Topology.Sheaves.Skyscraper
{X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {𝓕 : TopCat.Presheaf C X} {c : C} (f : 𝓕.stalk p₀ ⟶ c) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀ f).app U = if h : p₀ ∈ Opposite.unop U then CategoryTheory.CategoryStruct.comp (𝓕.germ (Opposite.unop U) p₀ h) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯)) else (⋯ ▸ CategoryTheory.Limits.terminalIsTerminal).from (𝓕.obj U)
skyscraperSheaf_obj_map 📋 Mathlib.Topology.Sheaves.Skyscraper
{X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V) : (skyscraperSheaf p₀ A).obj.map i = if h : p₀ ∈ Opposite.unop V then CategoryTheory.eqToHom ⋯ else (⋯ ▸ CategoryTheory.Limits.terminalIsTerminal).from (if p₀ ∈ Opposite.unop U then A else ⊤_ C)
SkyscraperPresheafFunctor.map'_app 📋 Mathlib.Topology.Sheaves.Skyscraper
{X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] {a b : C} (f : a ⟶ b) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (SkyscraperPresheafFunctor.map' p₀ f).app U = if h : p₀ ∈ Opposite.unop U then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯)) else (⋯ ▸ CategoryTheory.Limits.terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj U)
isFlasque_skyscraperSheaf_of_epi_from 📋 Mathlib.Topology.Sheaves.Flasque
{X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (A : C) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Epi (CategoryTheory.Limits.terminalIsTerminal.from A)] : (skyscraperSheaf p₀ A).IsFlasque

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