of_map_embedding — Mathlib

English

If there is a finite (substructure) witness for a finite-type substructure, then it is finitely generated.

Русский

Если имеется конечная подпорная структура в качестве свидетельства, то она конечнопорождаема.

LaTeX

$$$\text{Finite} (\text{Subtype fun x => mem s x}) \Rightarrow s.FG$$$

Lean4

theorem of_map_embedding {N : Type*} [L.Structure N] (f : M ↪[L] N) {s : L.Substructure M} (hs : (s.map f.toHom).FG) :
    s.FG := by
  rcases hs with ⟨t, h⟩
  rw [fg_def]
  refine ⟨f ⁻¹' t, t.finite_toSet.preimage f.injective.injOn, ?_⟩
  have hf : Function.Injective f.toHom := f.injective
  refine map_injective_of_injective hf ?_
  rw [← h, map_closure, Embedding.coe_toHom, image_preimage_eq_of_subset]
  intro x hx
  have h' := subset_closure (L := L) hx
  rw [h] at h'
  exact Hom.map_le_range h'

Похожие утверждения