fg_iff_structure_fg — Mathlib

English

For S a substructure, its CG property is equivalent to the CG of the induced L-structure on S.

Русский

Для подструктуры S эквивалентно cg для индукционированной структуры L на S.

LaTeX

$$$$ S.CG \\Leftrightarrow Structure.CG\\; L\\; S. $$$$

Lean4

theorem fg_iff_structure_fg (S : L.Substructure M) : S.FG ↔ Structure.FG L S :=
  by
  rw [Structure.fg_def]
  refine ⟨fun h => FG.of_map_embedding S.subtype ?_, fun h => ?_⟩
  · rw [← Hom.range_eq_map, range_subtype]
    exact h
  · have h := h.map S.subtype.toHom
    rw [← Hom.range_eq_map, range_subtype] at h
    exact h

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