English
There is an inverse equivalence to forgetting enrichment after transporting along F, providing a two-sided adjoint-like correspondence between ForgetEnrichment and TransportEnrichment along F, realized via a specified Equiv e and its inverse.
Русский
Существует обратная эквивалентность забывания обогащения после переноса вдоль F, дающая двустороннюю связь между ForgetEnrichment и TransportEnrichment вдоль F, реализованная через заданное эквивалентное отображение e и его обратное.
LaTeX
$$$ \\text{forgetEnrichmentEquivInverse}_{F,D} : \\mathrm{ForgetEnrichment}\\ W\\ (\\mathrm{TransportEnrichment}\\ F\\ D) \\simeq \\mathrm{TransportEnrichment}\\ F\\ (\\mathrm{ForgetEnrichment}\\ V\\ D). $$$
Lean4
/-- The inverse functor that makes up `TransportEnrichment.forgetEnrichmentEquiv`. -/
@[simps]
def forgetEnrichmentEquivInverse :
ForgetEnrichment W (TransportEnrichment F D) ⥤ TransportEnrichment F (ForgetEnrichment V D)
where
obj X := ForgetEnrichment.of V (ForgetEnrichment.to (C := TransportEnrichment F D) W X)
map f := ForgetEnrichment.homOf V ((e _).symm (ForgetEnrichment.homTo W f))
map_id
X := by
rw [← ForgetEnrichment.homOf_eId]
congr 1
apply Equiv.injective (e _)
rw [ForgetEnrichment.homTo_id, Equiv.apply_symm_apply, h, TransportEnrichment.eId_eq]
map_comp f
g := by
rw [← ForgetEnrichment.homOf_comp]
congr
apply Equiv.injective (e _)
rw [Equiv.apply_symm_apply, h]
simp only [ForgetEnrichment.homTo_comp, eComp_eq, Category.assoc, Functor.map_comp]
slice_rhs 1 3 =>
rw [← Functor.LaxMonoidal.left_unitality_inv, Category.assoc, Category.assoc, ← Functor.LaxMonoidal.μ_natural, ←
leftUnitor_inv_comp_tensorHom_assoc, tensorHom_comp_tensorHom_assoc]
simp [← h]
