of_map_embedding — Mathlib

English

If a finitely generated substructure maps under an embedding, the image is CG, hence the domain is CG as well.

Русский

Если образ конечнопорождаемой подструктуры по вложению CG, значит и исходная CG.

LaTeX

$$$f: M \to N, s.CG \Rightarrow (s.map f).CG$$$

Lean4

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

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