# 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.

def FirstOrder.Language.Substructure.FG {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (N : L.Substructure M) :

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

Equations
• N.FG = ∃ (S : ), .toFun S = N
Instances For
theorem FirstOrder.Language.Substructure.fg_def {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N : L.Substructure M} :
N.FG ∃ (S : Set M), S.Finite .toFun S = N
theorem FirstOrder.Language.Substructure.fg_iff_exists_fin_generating_family {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N : L.Substructure M} :
N.FG ∃ (n : ) (s : Fin nM), .toFun () = N
theorem FirstOrder.Language.Substructure.fg_closure {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {s : Set M} (hs : s.Finite) :
(.toFun s).FG
theorem FirstOrder.Language.Substructure.fg_closure_singleton {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (x : M) :
(.toFun {x}).FG
theorem FirstOrder.Language.Substructure.FG.sup {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N₁ : L.Substructure M} {N₂ : L.Substructure M} (hN₁ : N₁.FG) (hN₂ : N₂.FG) :
(N₁ N₂).FG
theorem FirstOrder.Language.Substructure.FG.map {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] (f : L.Hom M N) {s : L.Substructure M} (hs : s.FG) :
.FG
theorem FirstOrder.Language.Substructure.FG.of_map_embedding {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] (f : L.Embedding M N) {s : L.Substructure M} (hs : ().FG) :
s.FG
def FirstOrder.Language.Substructure.CG {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (N : L.Substructure M) :

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

Equations
• N.CG = ∃ (S : Set M), S.Countable .toFun S = N
Instances For
theorem FirstOrder.Language.Substructure.cg_def {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N : L.Substructure M} :
N.CG ∃ (S : Set M), S.Countable .toFun S = N
theorem FirstOrder.Language.Substructure.FG.cg {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N : L.Substructure M} (h : N.FG) :
N.CG
theorem FirstOrder.Language.Substructure.cg_iff_empty_or_exists_nat_generating_family {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N : L.Substructure M} :
N.CG N = ∃ (s : M), .toFun () = N
theorem FirstOrder.Language.Substructure.cg_closure {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {s : Set M} (hs : s.Countable) :
(.toFun s).CG
theorem FirstOrder.Language.Substructure.cg_closure_singleton {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (x : M) :
(.toFun {x}).CG
theorem FirstOrder.Language.Substructure.CG.sup {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N₁ : L.Substructure M} {N₂ : L.Substructure M} (hN₁ : N₁.CG) (hN₂ : N₂.CG) :
(N₁ N₂).CG
theorem FirstOrder.Language.Substructure.CG.map {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] (f : L.Hom M N) {s : L.Substructure M} (hs : s.CG) :
.CG
theorem FirstOrder.Language.Substructure.CG.of_map_embedding {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] (f : L.Embedding M N) {s : L.Substructure M} (hs : ().CG) :
s.CG
theorem FirstOrder.Language.Substructure.cg_iff_countable {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [Countable ((l : ) × L.Functions l)] {s : L.Substructure M} :
s.CG
class FirstOrder.Language.Structure.FG (L : FirstOrder.Language) (M : Type u_1) [L.Structure M] :

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

Instances
theorem FirstOrder.Language.Structure.FG.out {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [self : ] :
.FG
class FirstOrder.Language.Structure.CG (L : FirstOrder.Language) (M : Type u_1) [L.Structure M] :

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

Instances
theorem FirstOrder.Language.Structure.CG.out {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [self : ] :
.CG
theorem FirstOrder.Language.Structure.fg_def {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :
theorem FirstOrder.Language.Structure.fg_iff {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :
∃ (S : Set M), S.Finite .toFun S =

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} [L.Structure M] {N : Type u_2} [L.Structure N] (h : ) (f : L.Hom M N) :
f.range.FG
theorem FirstOrder.Language.Structure.FG.map_of_surjective {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] (h : ) (f : L.Hom M N) (hs : ) :
theorem FirstOrder.Language.Structure.cg_def {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :
theorem FirstOrder.Language.Structure.cg_iff {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :
∃ (S : Set M), S.Countable .toFun S =

An equivalent expression of Structure.cg.

theorem FirstOrder.Language.Structure.CG.range {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] (h : ) (f : L.Hom M N) :
f.range.CG
theorem FirstOrder.Language.Structure.CG.map_of_surjective {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] (h : ) (f : L.Hom M N) (hs : ) :
theorem FirstOrder.Language.Structure.cg_iff_countable {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [Countable ((l : ) × L.Functions l)] :
theorem FirstOrder.Language.Structure.FG.cg {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (h : ) :
@[instance 100]
instance FirstOrder.Language.Structure.cg_of_fg {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [h : ] :
Equations
• =
theorem FirstOrder.Language.Equiv.fg_iff {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] (f : L.Equiv M N) :
theorem FirstOrder.Language.Substructure.fg_iff_structure_fg {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (S : L.Substructure M) :
S.FG
theorem FirstOrder.Language.Equiv.cg_iff {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] (f : L.Equiv M N) :
theorem FirstOrder.Language.Substructure.cg_iff_structure_cg {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (S : L.Substructure M) :
S.CG