English
There is a natural equivalence between transporting along F and then forgetting the enrichment, versus forgetting first and then transporting, under appropriate hypotheses on F and the enrichment data.
Русский
Существует естественная эквивалентность между транспортировкой вдоль F с забыванием обогащения и между забыванием и последующим транспортированием при подходящих условиях на F и данные обогащения.
LaTeX
$$$ \\mathrm{forgetEnrichmentEquiv} : \\mathrm{TransportEnrichment}\\ F\\ (\\mathrm{ForgetEnrichment}\\ V\\ D) \\simeq \\mathrm{ForgetEnrichment}\\ W\\ (\\mathrm{TransportEnrichment}\\ F\\ D). $$$
Lean4
/-- If `D` is a `V`-enriched category, then forgetting the enrichment and transporting the resulting
enriched ordinary category along a functor `F : V ⥤ W`, for which
`f ↦ Functor.LaxMonoidal.ε F ≫ F.map f` has an inverse, results in a category equivalent to
transporting along `F` and then forgetting about the resulting `W`-enrichment. -/
@[simps]
def forgetEnrichmentEquiv : TransportEnrichment F (ForgetEnrichment V D) ≌ ForgetEnrichment W (TransportEnrichment F D)
where
functor := forgetEnrichmentEquivFunctor _ _ e h
inverse := forgetEnrichmentEquivInverse _ _ e h
unitIso := NatIso.ofComponents (fun _ => Iso.refl _) (by simp)
counitIso := NatIso.ofComponents (fun _ => Iso.refl _) fun f => by simp [ForgetEnrichment.to, ForgetEnrichment.of]
functor_unitIso_comp
X :=
by
simp only [Functor.id_obj, forgetEnrichmentEquivFunctor_obj, Functor.comp_obj, forgetEnrichmentEquivInverse_obj,
ForgetEnrichment.to_of, NatIso.ofComponents_hom_app, Iso.refl_hom, forgetEnrichmentEquivFunctor_map, h,
Category.comp_id]
rw [← ForgetEnrichment.homOf_eId, TransportEnrichment.eId_eq, ForgetEnrichment.homTo_id]
rfl
