# Documentation

Mathlib.ModelTheory.FinitelyGenerated

# Finitely Generated First-Order Structures #

This file defines what it means for a first-order (sub)structure to be finitely or countably generated, similarly to other finitely-generated objects in the algebra library.

## Main Definitions #

• FirstOrder.Language.Substructure.FG indicates that a substructure is finitely generated.
• FirstOrder.Language.Structure.FG indicates that a structure is finitely generated.
• FirstOrder.Language.Substructure.CG indicates that a substructure is countably generated.
• FirstOrder.Language.Structure.CG indicates that a structure is countably generated.

## TODO #

Develop a more unified definition of finite generation using the theory of closure operators, or use this definition of finite generation to define the others.

A substructure of M is finitely generated if it is the closure of a finite subset of M.

Instances For
theorem FirstOrder.Language.Substructure.FG.sup {L : FirstOrder.Language} {M : Type u_1} {N₁ : } {N₂ : } (hN₁ : ) (hN₂ : ) :
theorem FirstOrder.Language.Substructure.FG.map {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (f : ) {s : } :

A substructure of M is countably generated if it is the closure of a countable subset of M.

Instances For
theorem FirstOrder.Language.Substructure.CG.sup {L : FirstOrder.Language} {M : Type u_1} {N₁ : } {N₂ : } (hN₁ : ) (hN₂ : ) :
theorem FirstOrder.Language.Substructure.CG.map {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (f : ) {s : } :

A structure is finitely generated if it is the closure of a finite subset.

Instances

A structure is countably generated if it is the closure of a countable subset.

Instances

An equivalent expression of Structure.FG in terms of Set.Finite instead of Finset.

theorem FirstOrder.Language.Structure.FG.range {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (h : ) (f : ) :
theorem FirstOrder.Language.Structure.FG.map_of_surjective {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (h : ) (f : ) (hs : ) :

An equivalent expression of Structure.cg.

theorem FirstOrder.Language.Structure.CG.range {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (h : ) (f : ) :
theorem FirstOrder.Language.Structure.CG.map_of_surjective {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (h : ) (f : ) (hs : ) :
theorem FirstOrder.Language.Equiv.fg_iff {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (f : ) :
theorem FirstOrder.Language.Equiv.cg_iff {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} (f : ) :