def
category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v} :
(Impl) Given a product shape in C/B, construct the corresponding wide pullback diagram in C.
Equations
- category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F = category_theory.limits.wide_pullback_shape.wide_cospan B (λ (j : J), (F.obj j).left) (λ (j : J), (F.obj j).hom)
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_inverse_obj_π_app
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B)
(c : category_theory.limits.cone F)
(X : category_theory.limits.wide_pullback_shape J) :
def
category_theory.over.construct_products.cones_equiv_inverse_obj
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B) :
(Impl) A preliminary definition to avoid timeouts.
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_inverse_obj_X
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B)
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_inverse_obj_2
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B)
(c : category_theory.limits.cone F) :
def
category_theory.over.construct_products.cones_equiv_inverse
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B) :
(Impl) A preliminary definition to avoid timeouts.
Equations
- category_theory.over.construct_products.cones_equiv_inverse B F = {obj := category_theory.over.construct_products.cones_equiv_inverse_obj B F, map := λ (c₁ c₂ : category_theory.limits.cone F) (f : c₁ ⟶ c₂), {hom := f.hom.left, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_inverse_map_hom
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B)
(c₁ c₂ : category_theory.limits.cone F)
(f : c₁ ⟶ c₂) :
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_functor_obj_π_app
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B)
(c : category_theory.limits.cone (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F))
(j : category_theory.discrete J) :
((category_theory.over.construct_products.cones_equiv_functor B F).obj c).π.app j = category_theory.over.hom_mk (c.π.app (option.some j)) _
def
category_theory.over.construct_products.cones_equiv_functor
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B) :
(Impl) A preliminary definition to avoid timeouts.
Equations
- category_theory.over.construct_products.cones_equiv_functor B F = {obj := λ (c : category_theory.limits.cone (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F)), {X := category_theory.over.mk (c.π.app option.none), π := {app := λ (j : category_theory.discrete J), category_theory.over.hom_mk (c.π.app (option.some j)) _, naturality' := _}}, map := λ (c₁ c₂ : category_theory.limits.cone (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F)) (f : c₁ ⟶ c₂), {hom := category_theory.over.hom_mk f.hom _, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_functor_obj_X
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B)
(c : category_theory.limits.cone (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F)) :
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_functor_map_hom
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B)
(c₁ c₂ : category_theory.limits.cone (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F))
(f : c₁ ⟶ c₂) :
@[simp]
def
category_theory.over.construct_products.cones_equiv_unit_iso
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B) :
(Impl) A preliminary definition to avoid timeouts.
Equations
- category_theory.over.construct_products.cones_equiv_unit_iso B F = category_theory.nat_iso.of_components (λ (_x : category_theory.limits.cone (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F)), category_theory.limits.cones.ext {hom := 𝟙 ((𝟭 (category_theory.limits.cone (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F))).obj _x).X, inv := 𝟙 ((category_theory.over.construct_products.cones_equiv_functor B F ⋙ category_theory.over.construct_products.cones_equiv_inverse B F).obj _x).X, hom_inv_id' := _, inv_hom_id' := _} _) _
@[simp]
def
category_theory.over.construct_products.cones_equiv_counit_iso
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B) :
(Impl) A preliminary definition to avoid timeouts.
Equations
- category_theory.over.construct_products.cones_equiv_counit_iso B F = category_theory.nat_iso.of_components (λ (_x : category_theory.limits.cone F), category_theory.limits.cones.ext {hom := category_theory.over.hom_mk (𝟙 ((category_theory.over.construct_products.cones_equiv_inverse B F ⋙ category_theory.over.construct_products.cones_equiv_functor B F).obj _x).X.left) _, inv := category_theory.over.hom_mk (𝟙 ((𝟭 (category_theory.limits.cone F)).obj _x).X.left) _, hom_inv_id' := _, inv_hom_id' := _} _) _
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_counit_iso_2
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B) :
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_functor_2
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B) :
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_inverse_2
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B) :
def
category_theory.over.construct_products.cones_equiv
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B) :
(Impl) Establish an equivalence between the category of cones for F and for the "grown" F.
Equations
- category_theory.over.construct_products.cones_equiv B F = {functor := category_theory.over.construct_products.cones_equiv_functor B F, inverse := category_theory.over.construct_products.cones_equiv_inverse B F, unit_iso := category_theory.over.construct_products.cones_equiv_unit_iso B F, counit_iso := category_theory.over.construct_products.cones_equiv_counit_iso B F, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.over.construct_products.cones_equiv_unit_iso_2
{C : Type u}
[category_theory.category C]
(B : C)
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B) :
def
category_theory.over.construct_products.has_over_limit_discrete_of_wide_pullback_limit
{C : Type u}
[category_theory.category C]
{B : C}
{J : Type v}
(F : category_theory.discrete J ⥤ category_theory.over B)
[category_theory.limits.has_limit (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F)] :
Use the above equivalence to prove we have a limit.
Equations
- category_theory.over.construct_products.has_over_limit_discrete_of_wide_pullback_limit F = {cone := (category_theory.over.construct_products.cones_equiv B F).functor.obj (category_theory.limits.limit.cone (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F)), is_limit := category_theory.limits.is_limit.of_right_adjoint (category_theory.over.construct_products.cones_equiv B F).functor (category_theory.limits.limit.is_limit (category_theory.over.construct_products.wide_pullback_diagram_of_diagram_over B F))}
def
category_theory.over.construct_products.over_product_of_wide_pullback
{C : Type u}
[category_theory.category C]
{J : Type v}
[category_theory.limits.has_limits_of_shape (category_theory.limits.wide_pullback_shape J) C]
{B : C} :
Given a wide pullback in C, construct a product in C/B.
def
category_theory.over.construct_products.over_binary_product_of_pullback
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{B : C} :
Given a pullback in C, construct a binary product in C/B.
def
category_theory.over.construct_products.over_products_of_wide_pullbacks
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_wide_pullbacks C]
{B : C} :
Given all wide pullbacks in C, construct products in C/B.
def
category_theory.over.construct_products.over_finite_products_of_finite_wide_pullbacks
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_wide_pullbacks C]
{B : C} :
Given all finite wide pullbacks in C, construct finite products in C/B.
Equations
Construct terminal object in the over category. This isn't an instance as it's not typically the
way we want to define terminal objects.
(For instance, this gives a terminal object which is different from the generic one given by
over_product_of_wide_pullback above.)
Equations
- category_theory.over.over_has_terminal B = {has_limit := λ (F : category_theory.discrete pempty ⥤ category_theory.over B), {cone := {X := category_theory.over.mk (𝟙 B), π := {app := λ (p : category_theory.discrete pempty), pempty.elim p, naturality' := _}}, is_limit := {lift := λ (s : category_theory.limits.cone F), category_theory.over.hom_mk s.X.hom _, fac' := _, uniq' := _}}}