English
The embedding of a component-level element x into the direct limit corresponds to the canonical quotient embedding.
Русский
Встраивание элемента x из компоненты в прямой предел соответствует каноническому вложению в фактор-множество.
LaTeX
$$$\\mathrm{of}_L(i)(x) = \\langle i,x\\rangle$$$
Lean4
/-- The canonical map from a component to the direct limit. -/
noncomputable def of (i : ι) : G i ↪[L] DirectLimit G f
where
toFun := fun a => ⟦.mk f i a⟧
inj' x y
h := by
rw [Quotient.eq] at h
obtain ⟨j, h1, _, h3⟩ := h
exact (f i j h1).injective h3
map_fun' F
x := by
rw [← funMap_quotient_mk'_sigma_mk']
rfl
map_rel' := by
intro n R x
change RelMap R (fun a => (⟦.mk f i (x a)⟧ : DirectLimit G f)) ↔ _
simp only [relMap_quotient_mk'_sigma_mk']
