liftStructEquiv — Mathlib

English

A universal commuting property tying colimit and limit together via the curry/colimit constructions; a key equality of compositions.

Русский

Единая универсальная свзяь между колимитом и пределом через карри и колимит; ключевое равенство составов.

LaTeX

$$$\\text{ι_colimitLimitToLimitColimit}(F) : \\mathrm{colim}\\;\\lim \\Rightarrow \\lim\\;\\colim$ (описание в терминах категориального конуса).$$$

Lean4

/-- Given a parametrized adjunction `F ⊣₂ G` between bifunctors, structures
`sq₁₂ : F.PushoutObjObj f₁ f₂` and `sq₁₃ : G.PullbackObjObj f₁ f₃`,
there are as many liftings for the commutative square given by a
map `α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃` as there are liftings
for the square given by the corresponding map `Arrow.mk f₂ ⟶ Arrow.mk sq₁₃.π`. -/
noncomputable def liftStructEquiv (α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃) :
    Arrow.LiftStruct α ≃ Arrow.LiftStruct (adj₂.arrowHomEquiv sq₁₂ sq₁₃ α)
    where
  toFun
    l :=
    { l := adj₂.homEquiv l.l
      fac_left := by
        have := l.fac_left
        dsimp at this ⊢
        simp only [← adj₂.homEquiv_naturality_two, ← this, sq₁₂.inl_ι_assoc]
      fac_right := by
        apply sq₁₃.isPullback.hom_ext
        · have := l.fac_left
          dsimp at this ⊢
          simp only [Category.assoc, sq₁₃.π_fst, ← adj₂.homEquiv_naturality_one, arrowHomEquiv_apply_right_fst,
            Arrow.mk_left, ← this, sq₁₂.inr_ι_assoc]
        · have := l.fac_right
          dsimp at this ⊢
          simp only [Category.assoc, sq₁₃.π_snd, ← this, adj₂.homEquiv_naturality_three, arrowHomEquiv_apply_right_snd,
            Arrow.mk_right] }
  invFun
    l :=
    { l := adj₂.homEquiv.symm l.l
      fac_left := by
        apply sq₁₂.isPushout.hom_ext
        · have := l.fac_left
          dsimp at this ⊢
          simp only [sq₁₂.inl_ι_assoc, ← adj₂.homEquiv_symm_naturality_two, this, Equiv.symm_apply_apply]
        · have := l.fac_right =≫ sq₁₃.fst
          dsimp at this ⊢
          simp only [Category.assoc, sq₁₃.π_fst] at this
          simp only [sq₁₂.inr_ι_assoc, ← adj₂.homEquiv_symm_naturality_one, this, Equiv.symm_apply_apply,
            arrowHomEquiv_apply_right_fst, Arrow.mk_left]
      fac_right := by
        have := l.fac_right =≫ sq₁₃.snd
        dsimp at this ⊢
        simp only [Category.assoc, sq₁₃.π_snd, arrowHomEquiv_apply_right_snd, Arrow.mk_right] at this
        rw [← adj₂.homEquiv_symm_naturality_three, this, Equiv.symm_apply_apply] }
  left_inv _ := by aesop
  right_inv _ := by aesop

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