## Stream: maths

### Topic: more limit stuff

#### Johan Commelin (Dec 17 2018 at 04:08):

I've got the following lemmas

lemma colimit.pre_map {K : Type v} [small_category K] [has_colimits_of_shape.{u v} K C]
(F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟹ E₂) :
colimit.pre F E₁ = colim.map (whisker_right α F) ≫ colimit.pre F E₂ :=
begin
ext1, dsimp,
conv {to_rhs, rw ←category.assoc},
simp,
end

lemma colimit.pre_id (F : J ⥤ C) :
colimit.pre F (functor.id _) = colim.map (functor.left_unitor F).hom := by tidy

lemma colimit.pre_comp
{K : Type v} [small_category K] [has_colimits_of_shape.{u v} K C]
{L : Type v} [small_category L] [has_colimits_of_shape.{u v} L C]
(F : J ⥤ C) (E : K ⥤ J) (D : L ⥤ K) :
colimit.pre F (D ⋙ E) = colim.map (functor.associator D E F).hom
≫ colimit.pre _ D ≫ colimit.pre F E :=
begin
tidy {trace_result := tt},
erw ← category.assoc,
erw colim_ι_map (functor.associator D E F).hom j,
dsimp [functor.associator],
simp,
erw is_colimit.fac,
refl
end


Should I put these (and their duals) into a new PR? Or should this be cast into some other form first?

#### Reid Barton (Dec 17 2018 at 04:28):

Isn't the third one colimit.pre_pre?

#### Reid Barton (Dec 17 2018 at 04:28):

Oh I missed the actual second one.

#### Reid Barton (Dec 17 2018 at 04:29):

The associator is a definitional equality, so you don't really need it.

#### Reid Barton (Dec 17 2018 at 04:31):

Though sometimes Lean tries to be too smart, and gets confused by the reassociation unless you spell things out for it.

#### Johan Commelin (Dec 17 2018 at 05:53):

Aah, I see. So the third one can go. That leaves the other 2.

Last updated: May 18 2021 at 07:19 UTC