English
There is a canonical inclusion ι_S from the fiber F.obj ⟨op S⟩ into the Grothendieck construction ∫ᶜ F, mapping an object to its base and fiber components and sending a morphism to a pair consisting of the identity on the base and a fiber morphism adjusted by F-map and inverse of mapId.
Русский
Существует каноническое включение ι_S из пространства F.obj⟨op S⟩ в конструкцию Гротендд (∫ᶜ F), отправляющее объект в базовую и волоковую части и морфизм в пару, состоящую из тождества на базе и морфизма по волокну, упорядоченного через отображение F и обратное к mapId.
LaTeX
$$$\\iota_S : F.obj(⟨op S⟩) \\to ∫ᶜ F$, где obj и map заданы как в определении$$
Lean4
/-- The inclusion map from `F(S)` into `∫ᶜ F`. -/
@[simps]
def ι : F.obj ⟨op S⟩ ⥤ ∫ᶜ F where
obj a := { base := S, fiber := a }
map {a b} φ := { base := 𝟙 S, fiber := φ ≫ (F.mapId ⟨op S⟩).inv.app b }
map_comp {a b c} φ
ψ := by
ext
· simp
· simp [← (F.mapId ⟨op S⟩).inv.naturality_assoc ψ, F.whiskerRight_mapId_inv_app, Strict.leftUnitor_eqToIso]
