Loogle!

Result

Found 94 declarations mentioning CategoryTheory.Limits.Multifork.

CategoryTheory.Limits.Multifork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) : Type (max (max (max w w') u) v)
CategoryTheory.Limits.Multiequalizer.multifork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasMultiequalizer I] : CategoryTheory.Limits.Multifork I
CategoryTheory.Limits.Multifork.ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (a : J.L) : K.pt ⟶ I.left a
CategoryTheory.Limits.Multifork.isoOfι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (t : CategoryTheory.Limits.Multifork I) : t ≅ CategoryTheory.Limits.Multifork.ofι I t.pt t.ι ⋯
CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Limits.MulticospanShape) [Unique J.L] [Unique J.R] {X Y : C} (f g : X ⟶ Y) : CategoryTheory.Limits.Multifork (CategoryTheory.Limits.MulticospanIndex.ofParallelHoms J f g) ≌ CategoryTheory.Limits.Fork f g
CategoryTheory.Limits.Multifork.ofι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) (P : C) (ι : (a : J.L) → P ⟶ I.left a) (w : ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (ι (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (ι (J.snd b)) (I.snd b)) : CategoryTheory.Limits.Multifork I
CategoryTheory.Limits.Multifork.ofPiFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} {hd : CategoryTheory.Limits.IsLimit d} (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) : CategoryTheory.Limits.Multifork I
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] : CategoryTheory.Limits.Multifork I ≌ CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap
CategoryTheory.Limits.Multifork.toPiFork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (K : CategoryTheory.Limits.Multifork I) : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
CategoryTheory.Limits.Multifork.condition 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (b : J.R) : CategoryTheory.CategoryStruct.comp (K.ι (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (K.ι (J.snd b)) (I.snd b)
CategoryTheory.Limits.Multifork.IsLimit.lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {K : CategoryTheory.Limits.Multifork I} (hK : CategoryTheory.Limits.IsLimit K) {T : C} (k : (a : J.L) → T ⟶ I.left a) (hk : ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b)) : T ⟶ K.pt
CategoryTheory.Limits.Multifork.hom_comp_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K₁ K₂ : CategoryTheory.Limits.Multifork I) (f : K₁ ⟶ K₂) (j : J.L) : CategoryTheory.CategoryStruct.comp f.hom (K₂.ι j) = K₁.ι j
CategoryTheory.Limits.Multifork.app_left_eq_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (a : J.L) : K.π.app (CategoryTheory.Limits.WalkingMulticospan.left a) = K.ι a
CategoryTheory.Limits.Multifork.toPiFork_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (K : CategoryTheory.Limits.Multifork I) : (CategoryTheory.Limits.Multifork.toPiFork hc hd K).pt = K.pt
CategoryTheory.Limits.Multifork.IsLimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {K : CategoryTheory.Limits.Multifork I} (hK : CategoryTheory.Limits.IsLimit K) {T : C} {f g : T ⟶ K.pt} (h : ∀ (a : J.L), CategoryTheory.CategoryStruct.comp f (K.ι a) = CategoryTheory.CategoryStruct.comp g (K.ι a)) : f = g
CategoryTheory.Limits.Multifork.condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (b : J.R) {Z : C} (h : I.right b ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ι (J.fst b)) (CategoryTheory.CategoryStruct.comp (I.fst b) h) = CategoryTheory.CategoryStruct.comp (K.ι (J.snd b)) (CategoryTheory.CategoryStruct.comp (I.snd b) h)
CategoryTheory.Limits.Multifork.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {t s : CategoryTheory.Limits.Multifork I} (e : t.pt ≅ s.pt) (h : ∀ (i : J.L), CategoryTheory.CategoryStruct.comp e.hom (s.ι i) = t.ι i := by cat_disch) : t ≅ s
CategoryTheory.Limits.Multifork.IsLimit.fac 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {K : CategoryTheory.Limits.Multifork I} (hK : CategoryTheory.Limits.IsLimit K) {T : C} (k : (a : J.L) → T ⟶ I.left a) (hk : ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b)) (a : J.L) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.IsLimit.lift hK k hk) (K.ι a) = k a
CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.Functor (CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (CategoryTheory.Limits.Multifork I)
CategoryTheory.Limits.Multifork.isoOfι_hom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (t : CategoryTheory.Limits.Multifork I) : t.isoOfι.hom.hom = CategoryTheory.CategoryStruct.id t.pt
CategoryTheory.Limits.Multifork.isoOfι_inv_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (t : CategoryTheory.Limits.Multifork I) : t.isoOfι.inv.hom = CategoryTheory.CategoryStruct.id t.pt
CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (b : J.R) : K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.CategoryStruct.comp (K.ι (J.fst b)) (I.fst b)
CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (b : J.R) : K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.CategoryStruct.comp (K.ι (J.snd b)) (I.snd b)
CategoryTheory.Limits.Multifork.hom_comp_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K₁ K₂ : CategoryTheory.Limits.Multifork I) (f : K₁ ⟶ K₂) (j : J.L) {Z : C} (h : I.left j ⟶ Z) : CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp (K₂.ι j) h) = CategoryTheory.CategoryStruct.comp (K₁.ι j) h
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.Limits.Multifork I ≌ CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)
CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.Functor (CategoryTheory.Limits.Multifork I) (CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd))
CategoryTheory.Limits.Multifork.IsLimit.fac_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {K : CategoryTheory.Limits.Multifork I} (hK : CategoryTheory.Limits.IsLimit K) {T : C} (k : (a : J.L) → T ⟶ I.left a) (hk : ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b)) (a : J.L) {Z : C} (h : I.left a ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.IsLimit.lift hK k hk) (CategoryTheory.CategoryStruct.comp (K.ι a) h) = CategoryTheory.CategoryStruct.comp (k a) h
CategoryTheory.Limits.Multifork.ext_hom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {t s : CategoryTheory.Limits.Multifork I} (e : t.pt ≅ s.pt) (h : ∀ (i : J.L), CategoryTheory.CategoryStruct.comp e.hom (s.ι i) = t.ι i := by cat_disch) : (CategoryTheory.Limits.Multifork.ext e h).hom.hom = e.hom
CategoryTheory.Limits.Multifork.ext_inv_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} {t s : CategoryTheory.Limits.Multifork I} (e : t.pt ≅ s.pt) (h : ∀ (i : J.L), CategoryTheory.CategoryStruct.comp e.hom (s.ι i) = t.ι i := by cat_disch) : (CategoryTheory.Limits.Multifork.ext e h).inv.hom = e.inv
CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) : (I.ofPiForkFunctor hd).obj a = CategoryTheory.Limits.Multifork.ofPiFork a
CategoryTheory.Limits.Multifork.toPiFork_π_app_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (CategoryTheory.Limits.Multifork.toPiFork hc hd K).ι = CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι
CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) (K : CategoryTheory.Limits.Multifork I) : (I.toPiForkFunctor hc hd).obj K = CategoryTheory.Limits.Multifork.toPiFork hc hd K
CategoryTheory.Limits.Multifork.IsLimit.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (lift : (E : CategoryTheory.Limits.Multifork I) → E.pt ⟶ K.pt) (fac : ∀ (E : CategoryTheory.Limits.Multifork I) (i : J.L), CategoryTheory.CategoryStruct.comp (lift E) (K.ι i) = E.ι i) (uniq : ∀ (E : CategoryTheory.Limits.Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), CategoryTheory.CategoryStruct.comp m (K.ι i) = E.ι i) → m = lift E) : CategoryTheory.Limits.IsLimit K
CategoryTheory.Limits.Multifork.pi_condition 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (I.fstPiMapOfIsLimit c hd) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (I.sndPiMapOfIsLimit c hd)
CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_functor_obj_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Limits.MulticospanShape) [Unique J.L] [Unique J.R] {X Y : C} (f g : X ⟶ Y) (c : CategoryTheory.Limits.Multifork (CategoryTheory.Limits.MulticospanIndex.ofParallelHoms J f g)) : ((CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork J f g).functor.obj c).ι = c.ι default
CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_inverse_obj_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Limits.MulticospanShape) [Unique J.L] [Unique J.R] {X Y : C} (f g : X ⟶ Y) (c : CategoryTheory.Limits.Fork f g) (a : J.L) : ((CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork J f g).inverse.obj c).ι a = c.ι
CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (b : J.R) {Z : C} (h : I.multicospan.obj (CategoryTheory.Limits.WalkingMulticospan.right b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (K.ι (J.snd b)) (I.snd b)) h
CategoryTheory.Limits.Multifork.IsLimit.mk_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (lift : (E : CategoryTheory.Limits.Multifork I) → E.pt ⟶ K.pt) (fac : ∀ (E : CategoryTheory.Limits.Multifork I) (i : J.L), CategoryTheory.CategoryStruct.comp (lift E) (K.ι i) = E.ι i) (uniq : ∀ (E : CategoryTheory.Limits.Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), CategoryTheory.CategoryStruct.comp m (K.ι i) = E.ι i) → m = lift E) (E : CategoryTheory.Limits.Multifork I) : (CategoryTheory.Limits.Multifork.IsLimit.mk K lift fac uniq).lift E = lift E
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_inverse 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).inverse = I.ofPiForkFunctor hd
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_functor 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).functor = I.toPiForkFunctor hc hd
CategoryTheory.Limits.Multifork.pi_condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) {Z : C} (h : d.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (CategoryTheory.CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (CategoryTheory.CategoryStruct.comp (I.sndPiMapOfIsLimit c hd) h)
CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) {K₁ K₂ : CategoryTheory.Limits.Multifork I} (f : K₁ ⟶ K₂) : ((I.toPiForkFunctor hc hd).map f).hom = f.hom
CategoryTheory.Limits.Multifork.isLimitEquivOfIsos 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I I' : CategoryTheory.Limits.MulticospanIndex J C} (c : CategoryTheory.Limits.Multifork I) (c' : CategoryTheory.Limits.Multifork I') (e : c.pt ≅ c'.pt) (el : (i : J.L) → I.left i ≅ I'.left i) (er : (i : J.R) → I.right i ≅ I'.right i) (hl : ∀ (i : J.R), CategoryTheory.CategoryStruct.comp (I.fst i) (er i).hom = CategoryTheory.CategoryStruct.comp (el (J.fst i)).hom (I'.fst i) := by cat_disch) (hr : ∀ (i : J.R), CategoryTheory.CategoryStruct.comp (I.snd i) (er i).hom = CategoryTheory.CategoryStruct.comp (el (J.snd i)).hom (I'.snd i) := by cat_disch) (he : ∀ (i : J.L), CategoryTheory.CategoryStruct.comp e.hom (c'.ι i) = CategoryTheory.CategoryStruct.comp (c.ι i) (el i).hom := by cat_disch) : CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsLimit c'
CategoryTheory.Limits.Multifork.toPiFork_π_app_one 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (CategoryTheory.Limits.Multifork.toPiFork hc hd K).π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (I.fstPiMapOfIsLimit c hd)
CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) {K₁ K₂ : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)} (f : K₁ ⟶ K₂) : ((I.ofPiForkFunctor hd).map f).hom = f.hom
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.functor.obj K).pt = K.pt
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.inverse.obj a).pt = a.pt
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ K₂ : CategoryTheory.Limits.Multifork I} (f : K₁ ⟶ K₂) : (I.multiforkEquivPiFork.functor.map f).hom = f.hom
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_unitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).unitIso = CategoryTheory.NatIso.ofComponents (fun K => CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Multifork I)).obj K).pt) ⋯) ⋯
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) (X : CategoryTheory.Limits.WalkingParallelPair) : (I.multiforkEquivPiFork.functor.obj K).π.app X = CategoryTheory.Limits.WalkingParallelPair.rec (motive := fun t => X = t → (K.pt ⟶ (CategoryTheory.Limits.parallelPair (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))).obj X)) (fun h => ⋯ ▸ CategoryTheory.Limits.Fan.IsLimit.lift (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.left)) K.ι) (fun h => ⋯ ▸ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.left)) K.ι) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) X ⋯
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) (x✝ : CategoryTheory.Limits.WalkingMulticospan J) : (I.multiforkEquivPiFork.inverse.obj a).π.app x✝ = match x✝ with | CategoryTheory.Limits.WalkingMulticospan.left a_1 => CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) a_1) | CategoryTheory.Limits.WalkingMulticospan.right a_1 => CategoryTheory.CategoryStruct.comp a.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.proj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (J.fst a_1)) (I.fst a_1))
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_map_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ K₂ : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))} (f : K₁ ⟶ K₂) : (I.multiforkEquivPiFork.inverse.map f).hom = f.hom
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Multifork I) : (I.multiforkEquivPiFork.unitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_counitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).counitIso = CategoryTheory.NatIso.ofComponents (fun K => CategoryTheory.Limits.Fork.ext (CategoryTheory.Iso.refl (((I.ofPiForkFunctor hd).comp (I.toPiForkFunctor hc hd)).obj K).pt) ⋯) ⋯
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.counitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape} (I : CategoryTheory.Limits.MulticospanIndex J C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (X : CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))) (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))) : (I.multiforkEquivPiFork.counitIso.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
CategoryTheory.GrothendieckTopology.Cover.multifork 📋 Mathlib.CategoryTheory.Sites.Grothendieck
{C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C} {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (S : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.Limits.Multifork (S.index P)
CategoryTheory.Sheaf.multiforkEvaluationCone 📋 Mathlib.CategoryTheory.Sites.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] {K : Type z} [CategoryTheory.Category.{z', z} K] (F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)) (E : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.sheafToPresheaf J D))) (X : C) (W : J.Cover X) (S : CategoryTheory.Limits.Multifork (W.index E.pt)) : CategoryTheory.Limits.Cone (F.comp ((CategoryTheory.sheafToPresheaf J D).comp ((CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op X))))
CategoryTheory.PreOneHypercover.multifork 📋 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.Functor Cᵒᵖ A) : CategoryTheory.Limits.Multifork (E.multicospanIndex F)
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.GrothendieckTopology.OneHypercover.multiforkLift 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {J : CategoryTheory.GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : CategoryTheory.Sheaf J A} (c : CategoryTheory.Limits.Multifork (E.multicospanIndex F.obj)) : c.pt ⟶ F.obj.obj (Opposite.op S)
CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_id 📋 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} (P : CategoryTheory.Functor Cᵒᵖ A) {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} (hc : CategoryTheory.Limits.IsLimit c) (d : CategoryTheory.Limits.Multifork (E.multicospanIndex P)) : (CategoryTheory.PreOneHypercover.Hom.id E).mapMultiforkOfIsLimit P hc d = CategoryTheory.Limits.Multifork.IsLimit.lift hc d.ι ⋯
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.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.GrothendieckTopology.OneHypercover.multiforkLift_map 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {J : CategoryTheory.GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : CategoryTheory.Sheaf J A} (c : CategoryTheory.Limits.Multifork (E.multicospanIndex F.obj)) (i₀ : E.I₀) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift c) (F.obj.map (E.f i₀).op) = c.ι 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)) (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.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.GrothendieckTopology.OneHypercover.multiforkLift_map_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] {J : CategoryTheory.GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : CategoryTheory.Sheaf J A} (c : CategoryTheory.Limits.Multifork (E.multicospanIndex F.obj)) (i₀ : E.I₀) {Z : A} (h : F.obj.obj (Opposite.op (E.X i₀)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift c) (CategoryTheory.CategoryStruct.comp (F.obj.map (E.f i₀).op) h) = CategoryTheory.CategoryStruct.comp (c.ι i₀) h
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift 📋 Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] {H : J.OneHypercoverFamily} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) {X : C} {S : CategoryTheory.Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S) (F : CategoryTheory.Limits.Multifork (CategoryTheory.GrothendieckTopology.Cover.index ⟨S, ⋯⟩ P)) : F.pt ⟶ P.obj (Opposite.op X)
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac 📋 Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] {H : J.OneHypercoverFamily} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) {X : C} {S : CategoryTheory.Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S) (F : CategoryTheory.Limits.Multifork (CategoryTheory.GrothendieckTopology.Cover.index ⟨S, ⋯⟩ P)) [H.IsGenerating] {Y : C} (f : Y ⟶ X) (hf : S.arrows f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift hP hE le F) (P.map f.op) = F.ι { Y := Y, f := f, hf := hf }
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac' 📋 Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] {H : J.OneHypercoverFamily} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) {X : C} {S : CategoryTheory.Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S) (F : CategoryTheory.Limits.Multifork (CategoryTheory.GrothendieckTopology.Cover.index ⟨S, ⋯⟩ P)) (i : E.I₀) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift hP hE le F) (P.map (E.f i).op) = F.ι { Y := E.X i, f := E.f i, hf := ⋯ }
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac'_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] {H : J.OneHypercoverFamily} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) {X : C} {S : CategoryTheory.Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S) (F : CategoryTheory.Limits.Multifork (CategoryTheory.GrothendieckTopology.Cover.index ⟨S, ⋯⟩ P)) (i : E.I₀) {Z : A} (h : P.obj (Opposite.op (E.X i)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift hP hE le F) (CategoryTheory.CategoryStruct.comp (P.map (E.f i).op) h) = CategoryTheory.CategoryStruct.comp (F.ι { Y := E.X i, f := E.f i, hf := ⋯ }) h
CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux 📋 Mathlib.CategoryTheory.Sites.CoverLifting
{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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} (α : G.op.comp R ⟶ F) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) {Y : C} (f : G.obj Y ⟶ X) : s.pt ⟶ F.obj (Opposite.op Y)
CategoryTheory.RanIsSheafOfIsCocontinuous.lift 📋 Mathlib.CategoryTheory.Sites.CoverLifting
{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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) : s.pt ⟶ R.obj (Opposite.op X)
CategoryTheory.RanIsSheafOfIsCocontinuous.fac 📋 Mathlib.CategoryTheory.Sites.CoverLifting
{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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) (i : S.Arrow) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s) (R.map i.f.op) = s.ι i
CategoryTheory.RanIsSheafOfIsCocontinuous.fac_assoc 📋 Mathlib.CategoryTheory.Sites.CoverLifting
{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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) (i : S.Arrow) {Z : A} (h : R.obj (Opposite.op i.Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s) (CategoryTheory.CategoryStruct.comp (R.map i.f.op) h) = CategoryTheory.CategoryStruct.comp (s.ι i) h
CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map' 📋 Mathlib.CategoryTheory.Sites.CoverLifting
{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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} (α : G.op.comp R ⟶ F) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) {Y Y' : C} (f : G.obj Y ⟶ X) (f' : G.obj Y' ⟶ X) {W : C} (a : W ⟶ Y) (b : W ⟶ Y') (w : CategoryTheory.CategoryStruct.comp (G.map a) f = CategoryTheory.CategoryStruct.comp (G.map b) f') : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f) (F.map a.op) = CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f') (F.map b.op)
CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map 📋 Mathlib.CategoryTheory.Sites.CoverLifting
{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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} (α : G.op.comp R ⟶ F) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) {Y : C} (f : G.obj Y ⟶ X) {W : C} (g : W ⟶ Y) (i : S.Arrow) (h : G.obj W ⟶ i.Y) (w : CategoryTheory.CategoryStruct.comp h i.f = CategoryTheory.CategoryStruct.comp (G.map g) f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f) (F.map g.op) = CategoryTheory.CategoryStruct.comp (s.ι i) (CategoryTheory.CategoryStruct.comp (R.map h.op) (α.app (Opposite.op W)))
CategoryTheory.RanIsSheafOfIsCocontinuous.fac' 📋 Mathlib.CategoryTheory.Sites.CoverLifting
{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} {A : Type w} [CategoryTheory.Category.{w', w} A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R ⟶ F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} (s : CategoryTheory.Limits.Multifork (S.index R)) (j : CategoryTheory.StructuredArrow (Opposite.op X) G.op) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s) (CategoryTheory.CategoryStruct.comp (R.map j.hom) (α.app j.right)) = CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s j.hom.unop
CategoryTheory.Limits.Multifork.toSections 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
{J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} (c : CategoryTheory.Limits.Multifork I) (x : c.pt) : I.sections
CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
{J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} {c : CategoryTheory.Limits.Multifork I} (hc : CategoryTheory.Limits.IsLimit c) : I.sections ≃ c.pt
CategoryTheory.Limits.Multifork.isLimit_types_iff 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
{J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} (c : CategoryTheory.Limits.Multifork I) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ Function.Bijective c.toSections
CategoryTheory.Limits.Multifork.toSections_val 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
{J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} (c : CategoryTheory.Limits.Multifork I) (x : c.pt) (i : J.L) : (c.toSections x).val i = (CategoryTheory.ConcreteCategory.hom (c.ι i)) x
CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_apply_val 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
{J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} {c : CategoryTheory.Limits.Multifork I} (hc : CategoryTheory.Limits.IsLimit c) (s : I.sections) (i : J.L) : (CategoryTheory.ConcreteCategory.hom (c.ι i)) ((CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv hc) s) = s.val i
CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv_symm_apply_val 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
{J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} {c : CategoryTheory.Limits.Multifork I} (hc : CategoryTheory.Limits.IsLimit c) (x : c.pt) (i : J.L) : ((CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv hc).symm x).val i = (CategoryTheory.ConcreteCategory.hom (c.ι i)) x
CategoryTheory.Limits.Multifork.toSections_fac 📋 Mathlib.CategoryTheory.Limits.Types.Multiequalizer
{J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} (c : CategoryTheory.Limits.Multifork I) : ⇑I.sectionsEquiv.symm ∘ CategoryTheory.Limits.Types.sectionOfCone c = c.toSections
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjMultifork 📋 Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
{C₀ : Type u₀} {C : Type u} [CategoryTheory.Category.{v₀, u₀} C₀] [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀} {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) (X : C) : CategoryTheory.Limits.Multifork ((data X).multicospanIndex G₀.obj)
CategoryTheory.Limits.Multifork.map 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MulticospanShape} {d : CategoryTheory.Limits.MulticospanIndex J C} (c : CategoryTheory.Limits.Multifork d) (F : CategoryTheory.Functor C D) : CategoryTheory.Limits.Multifork (d.map F)
CategoryTheory.Limits.Multifork.map_pt 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MulticospanShape} {d : CategoryTheory.Limits.MulticospanIndex J C} (c : CategoryTheory.Limits.Multifork d) (F : CategoryTheory.Functor C D) : (c.map F).pt = F.obj c.pt
CategoryTheory.Limits.Multifork.isLimitMapOfPreserves 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MulticospanShape} {d : CategoryTheory.Limits.MulticospanIndex J C} (c : CategoryTheory.Limits.Multifork d) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit d.multicospan F] (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (c.map F)
CategoryTheory.Limits.Multifork.isLimitMapEquiv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MulticospanShape} {d : CategoryTheory.Limits.MulticospanIndex J C} (c : CategoryTheory.Limits.Multifork d) (F : CategoryTheory.Functor C D) : CategoryTheory.Limits.IsLimit (F.mapCone c) ≃ CategoryTheory.Limits.IsLimit (c.map F)
CategoryTheory.Limits.Multifork.map_π_app 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MulticospanShape} {d : CategoryTheory.Limits.MulticospanIndex J C} (c : CategoryTheory.Limits.Multifork d) (F : CategoryTheory.Functor C D) (x : CategoryTheory.Limits.WalkingMulticospan J) : (c.map F).π.app x = match x with | CategoryTheory.Limits.WalkingMulticospan.left a => F.map (c.ι a) | CategoryTheory.Limits.WalkingMulticospan.right b => CategoryTheory.CategoryStruct.comp (F.map (c.ι (J.fst b))) (F.map (d.fst b))
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

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