English
The range of the lift-inclusion map equals the supremum of all substructures S_i.
Русский
Образ отображения lifts-inclusion равен верхней границе (объединению) всех S_i.
LaTeX
$$$(\mathrm{liftInclusion}\,S)\mathrm{.toHom}.\mathrm{range} = \bigvee_i S_i.$$$
Lean4
/-- The direct limit of countably many countably generated structures is countably generated. -/
theorem cg {ι : Type*} [Countable ι] [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι] {G : ι → Type w}
[∀ i, L.Structure (G i)] (f : ∀ i j, i ≤ j → G i ↪[L] G j) (h : ∀ i, Structure.CG L (G i))
[DirectedSystem G fun i j h => f i j h] : Structure.CG L (DirectLimit G f) :=
by
refine ⟨⟨⋃ i, DirectLimit.of L ι G f i '' Classical.choose (h i).out, ?_, ?_⟩⟩
· exact Set.countable_iUnion fun i => Set.Countable.image (Classical.choose_spec (h i).out).1 _
· rw [eq_top_iff, Substructure.closure_iUnion]
simp_rw [← Embedding.coe_toHom, Substructure.closure_image]
rw [le_iSup_iff]
intro S hS x _
let out := Quotient.out (s := DirectLimit.setoid G f)
refine hS (out x).1 ⟨(out x).2, ?_, ?_⟩
· rw [(Classical.choose_spec (h (out x).1).out).2]
trivial
· simp only [out, Embedding.coe_toHom, DirectLimit.of_apply, Sigma.eta, Quotient.out_eq]
