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} [FirstOrder.Language.Structure L M] (N : FirstOrder.Language.Substructure L M) : Prop

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

Equations

• FirstOrder.Language.Substructure.FG N = ∃ (S : Finset M), (FirstOrder.Language.Substructure.closure L).toFun ↑S = N

theorem FirstOrder.Language.Substructure.fg_def {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {N : FirstOrder.Language.Substructure L M} : FirstOrder.Language.Substructure.FG N ↔ ∃ (S : Set M), Set.Finite S ∧ (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} [FirstOrder.Language.Structure L M] {N : FirstOrder.Language.Substructure L M} : FirstOrder.Language.Substructure.FG N ↔ ∃ (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} [FirstOrder.Language.Structure L M] : FirstOrder.Language.Substructure.FG ⊥

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

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

theorem FirstOrder.Language.Substructure.FG.sup {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {N₁ : FirstOrder.Language.Substructure L M} {N₂ : FirstOrder.Language.Substructure L M} (hN₁ : FirstOrder.Language.Substructure.FG N₁) (hN₂ : FirstOrder.Language.Substructure.FG N₂) : FirstOrder.Language.Substructure.FG (N₁ ⊔ N₂)

theorem FirstOrder.Language.Substructure.FG.map {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {N : Type u_2} [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) {s : FirstOrder.Language.Substructure L M} (hs : FirstOrder.Language.Substructure.FG s) : FirstOrder.Language.Substructure.FG (FirstOrder.Language.Substructure.map f s)

theorem FirstOrder.Language.Substructure.FG.of_map_embedding {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {N : Type u_2} [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Embedding L M N) {s : FirstOrder.Language.Substructure L M} (hs : FirstOrder.Language.Substructure.FG (FirstOrder.Language.Substructure.map (FirstOrder.Language.Embedding.toHom f) s)) : FirstOrder.Language.Substructure.FG s

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

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

Equations

• FirstOrder.Language.Substructure.CG N = ∃ (S : Set M), Set.Countable S ∧ (FirstOrder.Language.Substructure.closure L).toFun S = N

theorem FirstOrder.Language.Substructure.cg_def {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {N : FirstOrder.Language.Substructure L M} : FirstOrder.Language.Substructure.CG N ↔ ∃ (S : Set M), Set.Countable S ∧ (FirstOrder.Language.Substructure.closure L).toFun S = N

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

theorem FirstOrder.Language.Substructure.cg_iff_empty_or_exists_nat_generating_family {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {N : FirstOrder.Language.Substructure L M} : FirstOrder.Language.Substructure.CG N ↔ ↑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} [FirstOrder.Language.Structure L M] : FirstOrder.Language.Substructure.CG ⊥

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

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

theorem FirstOrder.Language.Substructure.CG.sup {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {N₁ : FirstOrder.Language.Substructure L M} {N₂ : FirstOrder.Language.Substructure L M} (hN₁ : FirstOrder.Language.Substructure.CG N₁) (hN₂ : FirstOrder.Language.Substructure.CG N₂) : FirstOrder.Language.Substructure.CG (N₁ ⊔ N₂)

theorem FirstOrder.Language.Substructure.CG.map {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {N : Type u_2} [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Hom L M N) {s : FirstOrder.Language.Substructure L M} (hs : FirstOrder.Language.Substructure.CG s) : FirstOrder.Language.Substructure.CG (FirstOrder.Language.Substructure.map f s)

theorem FirstOrder.Language.Substructure.CG.of_map_embedding {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {N : Type u_2} [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Embedding L M N) {s : FirstOrder.Language.Substructure L M} (hs : FirstOrder.Language.Substructure.CG (FirstOrder.Language.Substructure.map (FirstOrder.Language.Embedding.toHom f) s)) : FirstOrder.Language.Substructure.CG s

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

class FirstOrder.Language.Structure.FG (L : FirstOrder.Language) (M : Type u_1) [FirstOrder.Language.Structure L M] : Prop

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

• out : FirstOrder.Language.Substructure.FG ⊤

class FirstOrder.Language.Structure.CG (L : FirstOrder.Language) (M : Type u_1) [FirstOrder.Language.Structure L M] : Prop

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

• out : FirstOrder.Language.Substructure.CG ⊤

theorem FirstOrder.Language.Structure.fg_def {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] : FirstOrder.Language.Structure.FG L M ↔ FirstOrder.Language.Substructure.FG ⊤

theorem FirstOrder.Language.Structure.fg_iff {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] : FirstOrder.Language.Structure.FG L M ↔ ∃ (S : Set M), Set.Finite S ∧ (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} [FirstOrder.Language.Structure L M] {N : Type u_2} [FirstOrder.Language.Structure L N] (h : FirstOrder.Language.Structure.FG L M) (f : FirstOrder.Language.Hom L M N) : FirstOrder.Language.Substructure.FG (FirstOrder.Language.Hom.range f)

theorem FirstOrder.Language.Structure.FG.map_of_surjective {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {N : Type u_2} [FirstOrder.Language.Structure L N] (h : FirstOrder.Language.Structure.FG L M) (f : FirstOrder.Language.Hom L 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} [FirstOrder.Language.Structure L M] : FirstOrder.Language.Structure.CG L M ↔ FirstOrder.Language.Substructure.CG ⊤

theorem FirstOrder.Language.Structure.cg_iff {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] : FirstOrder.Language.Structure.CG L M ↔ ∃ (S : Set M), Set.Countable S ∧ (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} [FirstOrder.Language.Structure L M] {N : Type u_2} [FirstOrder.Language.Structure L N] (h : FirstOrder.Language.Structure.CG L M) (f : FirstOrder.Language.Hom L M N) : FirstOrder.Language.Substructure.CG (FirstOrder.Language.Hom.range f)

theorem FirstOrder.Language.Structure.CG.map_of_surjective {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {N : Type u_2} [FirstOrder.Language.Structure L N] (h : FirstOrder.Language.Structure.CG L M) (f : FirstOrder.Language.Hom L 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} [FirstOrder.Language.Structure L 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} [FirstOrder.Language.Structure L M] (h : FirstOrder.Language.Structure.FG L M) : FirstOrder.Language.Structure.CG L M

instance FirstOrder.Language.Structure.cg_of_fg {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L 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} [FirstOrder.Language.Structure L M] {N : Type u_2} [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Equiv L 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} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) : FirstOrder.Language.Substructure.FG S ↔ FirstOrder.Language.Structure.FG L ↥S

theorem FirstOrder.Language.Equiv.cg_iff {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {N : Type u_2} [FirstOrder.Language.Structure L N] (f : FirstOrder.Language.Equiv L 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} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) : FirstOrder.Language.Substructure.CG S ↔ FirstOrder.Language.Structure.CG L ↥S