Loogle!

Result

Found 61 declarations mentioning CategoryTheory.Limits.HasWidePullback.

CategoryTheory.Limits.HasWidePullback 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
{J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → objs j ⟶ B) : Prop
CategoryTheory.Limits.widePullback 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
{J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (B : C) (objs : J → C) (arrows : (j : J) → objs j ⟶ B) [CategoryTheory.Limits.HasWidePullback B objs arrows] : C
CategoryTheory.Limits.WidePullback.base 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
{J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [CategoryTheory.Limits.HasWidePullback B objs arrows] : CategoryTheory.Limits.widePullback B objs arrows ⟶ B
CategoryTheory.Limits.WidePullback.π 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
{J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [CategoryTheory.Limits.HasWidePullback B objs arrows] (j : J) : CategoryTheory.Limits.widePullback B objs arrows ⟶ objs j
CategoryTheory.Limits.WidePullback.π_arrow 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
{J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [CategoryTheory.Limits.HasWidePullback B objs arrows] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π arrows j) (arrows j) = CategoryTheory.Limits.WidePullback.base arrows
CategoryTheory.Limits.WidePullback.lift 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
{J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C} {arrows : (j : J) → objs j ⟶ B} [CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X ⟶ B) (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) : X ⟶ CategoryTheory.Limits.widePullback B objs arrows
CategoryTheory.Limits.WidePullback.π_arrow_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
{J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [CategoryTheory.Limits.HasWidePullback B objs arrows] (j : J) {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π arrows j) (CategoryTheory.CategoryStruct.comp (arrows j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base arrows) h
CategoryTheory.Limits.WidePullback.lift_base 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
{J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X ⟶ B) (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.lift f fs w) (CategoryTheory.Limits.WidePullback.base arrows) = f
CategoryTheory.Limits.WidePullback.lift_π 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
{J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X ⟶ B) (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.lift f fs w) (CategoryTheory.Limits.WidePullback.π arrows j) = fs j
CategoryTheory.Limits.WidePullback.hom_eq_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
{J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (g : X ⟶ CategoryTheory.Limits.widePullback B objs arrows) : g = CategoryTheory.Limits.WidePullback.lift (CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.WidePullback.base arrows)) (fun j => CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.WidePullback.π arrows j)) ⋯
CategoryTheory.Limits.WidePullback.lift_base_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
{J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X ⟶ B) (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) {Z : C} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.lift f fs w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base arrows) h) = CategoryTheory.CategoryStruct.comp f h
CategoryTheory.Limits.WidePullback.lift_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
{J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X ⟶ B) (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) (j : J) {Z : C} (h : objs j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.lift f fs w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π arrows j) h) = CategoryTheory.CategoryStruct.comp (fs j) h
CategoryTheory.Limits.WidePullback.eq_lift_of_comp_eq 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
{J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X ⟶ B) (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) (g : X ⟶ CategoryTheory.Limits.widePullback B objs arrows) : (∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.WidePullback.π arrows j) = fs j) → CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.WidePullback.base arrows) = f → g = CategoryTheory.Limits.WidePullback.lift f fs w
CategoryTheory.Limits.WidePullback.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
{J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C} (arrows : (j : J) → objs j ⟶ B) [CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (g1 g2 : X ⟶ CategoryTheory.Limits.widePullback B objs arrows) : (∀ (j : J), CategoryTheory.CategoryStruct.comp g1 (CategoryTheory.Limits.WidePullback.π arrows j) = CategoryTheory.CategoryStruct.comp g2 (CategoryTheory.Limits.WidePullback.π arrows j)) → CategoryTheory.CategoryStruct.comp g1 (CategoryTheory.Limits.WidePullback.base arrows) = CategoryTheory.CategoryStruct.comp g2 (CategoryTheory.Limits.WidePullback.base arrows) → g1 = g2
CategoryTheory.Limits.WidePullback.hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
{J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C} {arrows : (j : J) → objs j ⟶ B} [CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} {g1 g2 : X ⟶ CategoryTheory.Limits.widePullback B objs arrows} : g1 = g2 ↔ (∀ (j : J), CategoryTheory.CategoryStruct.comp g1 (CategoryTheory.Limits.WidePullback.π arrows j) = CategoryTheory.CategoryStruct.comp g2 (CategoryTheory.Limits.WidePullback.π arrows j)) ∧ CategoryTheory.CategoryStruct.comp g1 (CategoryTheory.Limits.WidePullback.base arrows) = CategoryTheory.CategoryStruct.comp g2 (CategoryTheory.Limits.WidePullback.base arrows)
CategoryTheory.Limits.Concrete.widePullback_ext' 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
{C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max v w)} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {B : C} {ι : Type w} [Nonempty ι] {X : ι → C} (f : (j : ι) → X j ⟶ B) [CategoryTheory.Limits.HasWidePullback B X f] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.WidePullbackShape.wideCospan B X f) (CategoryTheory.forget C)] (x y : CategoryTheory.ToType (CategoryTheory.Limits.widePullback B X f)) (h : ∀ (j : ι), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.π f j)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.π f j)) y) : x = y
CategoryTheory.Limits.Concrete.widePullback_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
{C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max v w)} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {B : C} {ι : Type w} {X : ι → C} (f : (j : ι) → X j ⟶ B) [CategoryTheory.Limits.HasWidePullback B X f] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.WidePullbackShape.wideCospan B X f) (CategoryTheory.forget C)] (x y : CategoryTheory.ToType (CategoryTheory.Limits.widePullback B X f)) (h₀ : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.base f)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.base f)) y) (h : ∀ (j : ι), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.π f j)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.π f j)) y) : x = y
CategoryTheory.CechNerveTerminalFrom.hasWidePullback' 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.HasWidePullback (⊤_ C) (fun x => X) fun x => CategoryTheory.Limits.terminal.from X
CategoryTheory.Arrow.augmentedCechNerve 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : CategoryTheory.SimplicialObject.Augmented C
CategoryTheory.Arrow.cechNerve 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : CategoryTheory.SimplicialObject C
CategoryTheory.CechNerveTerminalFrom.hasWidePullback 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] (ι : Type w) [CategoryTheory.Limits.HasFiniteProducts C] [Finite ι] (X : C) : CategoryTheory.Limits.HasWidePullback (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)).right (fun x => (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)).left) fun x => (CategoryTheory.Arrow.mk (CategoryTheory.Limits.terminal.from X)).hom
CategoryTheory.SimplicialObject.augmentedCechNerve 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.SimplicialObject.Augmented C)
CategoryTheory.SimplicialObject.cechNerve 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.SimplicialObject C)
CategoryTheory.SimplicialObject.cechNerveAdjunction 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : CategoryTheory.SimplicialObject.Augmented.toArrow ⊣ CategoryTheory.SimplicialObject.augmentedCechNerve
CategoryTheory.SimplicialObject.cechNerve_obj 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (f : CategoryTheory.Arrow C) : CategoryTheory.SimplicialObject.cechNerve.obj f = f.cechNerve
CategoryTheory.Arrow.augmentedCechNerve_right 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : f.augmentedCechNerve.right = f.right
CategoryTheory.Arrow.augmentedCechNerve_left 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] : f.augmentedCechNerve.left = f.cechNerve
CategoryTheory.SimplicialObject.equivalenceLeftToRight 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F) : X ⟶ F.augmentedCechNerve
CategoryTheory.SimplicialObject.equivalenceRightToLeft 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : X ⟶ F.augmentedCechNerve) : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F
CategoryTheory.SimplicialObject.cechNerveEquiv 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) : (CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F) ≃ (X ⟶ F.augmentedCechNerve)
CategoryTheory.SimplicialObject.augmentedCechNerve_obj_right 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (f : CategoryTheory.Arrow C) : (CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).right = f.right
CategoryTheory.Arrow.cechNerve_obj 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (n : SimplexCategoryᵒᵖ) : f.cechNerve.obj n = CategoryTheory.Limits.widePullback f.right (fun x => f.left) fun x => f.hom
CategoryTheory.Arrow.mapAugmentedCechNerve 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] (F : f ⟶ g) : f.augmentedCechNerve ⟶ g.augmentedCechNerve
CategoryTheory.SimplicialObject.cechNerve_map 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] {X✝ Y✝ : CategoryTheory.Arrow C} (F : X✝ ⟶ Y✝) : CategoryTheory.SimplicialObject.cechNerve.map F = CategoryTheory.Arrow.mapCechNerve F
CategoryTheory.Arrow.mapCechNerve 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] (F : f ⟶ g) : f.cechNerve ⟶ g.cechNerve
CategoryTheory.SimplicialObject.augmentedCechNerve_map_right 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] {X✝ Y✝ : CategoryTheory.Arrow C} (F : X✝ ⟶ Y✝) : (CategoryTheory.SimplicialObject.augmentedCechNerve.map F).right = CategoryTheory.Arrow.Hom.right F
CategoryTheory.SimplicialObject.equivalenceLeftToRight_right 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F) : (CategoryTheory.SimplicialObject.equivalenceLeftToRight X F G).right = CategoryTheory.Arrow.Hom.right G
CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_obj 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (f : CategoryTheory.Arrow C) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).left.obj n = CategoryTheory.Limits.widePullback f.right (fun x => f.left) fun x => f.hom
CategoryTheory.Arrow.mapAugmentedCechNerve_right 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] (F : f ⟶ g) : (CategoryTheory.Arrow.mapAugmentedCechNerve F).right = CategoryTheory.Arrow.Hom.right F
CategoryTheory.Arrow.mapAugmentedCechNerve_left 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] (F : f ⟶ g) : (CategoryTheory.Arrow.mapAugmentedCechNerve F).left = CategoryTheory.Arrow.mapCechNerve F
CategoryTheory.SimplicialObject.equivalenceRightToLeft_right 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : X ⟶ F.augmentedCechNerve) : (CategoryTheory.SimplicialObject.equivalenceRightToLeft X F G).right = G.right
CategoryTheory.Arrow.augmentedCechNerve_hom_app 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (x✝ : SimplexCategoryᵒᵖ) : f.augmentedCechNerve.hom.app x✝ = CategoryTheory.Limits.WidePullback.base fun x => f.hom
CategoryTheory.SimplicialObject.augmentedCechNerve_obj_hom_app 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (f : CategoryTheory.Arrow C) (x✝ : SimplexCategoryᵒᵖ) : (CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).hom.app x✝ = CategoryTheory.Limits.WidePullback.base fun x => f.hom
CategoryTheory.SimplicialObject.cechNerveEquiv_apply 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F) : (CategoryTheory.SimplicialObject.cechNerveEquiv X F) G = CategoryTheory.SimplicialObject.equivalenceLeftToRight X F G
CategoryTheory.SimplicialObject.cechNerveEquiv_symm_apply 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : X ⟶ F.augmentedCechNerve) : (CategoryTheory.SimplicialObject.cechNerveEquiv X F).symm G = CategoryTheory.SimplicialObject.equivalenceRightToLeft X F G
CategoryTheory.SimplicialObject.equivalenceRightToLeft_left 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : X ⟶ F.augmentedCechNerve) : (CategoryTheory.SimplicialObject.equivalenceRightToLeft X F G).left = CategoryTheory.CategoryStruct.comp (G.left.app (Opposite.op { len := 0 })) (CategoryTheory.Limits.WidePullback.π (fun x => F.hom) 0)
CategoryTheory.Arrow.mapCechNerve_app 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C} [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom] (F : f ⟶ g) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.Arrow.mapCechNerve F).app n = CategoryTheory.Limits.WidePullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => f.hom) (CategoryTheory.Arrow.Hom.right F)) (fun i => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) i) (CategoryTheory.Arrow.Hom.left F)) ⋯
CategoryTheory.SimplicialObject.augmentedCechNerve_map_left_app 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] {X✝ Y✝ : CategoryTheory.Arrow C} (F : X✝ ⟶ Y✝) (n : SimplexCategoryᵒᵖ) : (CategoryTheory.SimplicialObject.augmentedCechNerve.map F).left.app n = CategoryTheory.Limits.WidePullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => X✝.hom) (CategoryTheory.Arrow.Hom.right F)) (fun i => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => X✝.hom) i) (CategoryTheory.Arrow.Hom.left F)) ⋯
CategoryTheory.Arrow.cechNerve_map 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] {X✝ Y✝ : SimplexCategoryᵒᵖ} (g : X✝ ⟶ Y✝) : f.cechNerve.map g = CategoryTheory.Limits.WidePullback.lift (CategoryTheory.Limits.WidePullback.base fun x => f.hom) (fun i => CategoryTheory.Limits.WidePullback.π (fun x => f.hom) ((SimplexCategory.Hom.toOrderHom g.unop) i)) ⋯
CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_map 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (f : CategoryTheory.Arrow C) {X✝ Y✝ : SimplexCategoryᵒᵖ} (g : X✝ ⟶ Y✝) : (CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).left.map g = CategoryTheory.Limits.WidePullback.lift (CategoryTheory.Limits.WidePullback.base fun x => f.hom) (fun i => CategoryTheory.Limits.WidePullback.π (fun x => f.hom) ((SimplexCategory.Hom.toOrderHom g.unop) i)) ⋯
CategoryTheory.SimplicialObject.equivalenceLeftToRight_left_app 📋 Mathlib.AlgebraicTopology.CechNerve
{C : Type u} [CategoryTheory.Category.{v, u} C] [∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (X : CategoryTheory.SimplicialObject.Augmented C) (F : CategoryTheory.Arrow C) (G : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F) (x : SimplexCategoryᵒᵖ) : (CategoryTheory.SimplicialObject.equivalenceLeftToRight X F G).left.app x = CategoryTheory.Limits.WidePullback.lift (CategoryTheory.CategoryStruct.comp (X.hom.app x) (CategoryTheory.Arrow.Hom.right G)) (fun i => CategoryTheory.CategoryStruct.comp (X.left.map ({ len := 0 }.const (Opposite.unop x) i).op) (CategoryTheory.Arrow.Hom.left G)) ⋯
CategoryTheory.Arrow.AugmentedCechNerve.extraDegeneracy 📋 Mathlib.AlgebraicTopology.ExtraDegeneracy
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (S : CategoryTheory.SplitEpi f.hom) : f.augmentedCechNerve.ExtraDegeneracy
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s 📋 Mathlib.AlgebraicTopology.ExtraDegeneracy
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (S : CategoryTheory.SplitEpi f.hom) (n : ℕ) : f.cechNerve.obj (Opposite.op { len := n }) ⟶ f.cechNerve.obj (Opposite.op { len := n + 1 })
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_base 📋 Mathlib.AlgebraicTopology.ExtraDegeneracy
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (S : CategoryTheory.SplitEpi f.hom) (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n) (CategoryTheory.Limits.WidePullback.base fun x => f.hom) = CategoryTheory.Limits.WidePullback.base fun x => f.hom
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_succ 📋 Mathlib.AlgebraicTopology.ExtraDegeneracy
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (S : CategoryTheory.SplitEpi f.hom) (n : ℕ) (i : Fin (n + 1)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n) (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) i.succ) = CategoryTheory.Limits.WidePullback.π (fun x => f.hom) i
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0 📋 Mathlib.AlgebraicTopology.ExtraDegeneracy
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (S : CategoryTheory.SplitEpi f.hom) (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n) (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => f.hom) S.section_
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_base_assoc 📋 Mathlib.AlgebraicTopology.ExtraDegeneracy
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (S : CategoryTheory.SplitEpi f.hom) (n : ℕ) {Z : C} (h : f.right ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => f.hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => f.hom) h
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_succ_assoc 📋 Mathlib.AlgebraicTopology.ExtraDegeneracy
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (S : CategoryTheory.SplitEpi f.hom) (n : ℕ) (i : Fin (n + 1)) {Z : C} (h : f.left ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) i.succ) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) i) h
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0_assoc 📋 Mathlib.AlgebraicTopology.ExtraDegeneracy
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C) [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (S : CategoryTheory.SplitEpi f.hom) (n : ℕ) {Z : C} (h : f.left ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) 0) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => f.hom) (CategoryTheory.CategoryStruct.comp S.section_ h)
CategoryTheory.Limits.hasWidePullback_of_isTerminal 📋 Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal
{C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type w} {B : C} {objs : ι → C} (arrows : (j : ι) → objs j ⟶ B) [CategoryTheory.Limits.HasProduct objs] (hB : CategoryTheory.Limits.IsTerminal B) : CategoryTheory.Limits.HasWidePullback B objs arrows
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

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