fullSubcategory — Mathlib

Lean4
/-- The restriction of a Cartesian-monoidal category along an object property that's closed under
finite products is Cartesian-monoidal. -/
noncomputable def fullSubcategory (hP₀ : ClosedUnderLimitsOfShape (Discrete PEmpty) P)
    (hP₂ : ClosedUnderLimitsOfShape (Discrete WalkingPair) P) : CartesianMonoidalCategory P.FullSubcategory
    where
  __ :=
    MonoidalCategory.fullSubcategory P (hP₀ isTerminalTensorUnit <| by simp) fun X Y hX hY ↦
      hP₂ (tensorProductIsBinaryProduct X Y) (by rintro ⟨_ | _⟩ <;> simp [hX, hY])
  isTerminalTensorUnit := .ofUniqueHom (fun X ↦ toUnit X.1) fun _ _ ↦ by ext
  fst X Y := fst X.1 Y.1
  snd X Y := snd X.1 Y.1
  tensorProductIsBinaryProduct X
    Y :=
    BinaryFan.IsLimit.mk _ (lift (C := C)) (lift_fst (C := C)) (lift_snd (C := C))
      (by rintro T f g m rfl rfl; symm; exact lift_comp_fst_snd _)
  fst_def X Y := fst_def X.1 Y.1
  snd_def X Y := snd_def X.1 Y.1
Похожие утверждения