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

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

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

instance FirstOrder.Language.Substructure.instInhabited_fg {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] : Inhabited { S : L.Substructure M // S.FG }

Equations

• FirstOrder.Language.Substructure.instInhabited_fg = { default := ⟨⊥, ⋯⟩ }

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

theorem FirstOrder.Language.Substructure.FG.of_finite {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {s : L.Substructure M} [h : Finite ↥s] : s.FG

theorem FirstOrder.Language.Substructure.FG.finite {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [L.IsRelational] {S : L.Substructure M} (h : S.FG) : Finite ↥S

theorem FirstOrder.Language.Substructure.fg_iff_finite {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [L.IsRelational] {S : L.Substructure M} : S.FG ↔ Finite ↥S

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

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

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

theorem FirstOrder.Language.Substructure.cg_of_countable {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {s : L.Substructure M} [h : Countable ↥s] : s.CG

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

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

• out : ⊤.FG

theorem FirstOrder.Language.Structure.FG.out {L : FirstOrder.Language} {M : Type u_1} : ∀ {inst : 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] : Prop

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

• out : ⊤.CG

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

instance FirstOrder.Language.Structure.FG.instCountable_hom {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (N : Type u_2) [L.Structure N] [Countable N] [h : FirstOrder.Language.Structure.FG L M] : Countable (L.Hom M N)

Equations

• ⋯ = ⋯

theorem FirstOrder.Language.Structure.FG.countable_embedding {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (N : Type u_2) [L.Structure N] [Countable N] : FirstOrder.Language.Structure.FG L M → Countable (L.Embedding M N)

instance FirstOrder.Language.Structure.Fg.instCountable_embedding {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (N : Type u_2) [L.Structure N] [Countable N] [h : FirstOrder.Language.Structure.FG L M] : Countable (L.Embedding M N)

Equations

• ⋯ = ⋯

theorem FirstOrder.Language.Structure.FG.of_finite {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [Finite M] : FirstOrder.Language.Structure.FG L M

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

theorem FirstOrder.Language.Structure.fg_iff_finite {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [L.IsRelational] : FirstOrder.Language.Structure.FG L M ↔ Finite M

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.cg_of_countable {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [Countable M] : FirstOrder.Language.Structure.CG L 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

theorem FirstOrder.Language.Substructure.countable_fg_substructures_of_countable {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [Countable M] : Countable { S : L.Substructure M // S.FG }

instance FirstOrder.Language.Substructure.instCountable_fg_substructures_of_countable {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [Countable M] : Countable { S : L.Substructure M // S.FG }

Equations

• ⋯ = ⋯