Loogle!

Result

Found 94 declarations mentioning CategoryTheory.Limits.FormalCoproduct.I.

• CategoryTheory.Limits.FormalCoproduct.I 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} (self : CategoryTheory.Limits.FormalCoproduct C) : Type w
• CategoryTheory.Limits.FormalCoproduct.obj 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} (self : CategoryTheory.Limits.FormalCoproduct C) (i : self.I) : C
• CategoryTheory.Limits.FormalCoproduct.toFun 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) : X.I → CategoryTheory.Limits.FormalCoproduct C
• CategoryTheory.Limits.FormalCoproduct.Hom.f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (self : X.Hom Y) : X.I → Y.I
• CategoryTheory.Limits.FormalCoproduct.incl_obj_I 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : C) : ((CategoryTheory.Limits.FormalCoproduct.incl C).obj X).I = PUnit.{w + 1}
• CategoryTheory.Limits.FormalCoproduct.objIsoOfEq 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) {i j : X.I} (hij : i = j) : X.obj i ≅ X.obj j
• CategoryTheory.Limits.FormalCoproduct.category_id_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (a : X.I) : (CategoryTheory.CategoryStruct.id X).f a = a
• CategoryTheory.Limits.FormalCoproduct.Hom.φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (self : X.Hom Y) (i : X.I) : X.obj i ⟶ Y.obj (self.f i)
• CategoryTheory.Limits.FormalCoproduct.Hom.mk 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (f : X.I → Y.I) (φ : (i : X.I) → X.obj i ⟶ Y.obj (f i)) : X.Hom Y
• CategoryTheory.Limits.FormalCoproduct.objIsoOfEq_rfl 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I) : X.objIsoOfEq ⋯ = CategoryTheory.Iso.refl (X.obj i)
• CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Limits.FormalCoproduct C} (i : Y.I) (f : X ⟶ Y.obj i) : (CategoryTheory.Limits.FormalCoproduct.incl C).obj X ⟶ Y
• CategoryTheory.Limits.FormalCoproduct.category_id_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (x✝ : X.I) : (CategoryTheory.CategoryStruct.id X).φ x✝ = CategoryTheory.CategoryStruct.id (X.obj x✝)
• CategoryTheory.Limits.FormalCoproduct.cofanPtIsoSelf 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) : (CategoryTheory.Limits.FormalCoproduct.cofan X.I X.toFun).pt ≅ X
• CategoryTheory.Limits.FormalCoproduct.Hom.asSigma 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Limits.FormalCoproduct C} (f : (CategoryTheory.Limits.FormalCoproduct.incl C).obj X ⟶ Y) : (i : Y.I) × (X ⟶ Y.obj i)
• CategoryTheory.Limits.FormalCoproduct.inclHomEquiv 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : CategoryTheory.Limits.FormalCoproduct C) : ((CategoryTheory.Limits.FormalCoproduct.incl C).obj X ⟶ Y) ≃ (i : Y.I) × (X ⟶ Y.obj i)
• CategoryTheory.Limits.FormalCoproduct.incl_map_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (x✝ : { I := PUnit.{w + 1}, obj := fun x => X✝ }.I) : ((CategoryTheory.Limits.FormalCoproduct.incl C).map f).f x✝ = PUnit.unit
• CategoryTheory.Limits.FormalCoproduct.homOfPiHom_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {J : Type w} (f : J → C) (φ : (j : J) → f j ⟶ X) (x✝ : { I := J, obj := f }.I) : (CategoryTheory.Limits.FormalCoproduct.homOfPiHom X f φ).f x✝ = PUnit.unit
• CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) : ∐ X.toFun ≅ X
• CategoryTheory.Limits.FormalCoproduct.category_comp_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ Z✝ : CategoryTheory.Limits.FormalCoproduct C} (α : X✝.Hom Y✝) (β : Y✝.Hom Z✝) (a✝ : X✝.I) : (CategoryTheory.CategoryStruct.comp α β).f a✝ = β.f (α.f a✝)
• CategoryTheory.Limits.FormalCoproduct.incl_map_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (x✝ : { I := PUnit.{w + 1}, obj := fun x => X✝ }.I) : ((CategoryTheory.Limits.FormalCoproduct.incl C).map f).φ x✝ = f
• CategoryTheory.Limits.FormalCoproduct.objIsoOfEq_symm 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) {i j : X.I} (hij : i = j) : (X.objIsoOfEq hij).symm = X.objIsoOfEq ⋯
• CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Limits.FormalCoproduct C} (i : Y.I) (f : X ⟶ Y.obj i) (x✝ : ((CategoryTheory.Limits.FormalCoproduct.incl C).obj X).I) : (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i f).f x✝ = i
• CategoryTheory.Limits.FormalCoproduct.cofan_inj_f_fst 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C} (i : 𝒜) (x : (f i).I) : (((CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i).f x).fst = i
• CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Limits.FormalCoproduct C} (i : Y.I) (f : X ⟶ Y.obj i) (x✝ : ((CategoryTheory.Limits.FormalCoproduct.incl C).obj X).I) : (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i f).φ x✝ = f
• CategoryTheory.Limits.FormalCoproduct.isoOfComponents 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (e : X.I ≃ Y.I) (h : (i : X.I) → X.obj i ≅ Y.obj (e i)) : X ≅ Y
• CategoryTheory.Limits.FormalCoproduct.objIsoOfEq_trans 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) {i j k : X.I} (hij : i = j) (hjk : j = k) : X.objIsoOfEq hij ≪≫ X.objIsoOfEq hjk = X.objIsoOfEq ⋯
• CategoryTheory.Limits.FormalCoproduct.eval_obj_obj 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasCoproducts A] (F : CategoryTheory.Functor C A) (X : CategoryTheory.Limits.FormalCoproduct C) : ((CategoryTheory.Limits.FormalCoproduct.eval C A).obj F).obj X = ∐ fun i => F.obj (X.obj i)
• CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl_asSigma 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Limits.FormalCoproduct C} (f : (CategoryTheory.Limits.FormalCoproduct.incl C).obj X ⟶ Y) : CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl (CategoryTheory.Limits.FormalCoproduct.Hom.asSigma f).fst (CategoryTheory.Limits.FormalCoproduct.Hom.asSigma f).snd = f
• CategoryTheory.Limits.FormalCoproduct.cofan_inj 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C} (i : 𝒜) : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i = { f := fun x => ⟨i, x⟩, φ := fun x => CategoryTheory.CategoryStruct.id ((f i).obj x) }
• CategoryTheory.Limits.FormalCoproduct.cofan_inj_f_snd 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C} (i : 𝒜) (x : (f i).I) : (((CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i).f x).snd = x
• CategoryTheory.Limits.FormalCoproduct.evalOp_obj_obj 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasProducts A] (F : CategoryTheory.Functor Cᵒᵖ A) (X : (CategoryTheory.Limits.FormalCoproduct C)ᵒᵖ) : ((CategoryTheory.Limits.FormalCoproduct.evalOp C A).obj F).obj X = ∏ᶜ fun i => F.obj (Opposite.op ((Opposite.unop X).obj i))
• CategoryTheory.Limits.FormalCoproduct.category_comp_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ Z✝ : CategoryTheory.Limits.FormalCoproduct C} (α : X✝.Hom Y✝) (β : Y✝.Hom Z✝) (x✝ : X✝.I) : (CategoryTheory.CategoryStruct.comp α β).φ x✝ = CategoryTheory.CategoryStruct.comp (α.φ x✝) (β.φ (α.f x✝))
• CategoryTheory.Limits.FormalCoproduct.isoOfComponents_hom_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (e : X.I ≃ Y.I) (h : (i : X.I) → X.obj i ≅ Y.obj (e i)) (a : X.I) : (CategoryTheory.Limits.FormalCoproduct.isoOfComponents e h).hom.f a = e a
• CategoryTheory.Limits.FormalCoproduct.isoOfComponents_inv_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (e : X.I ≃ Y.I) (h : (i : X.I) → X.obj i ≅ Y.obj (e i)) (a : Y.I) : (CategoryTheory.Limits.FormalCoproduct.isoOfComponents e h).inv.f a = e.symm a
• CategoryTheory.Limits.FormalCoproduct.cofan_inj_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C} (i : 𝒜) (x : (f i).I) : ((CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i).φ x = CategoryTheory.CategoryStruct.id ((f i).obj x)
• CategoryTheory.Limits.FormalCoproduct.inj_comp_cofanPtIsoSelf_hom 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.FormalCoproduct.cofan X.I X.toFun).inj i) X.cofanPtIsoSelf.hom = CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i))
• CategoryTheory.Limits.FormalCoproduct.hom_ext 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} {f g : X ⟶ Y} (h₁ : f.f = g.f) (h₂ : ∀ (i : X.I), CategoryTheory.CategoryStruct.comp (f.φ i) (CategoryTheory.eqToHom ⋯) = g.φ i) : f = g
• CategoryTheory.Limits.FormalCoproduct.hom_ext_iff' 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (f g : X ⟶ Y) : f = g ↔ ∀ (i : X.I), ∃ (h₁ : f.f i = g.f i), CategoryTheory.CategoryStruct.comp (f.φ i) (CategoryTheory.eqToHom ⋯) = g.φ i
• CategoryTheory.Limits.FormalCoproduct.isColimitCofan_desc_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C) (t : CategoryTheory.Limits.Cofan f) (p : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt.I) : ((CategoryTheory.Limits.FormalCoproduct.isColimitCofan 𝒜 f).desc t).f p = (t.inj p.fst).f p.snd
• CategoryTheory.Limits.FormalCoproduct.hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (f g : X ⟶ Y) : f = g ↔ ∃ (h₁ : f.f = g.f), ∀ (i : X.I), CategoryTheory.CategoryStruct.comp (f.φ i) (CategoryTheory.eqToHom ⋯) = g.φ i
• CategoryTheory.Limits.FormalCoproduct.isoOfComponents_hom_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (e : X.I ≃ Y.I) (h : (i : X.I) → X.obj i ≅ Y.obj (e i)) (i : X.I) : (CategoryTheory.Limits.FormalCoproduct.isoOfComponents e h).hom.φ i = (h i).hom
• CategoryTheory.Limits.FormalCoproduct.ι_comp_coproductIsoSelf_hom 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι X.toFun i) X.coproductIsoSelf.hom = CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i))
• CategoryTheory.Limits.FormalCoproduct.fromIncl_comp_cofanPtIsoSelf_inv 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i))) X.cofanPtIsoSelf.inv = (CategoryTheory.Limits.FormalCoproduct.cofan X.I X.toFun).inj i
• CategoryTheory.Limits.FormalCoproduct.inj_comp_cofanPtIsoSelf_hom_assoc 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I) {Z : CategoryTheory.Limits.FormalCoproduct C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.FormalCoproduct.cofan X.I X.toFun).inj i) (CategoryTheory.CategoryStruct.comp X.cofanPtIsoSelf.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i))) h
• CategoryTheory.Limits.FormalCoproduct.fromIncl_comp_coproductIsoSelf_inv 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i))) X.coproductIsoSelf.inv = CategoryTheory.Limits.Sigma.ι X.toFun i
• CategoryTheory.Limits.FormalCoproduct.isColimitCofan_desc_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C) (t : CategoryTheory.Limits.Cofan f) (p : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt.I) : ((CategoryTheory.Limits.FormalCoproduct.isColimitCofan 𝒜 f).desc t).φ p = (t.inj p.fst).φ p.snd
• CategoryTheory.Limits.FormalCoproduct.ι_comp_coproductIsoSelf_hom_assoc 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I) {Z : CategoryTheory.Limits.FormalCoproduct C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι X.toFun i) (CategoryTheory.CategoryStruct.comp X.coproductIsoSelf.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i))) h
• CategoryTheory.Limits.FormalCoproduct.eval_obj_map 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasCoproducts A] (F : CategoryTheory.Functor C A) {X Y : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Y) : ((CategoryTheory.Limits.FormalCoproduct.eval C A).obj F).map f = CategoryTheory.Limits.Sigma.desc fun i => CategoryTheory.CategoryStruct.comp (F.map (f.φ i)) (CategoryTheory.Limits.Sigma.ι (F.obj ∘ Y.obj) (f.f i))
• CategoryTheory.Limits.FormalCoproduct.fromIncl_comp_cofanPtIsoSelf_inv_assoc 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I) {Z : CategoryTheory.Limits.FormalCoproduct C} (h : (CategoryTheory.Limits.FormalCoproduct.cofan X.I X.toFun).pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i))) (CategoryTheory.CategoryStruct.comp X.cofanPtIsoSelf.inv h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.FormalCoproduct.cofan X.I X.toFun).inj i) h
• CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_hom_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (a✝ : (∐ X.toFun).I) : X.coproductIsoSelf.hom.f a✝ = X.cofanPtIsoSelf.hom.f ((CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt X.I X.toFun).hom.f a✝)
• CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_inv_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (a✝ : X.I) : X.coproductIsoSelf.inv.f a✝ = (CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt X.I X.toFun).inv.f (X.cofanPtIsoSelf.inv.f a✝)
• CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_apply_fst 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : CategoryTheory.Limits.FormalCoproduct C) (f : (CategoryTheory.Limits.FormalCoproduct.incl C).obj X ⟶ Y) : ((CategoryTheory.Limits.FormalCoproduct.inclHomEquiv X Y) f).fst = f.f PUnit.unit
• CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_apply_snd 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : CategoryTheory.Limits.FormalCoproduct C) (f : (CategoryTheory.Limits.FormalCoproduct.incl C).obj X ⟶ Y) : ((CategoryTheory.Limits.FormalCoproduct.inclHomEquiv X Y) f).snd = f.φ PUnit.unit
• CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_symm_apply_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : CategoryTheory.Limits.FormalCoproduct C) (f : (i : Y.I) × (X ⟶ Y.obj i)) (x✝ : ((CategoryTheory.Limits.FormalCoproduct.incl C).obj X).I) : ((CategoryTheory.Limits.FormalCoproduct.inclHomEquiv X Y).symm f).f x✝ = f.fst
• CategoryTheory.Limits.FormalCoproduct.fromIncl_comp_coproductIsoSelf_inv_assoc 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I) {Z : CategoryTheory.Limits.FormalCoproduct C} (h : ∐ X.toFun ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i))) (CategoryTheory.CategoryStruct.comp X.coproductIsoSelf.inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι X.toFun i) h
• CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_symm_apply_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : CategoryTheory.Limits.FormalCoproduct C) (f : (i : Y.I) × (X ⟶ Y.obj i)) (x✝ : ((CategoryTheory.Limits.FormalCoproduct.incl C).obj X).I) : ((CategoryTheory.Limits.FormalCoproduct.inclHomEquiv X Y).symm f).φ x✝ = f.snd
• CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_apply_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C) (t : CategoryTheory.Limits.FormalCoproduct C) (m : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt ⟶ t) (i : 𝒜) (a✝ : (f i).I) : ((CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv 𝒜 f t) m i).f a✝ = m.f (((CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i).f a✝)
• CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_symm_apply_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C) (t : CategoryTheory.Limits.FormalCoproduct C) (s : (i : 𝒜) → f i ⟶ t) (p : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt.I) : ((CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv 𝒜 f t).symm s).f p = (s p.fst).f p.snd
• CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_symm_apply_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C) (t : CategoryTheory.Limits.FormalCoproduct C) (s : (i : 𝒜) → f i ⟶ t) (p : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt.I) : ((CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv 𝒜 f t).symm s).φ p = (s p.fst).φ p.snd
• CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv_apply_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒜 : Type w) (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C) (t : CategoryTheory.Limits.FormalCoproduct C) (m : (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt ⟶ t) (i : 𝒜) (x✝ : (f i).I) : ((CategoryTheory.Limits.FormalCoproduct.cofanHomEquiv 𝒜 f t) m i).φ x✝ = m.φ (((CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i).f x✝)
• CategoryTheory.Limits.FormalCoproduct.evalOp_obj_map 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasProducts A] (F : CategoryTheory.Functor Cᵒᵖ A) {X✝ Y✝ : (CategoryTheory.Limits.FormalCoproduct C)ᵒᵖ} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Limits.FormalCoproduct.evalOp C A).obj F).map f = CategoryTheory.Limits.Pi.lift fun i => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => F.obj (Opposite.op ((Opposite.unop X✝).obj i))) (f.unop.f i)) (F.map (f.unop.φ i).op)
• CategoryTheory.Limits.FormalCoproduct.isoOfComponents_inv_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (e : X.I ≃ Y.I) (h : (i : X.I) → X.obj i ≅ Y.obj (e i)) (i : Y.I) : (CategoryTheory.Limits.FormalCoproduct.isoOfComponents e h).inv.φ i = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (h (e.symm i)).inv
• CategoryTheory.Limits.FormalCoproduct.pullbackCone 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) : CategoryTheory.Limits.PullbackCone f g
• CategoryTheory.Limits.FormalCoproduct.eval_map_app 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasCoproducts A] {X✝ Y✝ : CategoryTheory.Functor C A} (α : X✝ ⟶ Y✝) (f : CategoryTheory.Limits.FormalCoproduct C) : ((CategoryTheory.Limits.FormalCoproduct.eval C A).map α).app f = CategoryTheory.Limits.Sigma.map fun i => α.app (f.obj i)
• CategoryTheory.Limits.FormalCoproduct.pullbackCone_fst_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) (i : (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).pt.I) : (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).fst.f i = (↑i).1
• CategoryTheory.Limits.FormalCoproduct.pullbackCone_snd_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) (i : (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).pt.I) : (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).snd.f i = (↑i).2
• CategoryTheory.Limits.FormalCoproduct.pullbackCone_condition 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).fst f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).snd g
• CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_inv_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (x✝ : X.I) : X.coproductIsoSelf.inv.φ x✝ = CategoryTheory.CategoryStruct.comp (X.cofanPtIsoSelf.inv.φ x✝) ((CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt X.I X.toFun).inv.φ (X.cofanPtIsoSelf.inv.f x✝))
• CategoryTheory.Limits.FormalCoproduct.coproductIsoSelf_hom_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (x✝ : (∐ X.toFun).I) : X.coproductIsoSelf.hom.φ x✝ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt X.I X.toFun).hom.φ x✝) (X.cofanPtIsoSelf.hom.φ ((CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt X.I X.toFun).hom.f x✝))
• CategoryTheory.Limits.FormalCoproduct.evalOp_map_app 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasProducts A] {X✝ Y✝ : CategoryTheory.Functor Cᵒᵖ A} (α : X✝ ⟶ Y✝) (f : (CategoryTheory.Limits.FormalCoproduct C)ᵒᵖ) : ((CategoryTheory.Limits.FormalCoproduct.evalOp C A).map α).app f = CategoryTheory.Limits.Pi.map fun i => α.app (Opposite.op ((Opposite.unop f).obj i))
• CategoryTheory.Limits.FormalCoproduct.hasPullback_of_pullbackCone 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) (hpb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i)) : CategoryTheory.Limits.HasPullback f g
• CategoryTheory.Limits.FormalCoproduct.isLimitPullbackCone 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) (hpb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb)
• CategoryTheory.Limits.FormalCoproduct.isPullback 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) (hpb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i)) : CategoryTheory.IsPullback (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).fst (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).snd f g
• CategoryTheory.Limits.FormalCoproduct.pullbackCone_fst_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) (i : (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).pt.I) : (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).fst.φ i = (pb i).fst
• CategoryTheory.Limits.FormalCoproduct.pullbackCone_snd_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) (i : (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).pt.I) : (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).snd.φ i = (pb i).snd
• CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) (hpb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i)) (T : CategoryTheory.Limits.FormalCoproduct C) : (T ⟶ (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).pt) ≃ { p // CategoryTheory.CategoryStruct.comp p.1 f = CategoryTheory.CategoryStruct.comp p.2 g }
• CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_apply_coe 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) (hpb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i)) (T : CategoryTheory.Limits.FormalCoproduct C) (m : T ⟶ (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).pt) : ↑((CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv f g pb hpb T) m) = (CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).fst, CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).snd)
• CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_symm_apply_f_coe 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) (hpb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i)) (T : CategoryTheory.Limits.FormalCoproduct C) (s : { p // CategoryTheory.CategoryStruct.comp p.1 f = CategoryTheory.CategoryStruct.comp p.2 g }) (i : T.I) : ↑(((CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv f g pb hpb T).symm s).f i) = ((↑s).1.f i, (↑s).2.f i)
• CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_symm_apply_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z) (g : Y ⟶ Z) (pb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) (hpb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i)) (T : CategoryTheory.Limits.FormalCoproduct C) (s : { p // CategoryTheory.CategoryStruct.comp p.1 f = CategoryTheory.CategoryStruct.comp p.2 g }) (i : T.I) : ((CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv f g pb hpb T).symm s).φ i = (hpb ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).lift (CategoryTheory.Limits.PullbackCone.mk ((↑s).1.φ i) ((↑s).2.φ i) ⋯)
• CategoryTheory.Limits.FormalCoproduct.power_I 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] : (U.power α).I = (α → U.I)
• CategoryTheory.Limits.FormalCoproduct.powerπ_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α : Type} [CategoryTheory.Limits.HasProductsOfShape α C] (a : α) (i : (U.power α).I) : (U.powerπ a).f i = i a
• CategoryTheory.Limits.FormalCoproduct.power_obj 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] (i : α → U.I) : (U.power α).obj i = ∏ᶜ U.obj ∘ i
• CategoryTheory.Limits.FormalCoproduct.mapPower_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α β : Type t} [CategoryTheory.Limits.HasProductsOfShape α C] [CategoryTheory.Limits.HasProductsOfShape β C] (f : α → β) : (U.mapPower f).f = fun i => i ∘ f
• CategoryTheory.Limits.FormalCoproduct.powerMap_f 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {U V : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V) (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] : (CategoryTheory.Limits.FormalCoproduct.powerMap f α).f = fun i => f.f ∘ i
• CategoryTheory.Limits.FormalCoproduct.powerπ_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α : Type} [CategoryTheory.Limits.HasProductsOfShape α C] (a : α) (x✝ : (U.power α).I) : (U.powerπ a).φ x✝ = CategoryTheory.Limits.Pi.π (U.obj ∘ x✝) a
• CategoryTheory.Limits.FormalCoproduct.mapPower_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α β : Type t} [CategoryTheory.Limits.HasProductsOfShape α C] [CategoryTheory.Limits.HasProductsOfShape β C] (f : α → β) : (U.mapPower f).φ = fun x => CategoryTheory.Limits.Pi.lift fun x_1 => CategoryTheory.Limits.Pi.π (U.obj ∘ x) (f x_1)
• CategoryTheory.Limits.FormalCoproduct.powerMap_φ 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {U V : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V) (α : Type t) [CategoryTheory.Limits.HasProductsOfShape α C] : (CategoryTheory.Limits.FormalCoproduct.powerMap f α).φ = fun i => CategoryTheory.Limits.Pi.map fun a => f.φ (i a)
• CategoryTheory.Limits.FormalCoproduct.extraDegeneracyCech 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) {i₀ : U.I} (d : T ⟶ U.obj i₀) : (U.cech.augmentOfIsTerminal (CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT)).ExtraDegeneracy
• CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_obj 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) (X : CategoryTheory.Functor Cᵒᵖ A) (X✝ : SimplexCategory) : ((CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor E).obj X).obj X✝ = ∏ᶜ fun i => X.obj (Opposite.op ((E.obj (Opposite.op X✝)).obj i))
• CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_X 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) [CategoryTheory.Preadditive A] (X : CategoryTheory.Functor Cᵒᵖ A) (n : ℕ) : ((CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor E).obj X).X n = ∏ᶜ fun i => X.obj (Opposite.op ((E.obj (Opposite.op { len := n })).obj i))
• CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) [CategoryTheory.Preadditive A] (X : CategoryTheory.Functor Cᵒᵖ A) (i j : ℕ) : ((CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor E).obj X).d i j = CochainComplex.of.d (fun n => ∏ᶜ fun i => X.obj (Opposite.op ((E.obj (Opposite.op { len := n })).obj i))) (AlgebraicTopology.AlternatingCofaceMapComplex.objD ((CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor E).obj X)) i j
• CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) [CategoryTheory.Preadditive A] {X✝ Y✝ : CategoryTheory.Functor Cᵒᵖ A} (f : X✝ ⟶ Y✝) (n : ℕ) : ((CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor E).map f).f n = CategoryTheory.Limits.Pi.map fun i => f.app (Opposite.op ((E.obj (Opposite.op { len := n })).obj i))
• CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_map_app 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) {X✝ Y✝ : CategoryTheory.Functor Cᵒᵖ A} (f : X✝ ⟶ Y✝) (X : SimplexCategory) : ((CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor E).map f).app X = CategoryTheory.Limits.Pi.map fun i => f.app (Opposite.op ((E.obj (Opposite.op X)).obj i))
• CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_map 📋 Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) (X : CategoryTheory.Functor Cᵒᵖ A) {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor E).obj X).map f = CategoryTheory.Limits.Pi.lift fun i => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun i => X.obj (Opposite.op ((E.obj (Opposite.op X✝)).obj i))) ((E.map f.op).f i)) (X.map ((E.map f.op).φ i).op)

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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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

4. 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.

5. 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