Documentation

Mathlib.ModelTheory.FinitelyGenerated

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.

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

Equations
theorem FirstOrder.Language.Substructure.fg_closure {L : Language} {M : Type u_1} [L.Structure M] {s : Set M} (hs : s.Finite) :
((closure L).toFun s).FG
theorem FirstOrder.Language.Substructure.FG.sup {L : Language} {M : Type u_1} [L.Structure M] {N₁ N₂ : L.Substructure M} (hN₁ : N₁.FG) (hN₂ : N₂.FG) :
theorem FirstOrder.Language.Substructure.FG.map {L : 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) :
theorem FirstOrder.Language.Substructure.FG.of_map_embedding {L : 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 : (Substructure.map f.toHom s).FG) :
s.FG

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

Equations
theorem FirstOrder.Language.Substructure.FG.cg {L : Language} {M : Type u_1} [L.Structure M] {N : L.Substructure M} (h : N.FG) :
N.CG
theorem FirstOrder.Language.Substructure.cg_closure {L : Language} {M : Type u_1} [L.Structure M] {s : Set M} (hs : s.Countable) :
((closure L).toFun s).CG
theorem FirstOrder.Language.Substructure.CG.sup {L : Language} {M : Type u_1} [L.Structure M] {N₁ N₂ : L.Substructure M} (hN₁ : N₁.CG) (hN₂ : N₂.CG) :
theorem FirstOrder.Language.Substructure.CG.map {L : 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) :
theorem FirstOrder.Language.Substructure.CG.of_map_embedding {L : 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 : (Substructure.map f.toHom s).CG) :
s.CG

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

Instances

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

    Instances

      An equivalent expression of Structure.FG in terms of Set.Finite instead of Finset.

      theorem FirstOrder.Language.Structure.FG.range {L : Language} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] (h : FG L M) (f : L.Hom M N) :
      theorem FirstOrder.Language.Structure.FG.map_of_surjective {L : Language} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] (h : FG L M) (f : L.Hom M N) (hs : Function.Surjective f) :
      FG L N
      theorem FirstOrder.Language.Structure.FG.countable_hom {L : Language} {M : Type u_1} [L.Structure M] (N : Type u_2) [L.Structure N] [Countable N] (h : FG L M) :
      Countable (L.Hom M N)
      instance FirstOrder.Language.Structure.FG.instCountable_hom {L : Language} {M : Type u_1} [L.Structure M] (N : Type u_2) [L.Structure N] [Countable N] [h : FG L M] :
      Countable (L.Hom M N)

      An equivalent expression of Structure.cg.

      theorem FirstOrder.Language.Structure.CG.range {L : Language} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] (h : CG L M) (f : L.Hom M N) :
      theorem FirstOrder.Language.Structure.CG.map_of_surjective {L : Language} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] (h : CG L M) (f : L.Hom M N) (hs : Function.Surjective f) :
      CG L N
      theorem FirstOrder.Language.Structure.FG.cg {L : Language} {M : Type u_1} [L.Structure M] (h : FG L M) :
      CG L M
      @[instance 100]
      instance FirstOrder.Language.Structure.cg_of_fg {L : Language} {M : Type u_1} [L.Structure M] [h : FG L M] :
      CG L M
      theorem FirstOrder.Language.Equiv.fg_iff {L : Language} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] (f : L.Equiv M N) :
      theorem FirstOrder.Language.Equiv.cg_iff {L : Language} {M : Type u_1} [L.Structure M] {N : Type u_2} [L.Structure N] (f : L.Equiv M N) :