Finitely Generated First-Order Structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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 #

first_order.language.substructure.fg indicates that a substructure is finitely generated.
first_order.language.Structure.fg indicates that a structure is finitely generated.
first_order.language.substructure.cg indicates that a substructure is countably generated.
first_order.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.

source

def first_order.language.substructure.fg {L : first_order.language} {M : Type u_3} [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), ⇑(first_order.language.substructure.closure L) ↑S = N

source

theorem first_order.language.substructure.fg_def {L : first_order.language} {M : Type u_3} [L.Structure M] {N : L.substructure M} :

N.fg ↔ ∃ (S : set M), S.finite ∧ ⇑(first_order.language.substructure.closure L) S = N

source

theorem first_order.language.substructure.fg_iff_exists_fin_generating_family {L : first_order.language} {M : Type u_3} [L.Structure M] {N : L.substructure M} :

N.fg ↔ ∃ (n : ℕ) (s : fin n → M), ⇑(first_order.language.substructure.closure L) (set.range s) = N

source

theorem first_order.language.substructure.fg_bot {L : first_order.language} {M : Type u_3} [L.Structure M] :

⊥.fg

source

theorem first_order.language.substructure.fg_closure {L : first_order.language} {M : Type u_3} [L.Structure M] {s : set M} (hs : s.finite) :

(⇑(first_order.language.substructure.closure L) s).fg

source

theorem first_order.language.substructure.fg_closure_singleton {L : first_order.language} {M : Type u_3} [L.Structure M] (x : M) :

(⇑(first_order.language.substructure.closure L) {x}).fg

source

theorem first_order.language.substructure.fg.sup {L : first_order.language} {M : Type u_3} [L.Structure M] {N₁ N₂ : L.substructure M} (hN₁ : N₁.fg) (hN₂ : N₂.fg) :

(N₁ ⊔ N₂).fg

source

theorem first_order.language.substructure.fg.map {L : first_order.language} {M : Type u_3} [L.Structure M] {N : Type u_4} [L.Structure N] (f : L.hom M N) {s : L.substructure M} (hs : s.fg) :

(first_order.language.substructure.map f s).fg

source

theorem first_order.language.substructure.fg.of_map_embedding {L : first_order.language} {M : Type u_3} [L.Structure M] {N : Type u_4} [L.Structure N] (f : L.embedding M N) {s : L.substructure M} (hs : (first_order.language.substructure.map f.to_hom s).fg) :

s.fg

source

def first_order.language.substructure.cg {L : first_order.language} {M : Type u_3} [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 ∧ ⇑(first_order.language.substructure.closure L) S = N

source

theorem first_order.language.substructure.cg_def {L : first_order.language} {M : Type u_3} [L.Structure M] {N : L.substructure M} :

N.cg ↔ ∃ (S : set M), S.countable ∧ ⇑(first_order.language.substructure.closure L) S = N

source

theorem first_order.language.substructure.fg.cg {L : first_order.language} {M : Type u_3} [L.Structure M] {N : L.substructure M} (h : N.fg) :

N.cg

source

theorem first_order.language.substructure.cg_iff_empty_or_exists_nat_generating_family {L : first_order.language} {M : Type u_3} [L.Structure M] {N : L.substructure M} :

N.cg ↔ ↑N = ∅ ∨ ∃ (s : ℕ → M), ⇑(first_order.language.substructure.closure L) (set.range s) = N

source

theorem first_order.language.substructure.cg_bot {L : first_order.language} {M : Type u_3} [L.Structure M] :

⊥.cg

source

theorem first_order.language.substructure.cg_closure {L : first_order.language} {M : Type u_3} [L.Structure M] {s : set M} (hs : s.countable) :

(⇑(first_order.language.substructure.closure L) s).cg

source

theorem first_order.language.substructure.cg_closure_singleton {L : first_order.language} {M : Type u_3} [L.Structure M] (x : M) :

(⇑(first_order.language.substructure.closure L) {x}).cg

source

theorem first_order.language.substructure.cg.sup {L : first_order.language} {M : Type u_3} [L.Structure M] {N₁ N₂ : L.substructure M} (hN₁ : N₁.cg) (hN₂ : N₂.cg) :

(N₁ ⊔ N₂).cg

source

theorem first_order.language.substructure.cg.map {L : first_order.language} {M : Type u_3} [L.Structure M] {N : Type u_4} [L.Structure N] (f : L.hom M N) {s : L.substructure M} (hs : s.cg) :

(first_order.language.substructure.map f s).cg

source

theorem first_order.language.substructure.cg.of_map_embedding {L : first_order.language} {M : Type u_3} [L.Structure M] {N : Type u_4} [L.Structure N] (f : L.embedding M N) {s : L.substructure M} (hs : (first_order.language.substructure.map f.to_hom s).cg) :

s.cg

source

theorem first_order.language.substructure.cg_iff_countable {L : first_order.language} {M : Type u_3} [L.Structure M] [countable (Σ (l : ℕ), L.functions l)] {s : L.substructure M} :

s.cg ↔ countable ↥s

source

@[class]

structure first_order.language.Structure.fg (L : first_order.language) (M : Type u_3) [L.Structure M] :

Prop

out : ⊤.fg

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

source

@[class]

structure first_order.language.Structure.cg (L : first_order.language) (M : Type u_3) [L.Structure M] :

Prop

out : ⊤.cg

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

Instances of this typeclass

source

theorem first_order.language.Structure.fg_def {L : first_order.language} {M : Type u_3} [L.Structure M] :

first_order.language.Structure.fg L M ↔ ⊤.fg

source

theorem first_order.language.Structure.fg_iff {L : first_order.language} {M : Type u_3} [L.Structure M] :

first_order.language.Structure.fg L M ↔ ∃ (S : set M), S.finite ∧ ⇑(first_order.language.substructure.closure L) S = ⊤

An equivalent expression of Structure.fg in terms of set.finite instead of finset.

source

theorem first_order.language.Structure.fg.range {L : first_order.language} {M : Type u_3} [L.Structure M] {N : Type u_4} [L.Structure N] (h : first_order.language.Structure.fg L M) (f : L.hom M N) :

f.range.fg

source

theorem first_order.language.Structure.fg.map_of_surjective {L : first_order.language} {M : Type u_3} [L.Structure M] {N : Type u_4} [L.Structure N] (h : first_order.language.Structure.fg L M) (f : L.hom M N) (hs : function.surjective ⇑f) :

first_order.language.Structure.fg L N

source

theorem first_order.language.Structure.cg_def {L : first_order.language} {M : Type u_3} [L.Structure M] :

first_order.language.Structure.cg L M ↔ ⊤.cg

source

theorem first_order.language.Structure.cg_iff {L : first_order.language} {M : Type u_3} [L.Structure M] :

first_order.language.Structure.cg L M ↔ ∃ (S : set M), S.countable ∧ ⇑(first_order.language.substructure.closure L) S = ⊤

An equivalent expression of Structure.cg.

source

theorem first_order.language.Structure.cg.range {L : first_order.language} {M : Type u_3} [L.Structure M] {N : Type u_4} [L.Structure N] (h : first_order.language.Structure.cg L M) (f : L.hom M N) :

f.range.cg

source

theorem first_order.language.Structure.cg.map_of_surjective {L : first_order.language} {M : Type u_3} [L.Structure M] {N : Type u_4} [L.Structure N] (h : first_order.language.Structure.cg L M) (f : L.hom M N) (hs : function.surjective ⇑f) :

first_order.language.Structure.cg L N

source

theorem first_order.language.Structure.cg_iff_countable {L : first_order.language} {M : Type u_3} [L.Structure M] [countable (Σ (l : ℕ), L.functions l)] :

first_order.language.Structure.cg L M ↔ countable M

source

theorem first_order.language.Structure.fg.cg {L : first_order.language} {M : Type u_3} [L.Structure M] (h : first_order.language.Structure.fg L M) :

first_order.language.Structure.cg L M

source

@[protected, instance]

def first_order.language.Structure.cg_of_fg {L : first_order.language} {M : Type u_3} [L.Structure M] [h : first_order.language.Structure.fg L M] :

first_order.language.Structure.cg L M

source

theorem first_order.language.equiv.fg_iff {L : first_order.language} {M : Type u_3} [L.Structure M] {N : Type u_4} [L.Structure N] (f : L.equiv M N) :

first_order.language.Structure.fg L M ↔ first_order.language.Structure.fg L N

source

theorem first_order.language.substructure.fg_iff_Structure_fg {L : first_order.language} {M : Type u_3} [L.Structure M] (S : L.substructure M) :

S.fg ↔ first_order.language.Structure.fg L ↥S

source

theorem first_order.language.equiv.cg_iff {L : first_order.language} {M : Type u_3} [L.Structure M] {N : Type u_4} [L.Structure N] (f : L.equiv M N) :

first_order.language.Structure.cg L M ↔ first_order.language.Structure.cg L N

source

theorem first_order.language.substructure.cg_iff_Structure_cg {L : first_order.language} {M : Type u_3} [L.Structure M] (S : L.substructure M) :

S.cg ↔ first_order.language.Structure.cg L ↥S