English
Compatibility of ι on tensor homs in the lawful Day convolution setup.
Русский
Совместимость ι на тензор-гомах в корректной Day-конволюционной настройке.
LaTeX
$$$ (ι C V D).map (f \otimes_ m f') = DayConvolution.map ((ι C V D).map f) ((ι C V D).map f') $$$
Lean4
/-- We can promote a `LawfulDayConvolutionMonoidalCategoryStruct` to a monoidal category,
note that every non-prop data is already here, so this is just about showing that they
satisfy the axioms of a monoidal category. -/
def monoidalOfLawfulDayConvolutionMonoidalCategoryStruct (D : Type u₃) [Category.{v₃} D] [MonoidalCategoryStruct D]
[LawfulDayConvolutionMonoidalCategoryStruct C V D]
[∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)]
[∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)]
[∀ (v : V) (d : C),
Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit.{0} <| 𝟙_ C) d) (tensorLeft v)]
[∀ (v : V) (d : C),
Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit.{0} <| 𝟙_ C) d) (tensorRight v)]
[∀ (v : V) (d : C × C),
Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod <| Functor.fromPUnit.{0} <| 𝟙_ C) d)
(tensorRight v)]
[∀ (v : V) (d : C × C),
Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)] :
MonoidalCategory D :=
MonoidalCategory.ofTensorHom (id_tensorHom_id := fun x y =>
by
apply Functor.Faithful.map_injective (F := ι C V D)
simp only [ι_map_tensorHom_hom_eq_tensorHom, Functor.map_id]
apply (DayConvolution.corepresentableBy (ι C V D |>.obj _) (ι C V D |>.obj _)).homEquiv.injective
dsimp
ext ⟨_, _⟩
simp only [externalProductBifunctor_obj_obj, Functor.comp_obj, tensor_obj, corepresentableBy_homEquiv_apply_app,
unit_app_map_app, NatTrans.id_app, tensorHom_id, id_whiskerRight, Category.id_comp]
dsimp [DayConvolution.convolution]
simp) (tensorHom_comp_tensorHom := fun _ _ _ _ =>
by
apply Functor.Faithful.map_injective (F := ι C V D)
simp only [ι_map_tensorHom_hom_eq_tensorHom, Functor.map_comp]
apply (corepresentableBy (ι C V D |>.obj _) (ι C V D |>.obj _)).homEquiv.injective
dsimp
ext ⟨_, _⟩
simp) (id_tensorHom := fun x {y₁ y₂} f =>
by
apply Functor.Faithful.map_injective (F := ι C V D)
simp only [ι_map_tensorHom_hom_eq_tensorHom]
apply (corepresentableBy (ι C V D |>.obj _) (ι C V D |>.obj _)).homEquiv.injective
dsimp
ext ⟨x, y⟩
dsimp
simp only [Functor.map_id, unit_app_map_app, Functor.comp_obj, tensor_obj, NatTrans.id_app, id_tensorHom]
dsimp [unit]
rw [convolutionExtensionUnit_comp_ι_map_whiskerLeft_app]) (tensorHom_id := fun x {y₁ y₂} f =>
by
apply Functor.Faithful.map_injective (F := ι C V D)
simp only [ι_map_tensorHom_hom_eq_tensorHom]
apply (corepresentableBy (ι C V D |>.obj _) (ι C V D |>.obj _)).homEquiv.injective
dsimp
ext ⟨x, y⟩
dsimp
simp only [Functor.map_id, DayConvolution.unit_app_map_app, Functor.comp_obj, tensor_obj, NatTrans.id_app,
tensorHom_id]
dsimp [DayConvolution.unit]
rw [convolutionExtensionUnit_comp_ι_map_whiskerRight_app]) (associator_naturality := fun f₁ f₂ f₃ =>
by
apply Functor.Faithful.map_injective (F := ι C V D)
simp only [Functor.map_comp, ι_map_associator_hom_eq_associator_hom, ι_map_tensorHom_hom_eq_tensorHom]
exact DayConvolution.associator_naturality ((ι C V D).map f₁) ((ι C V D).map f₂) ((ι C V D).map f₃))
(leftUnitor_naturality := fun f =>
by
apply Functor.Faithful.map_injective (F := ι C V D)
simp only [Functor.map_comp, ι_map_tensorHom_hom_eq_tensorHom, Functor.map_id]
rw [ι_map_leftUnitor_hom_eq_leftUnitor_hom, ι_map_leftUnitor_hom_eq_leftUnitor_hom]
exact DayConvolutionUnit.leftUnitor_naturality (ι C V D |>.obj <| 𝟙_ D) (ι C V D |>.map f))
(rightUnitor_naturality := fun f =>
by
apply Functor.Faithful.map_injective (F := ι C V D)
simp only [Functor.map_comp, ι_map_tensorHom_hom_eq_tensorHom, Functor.map_id]
rw [ι_map_rightUnitor_hom_eq_rightUnitor_hom, ι_map_rightUnitor_hom_eq_rightUnitor_hom]
exact DayConvolutionUnit.rightUnitor_naturality (ι C V D |>.obj <| 𝟙_ D) (ι C V D |>.map f)) (pentagon :=
fun a b c d => by
apply Functor.Faithful.map_injective (F := ι C V D)
simp only [Functor.map_comp, Functor.map_id, ι_map_tensorHom_hom_eq_tensorHom,
ι_map_associator_hom_eq_associator_hom]
-- this is a bit painful...
letI : DayConvolution (((ι C V D |>.obj a) ⊛ (ι C V D |>.obj b)) ⊛ (ι C V D |>.obj c)) (ι C V D |>.obj d) :=
convolution C V D _ _
letI : DayConvolution ((ι C V D |>.obj a) ⊛ (ι C V D |>.obj b)) ((ι C V D |>.obj c) ⊛ (ι C V D |>.obj d)) :=
convolution C V D _ _
letI : DayConvolution ((ι C V D |>.obj a) ⊛ ((ι C V D |>.obj b) ⊛ (ι C V D |>.obj c))) (ι C V D |>.obj d) :=
convolution C V D _ _
letI : DayConvolution (ι C V D |>.obj a) ((ι C V D |>.obj b) ⊛ ((ι C V D |>.obj c) ⊛ (ι C V D |>.obj d))) :=
convolution C V D _ _
letI : DayConvolution (ι C V D |>.obj a) (((ι C V D |>.obj b) ⊛ (ι C V D |>.obj c)) ⊛ (ι C V D |>.obj d)) :=
convolution C V D _ _
exact DayConvolution.pentagon (ι C V D |>.obj a) (ι C V D |>.obj b) (ι C V D |>.obj c) (ι C V D |>.obj d))
(triangle := fun a b => by
apply Functor.Faithful.map_injective (F := ι C V D)
simp only [Functor.map_comp, Functor.map_id, ι_map_tensorHom_hom_eq_tensorHom,
ι_map_associator_hom_eq_associator_hom, ι_map_leftUnitor_hom_eq_leftUnitor_hom,
ι_map_rightUnitor_hom_eq_rightUnitor_hom]
exact DayConvolution.triangle (ι C V D |>.obj a) (ι C V D |>.obj b) (ι C V D |>.obj <| 𝟙_ D))
