prod_preservesConnectedLimits — Mathlib

English

Given a cocone s and an isomorphism f: s.pt → X, Cocones.extend s f is an isomorphism.

Русский

Пусть дан кокон s и изоморфизм f: s.pt → X, тогда Cocones.extend s f является изоморфизмом.

LaTeX

$$$[\mathrm{IsIso}(f)] \Rightarrow \mathrm{IsIso}(\mathrm{Cocones.extend}\ s\ f)$$$

Lean4

/-- The functor `(X × -)` preserves any connected limit.
Note that this functor does not preserve the two most obvious disconnected limits - that is,
`(X × -)` does not preserve products or terminal object, e.g. `(X ⨯ A) ⨯ (X ⨯ B)` is not isomorphic
to `X ⨯ (A ⨯ B)` and `X ⨯ 1` is not isomorphic to `1`.
-/
theorem prod_preservesConnectedLimits [IsConnected J] (X : C) : PreservesLimitsOfShape J (prod.functor.obj X) where
  preservesLimit
    {K} :=
    {
      preserves := fun {c} l =>
        ⟨{  lift := fun s => prod.lift (s.π.app (Classical.arbitrary _) ≫ Limits.prod.fst) (l.lift (forgetCone s))
            fac := fun s j => by
              apply Limits.prod.hom_ext
              · erw [assoc, limMap_π, comp_id, limit.lift_π]
                exact (nat_trans_from_is_connected (s.π ≫ γ₁ X) j (Classical.arbitrary _)).symm
              · simp
            uniq := fun s m L => by
              apply Limits.prod.hom_ext
              · erw [limit.lift_π, ← L (Classical.arbitrary J), assoc, limMap_π, comp_id]
                rfl
              · rw [limit.lift_π]
                apply l.uniq (forgetCone s)
                intro j
                simp [← L j] }⟩ }

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