Loogle!

Result

Found 67 declarations mentioning CategoryTheory.PreOneHypercover.Hom.

CategoryTheory.PreOneHypercover.Hom 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.PreOneHypercover S) : Type (max (max u_2 u_3) v)
CategoryTheory.PreOneHypercover.Hom.id 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) : E.Hom E
CategoryTheory.PreOneHypercover.Hom.s₁' 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (k : E.I₁') : F.I₁'
CategoryTheory.PreOneHypercover.Hom.toHom 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (self : E.Hom F) : E.Hom F.toPreZeroHypercover
CategoryTheory.PreOneHypercover.Hom.comp 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {G : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) : E.Hom G
CategoryTheory.PreOneHypercover.Hom.mapMulticospan 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (f : E.Hom F) : CategoryTheory.Functor (CategoryTheory.Limits.WalkingMulticospan E.multicospanShape) (CategoryTheory.Limits.WalkingMulticospan F.multicospanShape)
CategoryTheory.PreOneHypercover.Hom.s₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) : F.I₁ (self.s₀ i) (self.s₀ j)
CategoryTheory.PreOneHypercover.Hom.h₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) : E.Y k ⟶ F.Y (self.s₁ k)
CategoryTheory.PreOneHypercover.Hom.comp_s₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {G : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) (a✝ : E.I₀) : (f.comp g).s₀ a✝ = g.s₀ (f.s₀ a✝)
CategoryTheory.PreOneHypercover.comp_s₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : CategoryTheory.PreOneHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (a✝ : X✝.I₀) : (CategoryTheory.CategoryStruct.comp f g).s₀ a✝ = g.s₀ (f.s₀ a✝)
CategoryTheory.PreOneHypercover.Hom.mapMulticospan_obj 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (x✝ : CategoryTheory.Limits.WalkingMulticospan E.multicospanShape) : f.mapMulticospan.obj x✝ = match x✝ with | CategoryTheory.Limits.WalkingMulticospan.left i => CategoryTheory.Limits.WalkingMulticospan.left (f.s₀ i) | CategoryTheory.Limits.WalkingMulticospan.right i => CategoryTheory.Limits.WalkingMulticospan.right (f.s₁' i)
CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (P : CategoryTheory.Functor Cᵒᵖ A) {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} (hc : CategoryTheory.Limits.IsLimit c) (d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)) : d.pt ⟶ c.pt
CategoryTheory.PreOneHypercover.Hom.comp_s₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {G : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) {i✝ j✝ : E.I₀} (a✝ : E.I₁ i✝ j✝) : (f.comp g).s₁ a✝ = g.s₁ (f.s₁ a✝)
CategoryTheory.PreOneHypercover.interFst 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] : (E.inter F).Hom E
CategoryTheory.PreOneHypercover.interSnd 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] : (E.inter F).Hom F
CategoryTheory.PreOneHypercover.comp_s₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : CategoryTheory.PreOneHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) {i✝ j✝ : X✝.I₀} (a✝ : X✝.I₁ i✝ j✝) : (CategoryTheory.CategoryStruct.comp f g).s₁ a✝ = g.s₁ (f.s₁ a✝)
CategoryTheory.PreOneHypercover.interLift 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] {G : CategoryTheory.PreOneHypercover S} (f : G.Hom E) (g : G.Hom F) : G.Hom (E.inter F)
CategoryTheory.PreOneHypercover.Hom.comp_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {G : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) (i : E.I₀) : (f.comp g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i))
CategoryTheory.PreOneHypercover.comp_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : CategoryTheory.PreOneHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (i : X✝.I₀) : (CategoryTheory.CategoryStruct.comp f g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i))
CategoryTheory.PreOneHypercover.Hom.w₁₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) : CategoryTheory.CategoryStruct.comp (self.h₁ k) (F.p₁ (self.s₁ k)) = CategoryTheory.CategoryStruct.comp (E.p₁ k) (self.h₀ i)
CategoryTheory.PreOneHypercover.Hom.w₁₂ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) : CategoryTheory.CategoryStruct.comp (self.h₁ k) (F.p₂ (self.s₁ k)) = CategoryTheory.CategoryStruct.comp (E.p₂ k) (self.h₀ j)
CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_comp 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {G : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (P : CategoryTheory.Functor Cᵒᵖ A) {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)} (g : F.Hom G) (t : CategoryTheory.Limits.Multifork (G.multicospanIndex P)) (hd : CategoryTheory.Limits.IsLimit d) : (f.comp g).mapMultiforkOfIsLimit P hc t = CategoryTheory.CategoryStruct.comp (g.mapMultiforkOfIsLimit P hd t) (f.mapMultiforkOfIsLimit P hc d)
CategoryTheory.PreOneHypercover.Hom.w₁₁_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) {Z : C} (h : F.X (self.s₀ i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.h₁ k) (CategoryTheory.CategoryStruct.comp (F.p₁ (self.s₁ k)) h) = CategoryTheory.CategoryStruct.comp (E.p₁ k) (CategoryTheory.CategoryStruct.comp (self.h₀ i) h)
CategoryTheory.PreOneHypercover.Hom.w₁₂_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) {Z : C} (h : F.X (self.s₀ j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.h₁ k) (CategoryTheory.CategoryStruct.comp (F.p₂ (self.s₁ k)) h) = CategoryTheory.CategoryStruct.comp (E.p₂ k) (CategoryTheory.CategoryStruct.comp (self.h₀ j) h)
CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_comp_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {G : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (P : CategoryTheory.Functor Cᵒᵖ A) {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)} (g : F.Hom G) (t : CategoryTheory.Limits.Multifork (G.multicospanIndex P)) (hd : CategoryTheory.Limits.IsLimit d) {Z : A} (h : c.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp ((f.comp g).mapMultiforkOfIsLimit P hc t) h = CategoryTheory.CategoryStruct.comp (g.mapMultiforkOfIsLimit P hd t) (CategoryTheory.CategoryStruct.comp (f.mapMultiforkOfIsLimit P hc d) h)
CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ι 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (P : CategoryTheory.Functor Cᵒᵖ A) {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} (hc : CategoryTheory.Limits.IsLimit c) (d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)) (a : E.I₀) : CategoryTheory.CategoryStruct.comp (f.mapMultiforkOfIsLimit P hc d) (c.ι a) = CategoryTheory.CategoryStruct.comp (d.ι (f.s₀ a)) (P.map (f.h₀ a).op)
CategoryTheory.PreOneHypercover.Hom.mapMulticospan_map 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (f : E.Hom F) {X✝ Y✝ : CategoryTheory.Limits.WalkingMulticospan E.multicospanShape} (x✝ : X✝ ⟶ Y✝) : f.mapMulticospan.map x✝ = match X✝, Y✝, x✝ with | x, .(x), CategoryTheory.Limits.WalkingMulticospan.Hom.id .(x) => CategoryTheory.Limits.WalkingMulticospan.Hom.id (match x with | CategoryTheory.Limits.WalkingMulticospan.left i => CategoryTheory.Limits.WalkingMulticospan.left (f.s₀ i) | CategoryTheory.Limits.WalkingMulticospan.right i => CategoryTheory.Limits.WalkingMulticospan.right (f.s₁' i)) | .(CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.fst i)), .(CategoryTheory.Limits.WalkingMulticospan.right i), CategoryTheory.Limits.WalkingMulticospan.Hom.fst i => CategoryTheory.Limits.WalkingMulticospan.Hom.fst (f.s₁' i) | .(CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.snd i)), .(CategoryTheory.Limits.WalkingMulticospan.right i), CategoryTheory.Limits.WalkingMulticospan.Hom.snd i => CategoryTheory.Limits.WalkingMulticospan.Hom.snd (f.s₁' i)
CategoryTheory.PreOneHypercover.Hom.ext 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {x y : E.Hom F} (s₀ : x.s₀ = y.s₀) (h₀ : x.h₀ ≍ y.h₀) (s₁ : @CategoryTheory.PreOneHypercover.Hom.s₁ C inst✝ S E F x ≍ @CategoryTheory.PreOneHypercover.Hom.s₁ C inst✝ S E F y) (h₁ : @CategoryTheory.PreOneHypercover.Hom.h₁ C inst✝ S E F x ≍ @CategoryTheory.PreOneHypercover.Hom.h₁ C inst✝ S E F y) : x = y
CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ι_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (P : CategoryTheory.Functor Cᵒᵖ A) {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} (hc : CategoryTheory.Limits.IsLimit c) (d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)) (a : E.I₀) {Z : A} (h : (E.multicospanIndex P).left a ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.mapMultiforkOfIsLimit P hc d) (CategoryTheory.CategoryStruct.comp (c.ι a) h) = CategoryTheory.CategoryStruct.comp (d.ι (f.s₀ a)) (CategoryTheory.CategoryStruct.comp (P.map (f.h₀ a).op) h)
CategoryTheory.PreOneHypercover.Hom.ext_iff 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {x y : E.Hom F} : x = y ↔ x.s₀ = y.s₀ ∧ x.h₀ ≍ y.h₀ ∧ @CategoryTheory.PreOneHypercover.Hom.s₁ C inst✝ S E F x ≍ @CategoryTheory.PreOneHypercover.Hom.s₁ C inst✝ S E F y ∧ @CategoryTheory.PreOneHypercover.Hom.h₁ C inst✝ S E F x ≍ @CategoryTheory.PreOneHypercover.Hom.h₁ C inst✝ S E F y
CategoryTheory.PreOneHypercover.Hom.comp_h₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {G : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) {i✝ j✝ : E.I₀} (i : E.I₁ i✝ j✝) : (f.comp g).h₁ i = CategoryTheory.CategoryStruct.comp (f.h₁ i) (g.h₁ (f.s₁ i))
CategoryTheory.PreOneHypercover.Hom.mk 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (toHom : E.Hom F.toPreZeroHypercover) (s₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHom.s₀ i) (toHom.s₀ j)) (h₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (s₁ k)) (w₁₁ : ∀ {i j : E.I₀} (k : E.I₁ i j), CategoryTheory.CategoryStruct.comp (h₁ k) (F.p₁ (s₁ k)) = CategoryTheory.CategoryStruct.comp (E.p₁ k) (toHom.h₀ i) := by cat_disch) (w₁₂ : ∀ {i j : E.I₀} (k : E.I₁ i j), CategoryTheory.CategoryStruct.comp (h₁ k) (F.p₂ (s₁ k)) = CategoryTheory.CategoryStruct.comp (E.p₂ k) (toHom.h₀ j) := by cat_disch) : E.Hom F
CategoryTheory.PreOneHypercover.comp_h₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : CategoryTheory.PreOneHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) {i✝ j✝ : X✝.I₀} (i : X✝.I₁ i✝ j✝) : (CategoryTheory.CategoryStruct.comp f g).h₁ i = CategoryTheory.CategoryStruct.comp (f.h₁ i) (g.h₁ (f.s₁ i))
CategoryTheory.PreOneHypercover.Hom.ext' 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} (hs₀ : f.s₀ = g.s₀) (hh₀ : ∀ (i : E.I₀), f.h₀ i = CategoryTheory.CategoryStruct.comp (g.h₀ i) (CategoryTheory.eqToHom ⋯)) (hs₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)) (hh₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.h₁ k = CategoryTheory.CategoryStruct.comp (g.h₁ k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)).inv (CategoryTheory.eqToHom ⋯))) : f = g
CategoryTheory.PreOneHypercover.Hom.ext'_iff 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} : f = g ↔ ∃ (hs₀ : f.s₀ = g.s₀) (_ : ∀ (i : E.I₀), f.h₀ i = CategoryTheory.CategoryStruct.comp (g.h₀ i) (CategoryTheory.eqToHom ⋯)) (hs₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)), ∀ (i j : E.I₀) (k : E.I₁ i j), f.h₁ k = CategoryTheory.CategoryStruct.comp (g.h₁ k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)).inv (CategoryTheory.eqToHom ⋯))
CategoryTheory.PreOneHypercover.Homotopy 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} (f g : E.Hom F) : Type (max (max v w) w')
CategoryTheory.PreOneHypercover.cylinder 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) : CategoryTheory.PreOneHypercover S
CategoryTheory.PreOneHypercover.cylinderHom 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) : (CategoryTheory.PreOneHypercover.cylinder f g).Hom E
CategoryTheory.PreOneHypercover.exists_nonempty_homotopy 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) : ∃ W h, Nonempty (CategoryTheory.PreOneHypercover.Homotopy (h.comp f) (h.comp g))
CategoryTheory.PreOneHypercover.cylinderX 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) {i : E.I₀} (k : F.I₁ (f.s₀ i) (g.s₀ i)) : C
CategoryTheory.PreOneHypercover.Homotopy.H 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} (self : CategoryTheory.PreOneHypercover.Homotopy f g) (i : E.I₀) : F.I₁ (f.s₀ i) (g.s₀ i)
CategoryTheory.PreOneHypercover.cylinderHomotopy 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) : CategoryTheory.PreOneHypercover.Homotopy ((CategoryTheory.PreOneHypercover.cylinderHom f g).comp f) ((CategoryTheory.PreOneHypercover.cylinderHom f g).comp g)
CategoryTheory.PreOneHypercover.cylinderf 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) {i : E.I₀} (k : F.I₁ (f.s₀ i) (g.s₀ i)) : CategoryTheory.PreOneHypercover.cylinderX f g k ⟶ S
CategoryTheory.PreOneHypercover.cylinder_I₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) : (CategoryTheory.PreOneHypercover.cylinder f g).I₀ = ((i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i))
CategoryTheory.PreOneHypercover.Homotopy.a 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} (self : CategoryTheory.PreOneHypercover.Homotopy f g) (i : E.I₀) : E.X i ⟶ F.Y (self.H i)
CategoryTheory.PreOneHypercover.Homotopy.isLimitMultifork 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] (f : E.Hom F) (g : F.Hom E) (hgf : CategoryTheory.PreOneHypercover.Homotopy (g.comp f) (CategoryTheory.PreOneHypercover.Hom.id F)) {G : CategoryTheory.Functor Cᵒᵖ A} (hE : CategoryTheory.Limits.IsLimit (E.multifork G)) : CategoryTheory.Limits.IsLimit (F.multifork G)
CategoryTheory.PreOneHypercover.Homotopy.isLimitMultiforkEquiv 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] (f : E.Hom F) (g : F.Hom E) (hfg : CategoryTheory.PreOneHypercover.Homotopy (f.comp g) (CategoryTheory.PreOneHypercover.Hom.id E)) (hgf : CategoryTheory.PreOneHypercover.Homotopy (g.comp f) (CategoryTheory.PreOneHypercover.Hom.id F)) {G : CategoryTheory.Functor Cᵒᵖ A} : CategoryTheory.Limits.IsLimit (E.multifork G) ≃ CategoryTheory.Limits.IsLimit (F.multifork G)
CategoryTheory.PreOneHypercover.cylinderHom_s₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) (p : (CategoryTheory.PreOneHypercover.cylinder f g).I₀) : (CategoryTheory.PreOneHypercover.cylinderHom f g).s₀ p = p.fst
CategoryTheory.PreOneHypercover.Homotopy.mapMultiforkOfIsLimit_eq 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {E F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} (H : CategoryTheory.PreOneHypercover.Homotopy f g) (P : CategoryTheory.Functor Cᵒᵖ A) {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} (hc : CategoryTheory.Limits.IsLimit c) (d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)) : f.mapMultiforkOfIsLimit P hc d = g.mapMultiforkOfIsLimit P hc d
CategoryTheory.PreOneHypercover.cylinder_X 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) (p : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)) : (CategoryTheory.PreOneHypercover.cylinder f g).X p = CategoryTheory.PreOneHypercover.cylinderX f g p.snd
CategoryTheory.PreOneHypercover.Homotopy.wl 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} (self : CategoryTheory.PreOneHypercover.Homotopy f g) (i : E.I₀) : CategoryTheory.CategoryStruct.comp (self.a i) (F.p₁ (self.H i)) = f.h₀ i
CategoryTheory.PreOneHypercover.Homotopy.wr 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} (self : CategoryTheory.PreOneHypercover.Homotopy f g) (i : E.I₀) : CategoryTheory.CategoryStruct.comp (self.a i) (F.p₂ (self.H i)) = g.h₀ i
CategoryTheory.PreOneHypercover.cylinder_I₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) (p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)) : (CategoryTheory.PreOneHypercover.cylinder f g).I₁ p q = ULift.{max w w', w} (E.I₁ p.fst q.fst)
CategoryTheory.PreOneHypercover.cylinderHom_s₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) {i✝ j✝ : (CategoryTheory.PreOneHypercover.cylinder f g).I₀} (k : (CategoryTheory.PreOneHypercover.cylinder f g).I₁ i✝ j✝) : (CategoryTheory.PreOneHypercover.cylinderHom f g).s₁ k = k.down
CategoryTheory.PreOneHypercover.Homotopy.wl_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} (self : CategoryTheory.PreOneHypercover.Homotopy f g) (i : E.I₀) {Z : C} (h : F.X (f.s₀ i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.a i) (CategoryTheory.CategoryStruct.comp (F.p₁ (self.H i)) h) = CategoryTheory.CategoryStruct.comp (f.h₀ i) h
CategoryTheory.PreOneHypercover.Homotopy.wr_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} (self : CategoryTheory.PreOneHypercover.Homotopy f g) (i : E.I₀) {Z : C} (h : F.X (g.s₀ i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.a i) (CategoryTheory.CategoryStruct.comp (F.p₂ (self.H i)) h) = CategoryTheory.CategoryStruct.comp (g.h₀ i) h
CategoryTheory.PreOneHypercover.cylinder_f 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) (p : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)) : (CategoryTheory.PreOneHypercover.cylinder f g).f p = CategoryTheory.PreOneHypercover.cylinderf f g p.snd
CategoryTheory.PreOneHypercover.Homotopy.mk 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} (H : (i : E.I₀) → F.I₁ (f.s₀ i) (g.s₀ i)) (a : (i : E.I₀) → E.X i ⟶ F.Y (H i)) (wl : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (a i) (F.p₁ (H i)) = f.h₀ i) (wr : ∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (a i) (F.p₂ (H i)) = g.h₀ i) : CategoryTheory.PreOneHypercover.Homotopy f g
CategoryTheory.PreOneHypercover.sieve₀_cylinder 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) : (CategoryTheory.PreOneHypercover.cylinder f g).sieve₀ = CategoryTheory.Sieve.generate (CategoryTheory.Presieve.bindOfArrows E.X E.f fun i => (CategoryTheory.Sieve.pullback (CategoryTheory.Limits.pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)
CategoryTheory.PreOneHypercover.cylinderHom_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) (p : (CategoryTheory.PreOneHypercover.cylinder f g).I₀) : (CategoryTheory.PreOneHypercover.cylinderHom f g).h₀ p = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)
CategoryTheory.PreOneHypercover.cylinder_Y 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) {p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)} (k : ULift.{max w w', w} (E.I₁ p.fst q.fst)) : (CategoryTheory.PreOneHypercover.cylinder f g).Y k = CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g p.snd) (CategoryTheory.PreOneHypercover.cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)
CategoryTheory.PreOneHypercover.toPullback_cylinder 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) {i j : (CategoryTheory.PreOneHypercover.cylinder f g).I₀} (k : (CategoryTheory.PreOneHypercover.cylinder f g).I₁ i j) : (CategoryTheory.PreOneHypercover.cylinder f g).toPullback k = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g i.snd) (CategoryTheory.PreOneHypercover.cylinderf f g j.snd) (E.f i.fst) (E.f j.fst) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)
CategoryTheory.PreOneHypercover.cylinderHom_h₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) {p q : (CategoryTheory.PreOneHypercover.cylinder f g).I₀} (k : (CategoryTheory.PreOneHypercover.cylinder f g).I₁ p q) : (CategoryTheory.PreOneHypercover.cylinderHom f g).h₁ k = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g p.snd) (CategoryTheory.PreOneHypercover.cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)
CategoryTheory.PreOneHypercover.sieve₁'_cylinder 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) (i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)) : (CategoryTheory.PreOneHypercover.cylinder f g).sieve₁' i j = CategoryTheory.Sieve.pullback (CategoryTheory.Limits.pullback.map ((CategoryTheory.PreOneHypercover.cylinder f g).f i) ((CategoryTheory.PreOneHypercover.cylinder f g).f j) (E.f i.fst) (E.f j.fst) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (E.sieve₁' i.fst j.fst)
CategoryTheory.PreOneHypercover.cylinder_p₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) {p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)} (k : ULift.{max w w', w} (E.I₁ p.fst q.fst)) : (CategoryTheory.PreOneHypercover.cylinder f g).p₁ k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g p.snd) (CategoryTheory.PreOneHypercover.cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.PreOneHypercover.cylinderf f g p.snd) (CategoryTheory.PreOneHypercover.cylinderf f g q.snd))
CategoryTheory.PreOneHypercover.cylinder_p₂ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) {p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)} (k : ULift.{max w w', w} (E.I₁ p.fst q.fst)) : (CategoryTheory.PreOneHypercover.cylinder f g).p₂ k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g p.snd) (CategoryTheory.PreOneHypercover.cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.PreOneHypercover.cylinderf f g p.snd) (CategoryTheory.PreOneHypercover.cylinderf f g q.snd))
CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks 📋 Mathlib.CategoryTheory.Sites.Hypercover.Saturate
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) [E.HasPullbacks] : CategoryTheory.PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks = CategoryTheory.PreOneHypercover.Hom.id E.toPreOneHypercover

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