Loogle!

Result

Found 82 declarations mentioning CategoryTheory.StructuredArrow.proj.

CategoryTheory.StructuredArrow.proj 📋 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) : CategoryTheory.Functor (CategoryTheory.StructuredArrow S T) C
CategoryTheory.StructuredArrow.proj_faithful 📋 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} : (CategoryTheory.StructuredArrow.proj S T).Faithful
CategoryTheory.StructuredArrow.proj_reflectsIsomorphisms 📋 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} : (CategoryTheory.StructuredArrow.proj S T).ReflectsIsomorphisms
CategoryTheory.StructuredArrow.proj_obj 📋 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) (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T) : (CategoryTheory.StructuredArrow.proj S T).obj X = X.right
CategoryTheory.StructuredArrow.proj_map 📋 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) {Y✝ X✝ : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T} (f : Y✝ ⟶ X✝) : (CategoryTheory.StructuredArrow.proj S T).map f = f.right
CategoryTheory.Functor.toStructuredArrow_comp_proj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (X : D) (F : CategoryTheory.Functor C D) (f : (Y : E) → X ⟶ F.obj (G.obj Y)) (h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z) : (G.toStructuredArrow X F f ⋯).comp (CategoryTheory.StructuredArrow.proj X F) = G
CategoryTheory.Functor.toStructuredArrowCompProj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (X : D) (F : CategoryTheory.Functor C D) (f : (Y : E) → X ⟶ F.obj (G.obj Y)) (h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z) : (G.toStructuredArrow X F f ⋯).comp (CategoryTheory.StructuredArrow.proj X F) ≅ G
CategoryTheory.StructuredArrow.map₂IsoPreEquivalenceInverseCompProj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {T : CategoryTheory.Functor C D} {S : CategoryTheory.Functor D E} {T' : CategoryTheory.Functor C E} (d : D) (e : E) (u : e ⟶ S.obj d) (α : T.comp S ⟶ T') : CategoryTheory.StructuredArrow.map₂ u α ≅ (CategoryTheory.StructuredArrow.preEquivalence T (CategoryTheory.StructuredArrow.mk u)).inverse.comp ((CategoryTheory.StructuredArrow.proj (CategoryTheory.StructuredArrow.mk u) (CategoryTheory.StructuredArrow.pre e T S)).comp (CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id e) α))
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F) ≌ CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) : CategoryTheory.Functor (CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)) (CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F))
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) : CategoryTheory.Functor (CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)) (CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F))
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y✝).left.as = PUnit.unit
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y✝).left.as = PUnit.unit
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y✝).right.left.as = PUnit.unit
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_left_as 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y✝).right.left.as = PUnit.unit
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y✝).right.right = Y✝.right.right
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y✝).right.right = Y✝.right.right
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y✝).hom = Y✝.right.hom
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y✝).hom = Y✝.right.hom
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y✝).right.hom = Y✝.hom
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_obj_right_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) (Y✝ : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).obj Y✝).right.hom = Y✝.hom
CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_obj_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) (Y : CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1)) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse X).obj Y).hom = (Y.right.hom, Y.hom)
CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_map_right_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) {X✝ Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)} (g : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.functor X).map g).right.right = g.right
CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_map_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T × T) {X✝ Y✝ : CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1)} (g : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse X).map g).right = CategoryTheory.Under.Hom.right g.right
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_map_right_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) {X✝ Y✝ : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)} (g : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).map g).right.right = g.right.right
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_map_right_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
{T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D T) (Y : T) (X : D) {X✝ Y✝ : CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F)} (g : X✝ ⟶ Y✝) : ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse F Y X).map g).right.right = CategoryTheory.Under.Hom.right g.right
CategoryTheory.StructuredArrow.createsFiniteLimits 📋 Mathlib.CategoryTheory.Limits.Comma
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T} [CategoryTheory.Limits.PreservesFiniteLimits G] : CategoryTheory.Limits.CreatesFiniteLimits (CategoryTheory.StructuredArrow.proj X G)
CategoryTheory.StructuredArrow.createsLimitsOfSize 📋 Mathlib.CategoryTheory.Limits.Comma
{A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T} [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₃, u₁, u₃} G] : CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₁, max u₁ v₃, u₁} (CategoryTheory.StructuredArrow.proj X G)
CategoryTheory.StructuredArrow.createsLimitsOfShape 📋 Mathlib.CategoryTheory.Limits.Comma
{J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T} [CategoryTheory.Limits.PreservesLimitsOfShape J G] : CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.StructuredArrow.proj X G)
CategoryTheory.StructuredArrow.createsLimit 📋 Mathlib.CategoryTheory.Limits.Comma
{J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T} (F : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X G)) [i : CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.StructuredArrow.proj X G)) G] : CategoryTheory.CreatesLimit F (CategoryTheory.StructuredArrow.proj X G)
CategoryTheory.StructuredArrow.hasLimit 📋 Mathlib.CategoryTheory.Limits.Comma
{J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {X : T} {G : CategoryTheory.Functor A T} (F : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X G)) [i₁ : CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.StructuredArrow.proj X G))] [i₂ : CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.StructuredArrow.proj X G)) G] : CategoryTheory.Limits.HasLimit F
CategoryTheory.Limits.Cone.toStructuredArrow_comp_proj 📋 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) : c.toStructuredArrow.comp (CategoryTheory.StructuredArrow.proj c.pt F) = CategoryTheory.Functor.id J
CategoryTheory.Limits.Cone.toStructuredArrowCompProj 📋 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) : c.toStructuredArrow.comp (CategoryTheory.StructuredArrow.proj c.pt F) ≅ CategoryTheory.Functor.id J
CategoryTheory.Limits.Cone.fromStructuredArrow 📋 Mathlib.CategoryTheory.Limits.ConeCategory
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) {X : D} (G : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X F)) : CategoryTheory.Limits.Cone (G.comp ((CategoryTheory.StructuredArrow.proj X F).comp F))
CategoryTheory.Limits.Cone.fromStructuredArrow_pt 📋 Mathlib.CategoryTheory.Limits.ConeCategory
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) {X : D} (G : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X F)) : (CategoryTheory.Limits.Cone.fromStructuredArrow F G).pt = X
CategoryTheory.Limits.Cone.fromStructuredArrow_π_app 📋 Mathlib.CategoryTheory.Limits.ConeCategory
{J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) {X : D} (G : CategoryTheory.Functor J (CategoryTheory.StructuredArrow X F)) (j : J) : (CategoryTheory.Limits.Cone.fromStructuredArrow F G).π.app j = (G.obj j).hom
CategoryTheory.Limits.Cone.toStructuredArrowCompProj_hom_app 📋 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) (X : J) : c.toStructuredArrowCompProj.hom.app X = CategoryTheory.CategoryStruct.id X
CategoryTheory.Limits.Cone.toStructuredArrowCompProj_inv_app 📋 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) (X : J) : c.toStructuredArrowCompProj.inv.app X = CategoryTheory.CategoryStruct.id X
CategoryTheory.Functor.RightExtension.coneAt 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.RightExtension F) (Y : D) : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj Y L).comp F)
CategoryTheory.Functor.pointwiseRightKanExtension_obj 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] (Y : D) : (L.pointwiseRightKanExtension F).obj Y = CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj Y L).comp F)
CategoryTheory.Functor.structuredArrowMapCone 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor D H) (α : L.comp G ⟶ F) (Y : D) : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj Y L).comp F)
CategoryTheory.Functor.structuredArrowMapCone_pt 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor D H) (α : L.comp G ⟶ F) (Y : D) : (L.structuredArrowMapCone F G α Y).pt = G.obj Y
CategoryTheory.Functor.RightExtension.coneAt_pt 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.RightExtension F) (Y : D) : (E.coneAt Y).pt = (CategoryTheory.CostructuredArrow.left E).obj Y
CategoryTheory.Functor.RightExtension.coneAtFunctor 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (Y : D) : CategoryTheory.Functor (L.RightExtension F) (CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj Y L).comp F))
CategoryTheory.Functor.pointwiseRightKanExtension_lift_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] (G : CategoryTheory.Functor D H) (α : L.comp G ⟶ F) (Y : D) : ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y = CategoryTheory.Limits.limit.lift ((CategoryTheory.StructuredArrow.proj Y L).comp F) (L.structuredArrowMapCone F G α Y)
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) [CategoryTheory.Limits.HasLimit ((CategoryTheory.StructuredArrow.proj Y L).comp F)] : (CategoryTheory.CostructuredArrow.left E).obj Y ≅ CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj Y L).comp F)
CategoryTheory.Functor.RightExtension.coneAtFunctor_obj 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (Y : D) (E : L.RightExtension F) : (CategoryTheory.Functor.RightExtension.coneAtFunctor L F Y).obj E = E.coneAt Y
CategoryTheory.Functor.pointwiseRightKanExtensionCounit_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] (X : C) : (L.pointwiseRightKanExtensionCounit F).app X = CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj (L.obj X) L).comp F) (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X)))
CategoryTheory.Functor.structuredArrowMapCone_π_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor D H) (α : L.comp G ⟶ F) (Y : D) (f : CategoryTheory.StructuredArrow Y L) : (L.structuredArrowMapCone F G α Y).π.app f = CategoryTheory.CategoryStruct.comp (G.map f.hom) (α.app f.right)
CategoryTheory.Functor.RightExtension.coneAtFunctor_map_hom 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (Y : D) {E E' : L.RightExtension F} (φ : E ⟶ E') : ((CategoryTheory.Functor.RightExtension.coneAtFunctor L F Y).map φ).hom = φ.left.app Y
CategoryTheory.Functor.pointwiseRightKanExtension_map 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂) : (L.pointwiseRightKanExtension F).map f = CategoryTheory.Limits.limit.lift ((CategoryTheory.StructuredArrow.proj Y₂ L).comp F) { pt := CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj Y₁ L).comp F), π := { app := fun g => CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj Y₁ L).comp F) ((CategoryTheory.StructuredArrow.map f).obj g), naturality := ⋯ } }
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) [CategoryTheory.Limits.HasLimit ((CategoryTheory.StructuredArrow.proj Y L).comp F)] (g : CategoryTheory.StructuredArrow Y L) : CategoryTheory.CategoryStruct.comp h.isoLimit.inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.left E).map g.hom) ((CategoryTheory.CostructuredArrow.hom E).app g.right)) = CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj Y L).comp F) g
CategoryTheory.Functor.RightExtension.coneAt_π_app 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.RightExtension F) (Y : D) (g : CategoryTheory.StructuredArrow Y L) : (E.coneAt Y).π.app g = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.left E).map g.hom) ((CategoryTheory.CostructuredArrow.hom E).app g.right)
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) [CategoryTheory.Limits.HasLimit ((CategoryTheory.StructuredArrow.proj Y L).comp F)] (g : CategoryTheory.StructuredArrow Y L) : CategoryTheory.CategoryStruct.comp h.isoLimit.hom (CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj Y L).comp F) g) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.left E).map g.hom) ((CategoryTheory.CostructuredArrow.hom E).app g.right)
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π_assoc 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) [CategoryTheory.Limits.HasLimit ((CategoryTheory.StructuredArrow.proj Y L).comp F)] (g : CategoryTheory.StructuredArrow Y L) {Z : H} (h✝ : F.obj g.right ⟶ Z) : CategoryTheory.CategoryStruct.comp h.isoLimit.inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.left E).map g.hom) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.hom E).app g.right) h✝)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj Y L).comp F) g) h✝
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π_assoc 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
{C : Type u_1} {D : Type u_2} {H : Type u_4} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_4, u_4} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) [CategoryTheory.Limits.HasLimit ((CategoryTheory.StructuredArrow.proj Y L).comp F)] (g : CategoryTheory.StructuredArrow Y L) {Z : H} (h✝ : F.obj ((CategoryTheory.StructuredArrow.proj Y L).obj g) ⟶ Z) : CategoryTheory.CategoryStruct.comp h.isoLimit.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj Y L).comp F) g) h✝) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.left E).map g.hom) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.hom E).app g.right) h✝)
CategoryTheory.Functor.ranObjObjIsoLimit 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] (X : D) : (L.ran.obj F).obj X ≅ CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj X L).comp F)
CategoryTheory.Functor.ranObjObjIsoLimit_inv_π_assoc 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] (X : D) (f : CategoryTheory.StructuredArrow X L) {Z : H} (h : F.obj f.right ⟶ Z) : CategoryTheory.CategoryStruct.comp (L.ranObjObjIsoLimit F X).inv (CategoryTheory.CategoryStruct.comp ((L.ran.obj F).map f.hom) (CategoryTheory.CategoryStruct.comp ((L.ranCounit.app F).app f.right) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj X L).comp F) f) h
CategoryTheory.Functor.ranObjObjIsoLimit_hom_π 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] (X : D) (f : CategoryTheory.StructuredArrow X L) : CategoryTheory.CategoryStruct.comp (L.ranObjObjIsoLimit F X).hom (CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj X L).comp F) f) = CategoryTheory.CategoryStruct.comp ((L.ran.obj F).map f.hom) ((L.ranCounit.app F).app f.right)
CategoryTheory.Functor.ranObjObjIsoLimit_inv_π 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] (X : D) (f : CategoryTheory.StructuredArrow X L) : CategoryTheory.CategoryStruct.comp (L.ranObjObjIsoLimit F X).inv (CategoryTheory.CategoryStruct.comp ((L.ran.obj F).map f.hom) ((L.ranCounit.app F).app f.right)) = CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj X L).comp F) f
CategoryTheory.Functor.ranObjObjIsoLimit_hom_π_assoc 📋 Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3} [CategoryTheory.Category.{v_3, u_3} H] [∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (F : CategoryTheory.Functor C H) [L.HasPointwiseRightKanExtension F] (X : D) (f : CategoryTheory.StructuredArrow X L) {Z : H} (h : F.obj ((CategoryTheory.StructuredArrow.proj X L).obj f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (L.ranObjObjIsoLimit F X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj X L).comp F) f) h) = CategoryTheory.CategoryStruct.comp ((L.ran.obj F).map f.hom) (CategoryTheory.CategoryStruct.comp ((L.ranCounit.app F).app f.right) h)
CategoryTheory.StructuredArrow.small_inverseImage_proj_of_locallySmall 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Small
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {P : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.Small.{w, v₁, u₁} P] [CategoryTheory.LocallySmall.{w, v₂, u₂} D] : CategoryTheory.ObjectProperty.Small.{w, v₁, max u₁ v₂} (P.inverseImage (CategoryTheory.StructuredArrow.proj S T))
CategoryTheory.StructuredArrow.isCoseparating_inverseImage_proj 📋 Mathlib.CategoryTheory.Generator.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (S : D) (T : CategoryTheory.Functor C D) {P : CategoryTheory.ObjectProperty C} (hP : P.IsCoseparating) : (P.inverseImage (CategoryTheory.StructuredArrow.proj S T)).IsCoseparating
CategoryTheory.StructuredArrow.final_proj_of_isFiltered 📋 Mathlib.CategoryTheory.Filtered.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsFilteredOrEmpty C] (T : CategoryTheory.Functor C D) [T.Final] (Y : D) : (CategoryTheory.StructuredArrow.proj Y T).Final
CategoryTheory.Functor.preservesPointwiseRightKanExtensionAtOfPreservesLimit 📋 Mathlib.CategoryTheory.Functor.KanExtension.Preserves
{A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B) (L : CategoryTheory.Functor A C) (c : C) [CategoryTheory.Limits.PreservesLimit ((CategoryTheory.StructuredArrow.proj c L).comp F) G] : G.PreservesPointwiseRightKanExtensionAt F L c
CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso 📋 Mathlib.CategoryTheory.Functor.KanExtension.Preserves
{A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B) (L : CategoryTheory.Functor A C) (E : L.RightExtension F) (c : C) : ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).obj E).coneAt c ≅ G.mapCone (E.coneAt c)
CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso_hom_hom 📋 Mathlib.CategoryTheory.Functor.KanExtension.Preserves
{A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B) (L : CategoryTheory.Functor A C) (E : L.RightExtension F) (c : C) : (CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso G F L E c).hom.hom = CategoryTheory.CategoryStruct.id (G.obj (E.left.obj c))
CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso_inv_hom 📋 Mathlib.CategoryTheory.Functor.KanExtension.Preserves
{A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B) (L : CategoryTheory.Functor A C) (E : L.RightExtension F) (c : C) : (CategoryTheory.Functor.RightExtension.coneAtWhiskerRightIso G F L E c).inv.hom = CategoryTheory.CategoryStruct.id (G.obj (E.left.obj c))
CategoryTheory.Functor.IsDenseSubsite.instIsIsoSheafAppCounitSheafAdjunctionCocontinuous 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {A : Type w} [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] [CategoryTheory.Functor.IsDenseSubsite J K G] (Y : CategoryTheory.Sheaf J A) : CategoryTheory.IsIso ((G.sheafAdjunctionCocontinuous A J K).counit.app Y)
CategoryTheory.Functor.IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {A : Type w} [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] [CategoryTheory.Functor.IsDenseSubsite J K G] (Y : CategoryTheory.Sheaf J A) (U : C) (X : A) : CategoryTheory.IsIso ((CategoryTheory.yoneda.map ((G.op.ranCounit.app Y.obj).app (Opposite.op U))).app (Opposite.op X))
CategoryTheory.StructuredArrow.instCreatesColimitsOfShapeProjOfIsConnected 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
{J : Type u'} [CategoryTheory.Category.{v', u'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Functor C D} [CategoryTheory.IsConnected J] {B : D} : CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.StructuredArrow.proj B K)
CategoryTheory.StructuredArrow.instPreservesColimitsOfShapeProjOfIsConnected 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
{J : Type u'} [CategoryTheory.Category.{v', u'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Functor C D} [CategoryTheory.IsConnected J] {B : D} : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.StructuredArrow.proj B K)
SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift 📋 Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
{X : SSet} (sx : X.StrictSegal) {n : ℕ} (s : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj (Opposite.op { len := n }) (SimplexCategory.Truncated.inclusion 2).op).comp ((SimplexCategory.Truncated.inclusion 2).op.comp X))) (x : s.pt) : X.obj (Opposite.op { len := n })
SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃ 📋 Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
{X : SSet} (sx : X.StrictSegal) {n : ℕ} (s : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj (Opposite.op { len := n }) (SimplexCategory.Truncated.inclusion 2).op).comp ((SimplexCategory.Truncated.inclusion 2).op.comp X))) (x : s.pt) (φ : { len := 1 } ⟶ { len := n }) : (CategoryTheory.ConcreteCategory.hom (X.map φ.op)) (SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift sx s x) = (CategoryTheory.ConcreteCategory.hom (s.π.app (SSet.StrictSegal.isPointwiseRightKanExtensionAt.strArrowMk₂ φ SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁._proof_1))) x
SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁ 📋 Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
{X : SSet} (sx : X.StrictSegal) {n : ℕ} (s : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj (Opposite.op { len := n }) (SimplexCategory.Truncated.inclusion 2).op).comp ((SimplexCategory.Truncated.inclusion 2).op.comp X))) (x : s.pt) (i : ℕ) (hi : i < n) : (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc ⟨i, hi⟩).op)) (SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift sx s x) = (CategoryTheory.ConcreteCategory.hom (s.π.app (SSet.StrictSegal.isPointwiseRightKanExtensionAt.strArrowMk₂ (SimplexCategory.mkOfSucc ⟨i, hi⟩) SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁._proof_1))) x
SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂ 📋 Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
{X : SSet} (sx : X.StrictSegal) {n : ℕ} (s : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj (Opposite.op { len := n }) (SimplexCategory.Truncated.inclusion 2).op).comp ((SimplexCategory.Truncated.inclusion 2).op.comp X))) (x : s.pt) (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n) : (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift sx s x) = (CategoryTheory.ConcreteCategory.hom (s.π.app (SSet.StrictSegal.isPointwiseRightKanExtensionAt.strArrowMk₂ (SimplexCategory.mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁._proof_1))) x
Profinite.Extend.cone 📋 Mathlib.Topology.Category.Profinite.Extend
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor Profinite C) (S : Profinite) : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj S FintypeCat.toProfinite).comp (FintypeCat.toProfinite.comp G))
Profinite.Extend.cone_pt 📋 Mathlib.Topology.Category.Profinite.Extend
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor Profinite C) (S : Profinite) : (Profinite.Extend.cone G S).pt = G.obj S
Profinite.Extend.cone_π_app 📋 Mathlib.Topology.Category.Profinite.Extend
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor Profinite C) (S : Profinite) (i : CategoryTheory.StructuredArrow S FintypeCat.toProfinite) : (Profinite.Extend.cone G S).π.app i = G.map i.hom
Profinite.Extend.isLimitCone 📋 Mathlib.Topology.Category.Profinite.Extend
{I : Type u} [CategoryTheory.SmallCategory I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor Profinite C) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CategoryTheory.Epi (c.π.app i)] (hc' : CategoryTheory.Limits.IsLimit (G.mapCone c)) : CategoryTheory.Limits.IsLimit (Profinite.Extend.cone G c.pt)
LightProfinite.Extend.cone 📋 Mathlib.Topology.Category.LightProfinite.Extend
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor LightProfinite C) (S : LightProfinite) : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj S FintypeCat.toLightProfinite).comp (FintypeCat.toLightProfinite.comp G))
LightProfinite.Extend.isLimitCone 📋 Mathlib.Topology.Category.LightProfinite.Extend
{F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor LightProfinite C) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] (hc' : CategoryTheory.Limits.IsLimit (G.mapCone c)) : CategoryTheory.Limits.IsLimit (LightProfinite.Extend.cone G c.pt)

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