binaryProductLimitCone — Mathlib

English

There is a construction of a limit cone for the binary product in ModuleCat R, using the object mkOfSMul φ with projections fst and snd given by fst and snd linear maps.

Русский

Существуют данные предела для бинарного произведения в ModuleCat R, используя mkOfSMul φ и проекции fst, snd из линейных отображений fst и snd.

LaTeX

$$$\text{binaryProductLimitCone}(M,N) = \text{limit cone for } (M,N) \text{ with } \mathrm{pt}=\mathrm{ModuleCat.of}(R, M\times N)$$$

Lean4

/-- Construct limit data for a binary product in `ModuleCat R`, using `ModuleCat.of R (M × N)`.
-/
@[simps cone_pt isLimit_lift]
def binaryProductLimitCone (M N : ModuleCat.{v} R) : Limits.LimitCone (pair M N)
    where
  cone :=
    { pt := ModuleCat.of R (M × N)
      π :=
        { app := fun j =>
            Discrete.casesOn j fun j =>
              WalkingPair.casesOn j (ofHom <| LinearMap.fst R M N) (ofHom <| LinearMap.snd R M N)
          naturality := by rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟨⟩⟩⟩ <;> rfl } }
  isLimit :=
    { lift := fun s => ofHom <| LinearMap.prod (s.π.app ⟨WalkingPair.left⟩).hom (s.π.app ⟨WalkingPair.right⟩).hom
      fac := by rintro s (⟨⟩ | ⟨⟩) <;> rfl
      uniq := fun s m w => by
        simp_rw [← w ⟨WalkingPair.left⟩, ← w ⟨WalkingPair.right⟩]
        rfl }

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