mathlib documentation

model_theory.finitely_generated

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 #

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 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
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
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) :
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
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
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
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) :
@[class]
structure first_order.language.Structure.fg (L : first_order.language) (M : Type u_3) [L.Structure M] :
Prop

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

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

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

Instances of this typeclass

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

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

An equivalent expression of Structure.cg.

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