Lean4
/-- Given a reflective subcategory `D` of a category with chosen finite products `C`, `D` admits
finite chosen products. -/
-- Note: This is not an instance as one might already have a (different) `CartesianMonoidalCategory`
-- instance on `D` (as for example with sheaves).
-- See note [reducible non-instances]
abbrev ofReflective [CartesianMonoidalCategory C] [Reflective i] : CartesianMonoidalCategory D :=
.ofChosenFiniteProducts
({
cone := Limits.asEmptyCone <| (reflector i).obj (𝟙_ C)
isLimit := by
apply isLimitOfReflects i
apply isLimitChangeEmptyCone _ isTerminalTensorUnit
letI : IsIso ((reflectorAdjunction i).unit.app (𝟙_ C)) :=
by
have := reflective_products i
refine Functor.essImage.unit_isIso ⟨terminal D, ⟨PreservesTerminal.iso i |>.trans ?_⟩⟩
exact IsLimit.conePointUniqueUpToIso (limit.isLimit _) isTerminalTensorUnit
exact asIso ((reflectorAdjunction i).unit.app (𝟙_ C)) })
fun X Y ↦
{ cone :=
BinaryFan.mk ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app _)
((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app _)
isLimit := by
apply isLimitOfReflects i
apply
IsLimit.equivOfNatIsoOfIso (pairComp X Y _) _ _ _ |>.invFun (tensorProductIsBinaryProduct (i.obj X) (i.obj Y))
fapply BinaryFan.ext
· change (reflector i ⋙ i).obj (i.obj X ⊗ i.obj Y) ≅ (𝟭 C).obj (i.obj X ⊗ i.obj Y)
letI : IsIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y)) :=
by
apply Functor.essImage.unit_isIso
haveI := reflective_products i
use Limits.prod X Y
constructor
apply Limits.PreservesLimitPair.iso i _ _ |>.trans
refine
Limits.IsLimit.conePointUniqueUpToIso (limit.isLimit (pair (i.obj X) (i.obj Y)))
(tensorProductIsBinaryProduct _ _)
exact asIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y)) |>.symm
· simp only [BinaryFan.fst, Cones.postcompose, pairComp]
simp [← Functor.comp_map, ← NatTrans.naturality_assoc]
· simp only [BinaryFan.snd, Cones.postcompose, pairComp]
simp [← Functor.comp_map, ← NatTrans.naturality_assoc] }
