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.

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

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

Equations
Instances For
    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 nM), (FirstOrder.Language.Substructure.closure L).toFun (Set.range s) = N
    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) :
    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) :
    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) :

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

    Equations
    Instances For
      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_closure {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {s : Set M} (hs : s.Countable) :
      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) :
      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] :

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

      Instances
        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] :

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

        Instances
          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

          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) :
          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] :
          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.finite {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [L.IsRelational] (h : FirstOrder.Language.Structure.FG L M) :

          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) :
          @[instance 100]
          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) :
          theorem FirstOrder.Language.Substructure.fg_iff_structure_fg {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (S : L.Substructure M) :
          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) :
          theorem FirstOrder.Language.Substructure.cg_iff_structure_cg {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (S : L.Substructure M) :
          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
          • =