mathlib3documentation

model_theory.finitely_generated

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.

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) :
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 : .fg) :
s.fg

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

Equations
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) :
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 : .cg) :
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] (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] (f : L.hom M N) :
@[protected, instance]
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) :
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) :