English
If a V-enriched category D is transported along a lax monoidal functor F: V → W and then forgotten, this process is equivalent to first forgetting the enrichment and then transporting along F to obtain a W-enriched category; there is a canonical equivalence between these two pathways.
Русский
Если D — V-зреленная категория, транспортируемая вдоль слабомоноидного функторa F: V → W и затем забывается обогащение, то этот процесс эквивалентен сначала забыванию обогащения, а затем переносу через F, давая эквивалентность между двумя путями.
LaTeX
$$$ \\text{forgetEnrichmentEquiv}_{F,D} : \\mathrm{TransportEnrichment}\\ F\\ (\\mathrm{ForgetEnrichment}\\ V\\ D) \\simeq \\mathrm{ForgetEnrichment}\\ W\\ (\\mathrm{TransportEnrichment}\\ F\\ D). $$$
Lean4
/-- The functor that makes up `TransportEnrichment.forgetEnrichmentEquiv`. -/
@[simps]
def forgetEnrichmentEquivFunctor :
TransportEnrichment F (ForgetEnrichment V D) ⥤ ForgetEnrichment W (TransportEnrichment F D)
where
obj X := ForgetEnrichment.of W X
map {X} {Y} f := ForgetEnrichment.homOf W <| (e (Hom (C := ForgetEnrichment V D) X Y)) <| ForgetEnrichment.homTo V f
map_id
X := by
rw [h, ForgetEnrichment.homTo_id, ← TransportEnrichment.eId_eq]
simp [ForgetEnrichment.to]
map_comp f
g :=
by
rw [h, h, h, ForgetEnrichment.homTo_comp, F.map_comp, F.map_comp, ← Category.assoc, ←
Functor.LaxMonoidal.left_unitality_inv, Category.assoc, Category.assoc, Category.assoc, Category.assoc, ←
Functor.LaxMonoidal.μ_natural_assoc, ← TransportEnrichment.eComp_eq, ← ForgetEnrichment.homOf_comp,
leftUnitor_inv_naturality_assoc, ← tensorHom_def'_assoc, tensorHom_comp_tensorHom_assoc]
rfl
