hasBiproductsOfShape_of_equiv — Mathlib

English

There is a construction of biproducts of shape J from K given an equivalence J ≃ K, using whiskering and bilimit equivalences.

Русский

Существует конструирование бипродуктов формы J из K при эквивалентности J ≃ K посредством whiskering и эквивалентностей билилимита.

LaTeX

$$$$ \\text{hasBiproductsOfShape}(J,C) \\;\\xleftarrow{\\text{via}}\\; \\text{hasBiproductsOfShape}(K,C) \\text{ along } e:J\\simeq K. $$$$

Lean4

theorem hasBiproductsOfShape_of_equiv {K : Type w'} [HasBiproductsOfShape K C] (e : J ≃ K) : HasBiproductsOfShape J C :=
  ⟨fun F =>
    let ⟨⟨h⟩⟩ := HasBiproductsOfShape.has_biproduct (F ∘ e.symm)
    let ⟨c, hc⟩ := h
    HasBiproduct.mk <| by
      simpa only [Function.comp_def, e.symm_apply_apply] using
        LimitBicone.mk (c.whisker e) ((c.whiskerIsBilimitIff _).2 hc)⟩

Похожие утверждения