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.

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 : Finset M), (FirstOrder.Language.Substructure.closure L).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 ∧ (FirstOrder.Language.Substructure.closure L).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 n → M), (FirstOrder.Language.Substructure.closure L).toFun (Set.range s) = N

theorem FirstOrder.Language.Substructure.fg_bot {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :

⊥.FG

theorem FirstOrder.Language.Substructure.fg_closure {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {s : Set M} (hs : s.Finite) :

((FirstOrder.Language.Substructure.closure L).toFun s).FG

theorem FirstOrder.Language.Substructure.fg_closure_singleton {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (x : M) :

((FirstOrder.Language.Substructure.closure L).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) :

(FirstOrder.Language.Substructure.map f s).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 : (FirstOrder.Language.Substructure.map f.toHom s).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 ∧ (FirstOrder.Language.Substructure.closure L).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 ∧ (FirstOrder.Language.Substructure.closure L).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), (FirstOrder.Language.Substructure.closure L).toFun (Set.range s) = N

theorem FirstOrder.Language.Substructure.cg_bot {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :

⊥.CG

theorem FirstOrder.Language.Substructure.cg_closure {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {s : Set M} (hs : s.Countable) :

((FirstOrder.Language.Substructure.closure L).toFun s).CG

theorem FirstOrder.Language.Substructure.cg_closure_singleton {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (x : M) :

((FirstOrder.Language.Substructure.closure L).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) :

(FirstOrder.Language.Substructure.map f s).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 : (FirstOrder.Language.Substructure.map f.toHom s).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 ↔ Countable ↥s

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.

out : ⊤.FG

Instances

theorem FirstOrder.Language.Structure.FG.out {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [self : FirstOrder.Language.Structure.FG L M] :

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

out : ⊤.CG

Instances

theorem FirstOrder.Language.Structure.CG.out {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [self : FirstOrder.Language.Structure.CG L M] :

⊤.CG

theorem FirstOrder.Language.Structure.fg_def {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :

FirstOrder.Language.Structure.FG L M ↔ ⊤.FG

theorem FirstOrder.Language.Structure.fg_iff {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :

FirstOrder.Language.Structure.FG L M ↔ ∃ (S : Set M), S.Finite ∧ (FirstOrder.Language.Substructure.closure L).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 : FirstOrder.Language.Structure.FG L M) (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 : FirstOrder.Language.Structure.FG L M) (f : L.Hom M N) (hs : Function.Surjective ⇑f) :

FirstOrder.Language.Structure.FG L N

theorem FirstOrder.Language.Structure.cg_def {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :

FirstOrder.Language.Structure.CG L M ↔ ⊤.CG

theorem FirstOrder.Language.Structure.cg_iff {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :

FirstOrder.Language.Structure.CG L M ↔ ∃ (S : Set M), S.Countable ∧ (FirstOrder.Language.Substructure.closure L).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 : FirstOrder.Language.Structure.CG L M) (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 : FirstOrder.Language.Structure.CG L M) (f : L.Hom M N) (hs : Function.Surjective ⇑f) :

FirstOrder.Language.Structure.CG L N

theorem FirstOrder.Language.Structure.cg_iff_countable {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [Countable ((l : ℕ) × L.Functions l)] :

FirstOrder.Language.Structure.CG L M ↔ Countable M

theorem FirstOrder.Language.Structure.FG.cg {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (h : FirstOrder.Language.Structure.FG L M) :

FirstOrder.Language.Structure.CG L M

@[instance 100]

instance FirstOrder.Language.Structure.cg_of_fg {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [h : FirstOrder.Language.Structure.FG L M] :

FirstOrder.Language.Structure.CG L M

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) :

FirstOrder.Language.Structure.FG L M ↔ FirstOrder.Language.Structure.FG L 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 ↔ FirstOrder.Language.Structure.FG L ↥S

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) :

FirstOrder.Language.Structure.CG L M ↔ FirstOrder.Language.Structure.CG L 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 ↔ FirstOrder.Language.Structure.CG L ↥S