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.

source
def FirstOrder.Language.Substructure.FG {L : Language} {M : Type u_1} [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
    Instances For
      source
      theorem FirstOrder.Language.Substructure.fg_def {L : Language} {M : Type u_1} [L.Structure M] {N : L.Substructure M} :
      N.FG ↔ ∃ (S : Set M), S.Finite ∧ (closure L).toFun S = N
      source
      theorem FirstOrder.Language.Substructure.fg_iff_exists_fin_generating_family {L : Language} {M : Type u_1} [L.Structure M] {N : L.Substructure M} :
      N.FG ↔ ∃ (n : ℕ) (s : Fin n → M), (closure L).toFun (Set.range s) = N
      source
      theorem FirstOrder.Language.Substructure.fg_bot {L : Language} {M : Type u_1} [L.Structure M] :
      ⊥.FG
      source
      instance FirstOrder.Language.Substructure.instInhabited_fg {L : Language} {M : Type u_1} [L.Structure M] :
      Inhabited { S : L.Substructure M // S.FG }
      Equations
        source
        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
        source
        theorem FirstOrder.Language.Substructure.fg_closure_singleton {L : Language} {M : Type u_1} [L.Structure M] (x : M) :
        ((closure L).toFun {x}).FG
        source
        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) :
        (N₁ ⊔ N₂).FG
        source
        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) :
        (Substructure.map f s).FG
        source
        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
        source
        theorem FirstOrder.Language.Substructure.FG.of_finite {L : Language} {M : Type u_1} [L.Structure M] {s : L.Substructure M} [h : Finite ↥s] :
        s.FG
        source
        theorem FirstOrder.Language.Substructure.FG.finite {L : Language} {M : Type u_1} [L.Structure M] [L.IsRelational] {S : L.Substructure M} (h : S.FG) :
        Finite ↥S
        source
        theorem FirstOrder.Language.Substructure.fg_iff_finite {L : Language} {M : Type u_1} [L.Structure M] [L.IsRelational] {S : L.Substructure M} :
        S.FG ↔ Finite ↥S
        source
        def FirstOrder.Language.Substructure.CG {L : Language} {M : Type u_1} [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
          Instances For
            source
            theorem FirstOrder.Language.Substructure.cg_def {L : Language} {M : Type u_1} [L.Structure M] {N : L.Substructure M} :
            N.CG ↔ ∃ (S : Set M), S.Countable ∧ (closure L).toFun S = N
            source
            theorem FirstOrder.Language.Substructure.FG.cg {L : Language} {M : Type u_1} [L.Structure M] {N : L.Substructure M} (h : N.FG) :
            N.CG
            source
            theorem FirstOrder.Language.Substructure.cg_iff_empty_or_exists_nat_generating_family {L : Language} {M : Type u_1} [L.Structure M] {N : L.Substructure M} :
            N.CG ↔ ↑N = ∅ ∨ ∃ (s : ℕ → M), (closure L).toFun (Set.range s) = N
            source
            theorem FirstOrder.Language.Substructure.cg_bot {L : Language} {M : Type u_1} [L.Structure M] :
            ⊥.CG
            source
            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
            source
            theorem FirstOrder.Language.Substructure.cg_closure_singleton {L : Language} {M : Type u_1} [L.Structure M] (x : M) :
            ((closure L).toFun {x}).CG
            source
            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) :
            (N₁ ⊔ N₂).CG
            source
            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) :
            (Substructure.map f s).CG
            source
            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
            source
            theorem FirstOrder.Language.Substructure.cg_iff_countable {L : Language} {M : Type u_1} [L.Structure M] [Countable ((l : ℕ) × L.Functions l)] {s : L.Substructure M} :
            s.CG ↔ Countable ↥s
            source
            theorem FirstOrder.Language.Substructure.cg_of_countable {L : Language} {M : Type u_1} [L.Structure M] {s : L.Substructure M} [h : Countable ↥s] :
            s.CG
            source
            class FirstOrder.Language.Structure.FG (L : Language) (M : Type u_1) [L.Structure M] :
            Prop

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

            Instances
              source
              class FirstOrder.Language.Structure.CG (L : Language) (M : Type u_1) [L.Structure M] :
              Prop

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

              Instances
                source
                theorem FirstOrder.Language.Structure.fg_def {L : Language} {M : Type u_1} [L.Structure M] :
                FG L M ↔ ⊤.FG
                source
                theorem FirstOrder.Language.Structure.fg_iff {L : Language} {M : Type u_1} [L.Structure M] :
                FG L M ↔ ∃ (S : Set M), S.Finite ∧ (Substructure.closure L).toFun S = ⊤

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

                source
                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) :
                f.range.FG
                source
                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
                source
                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)
                source
                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)
                source
                theorem FirstOrder.Language.Structure.FG.countable_embedding {L : Language} {M : Type u_1} [L.Structure M] (N : Type u_2) [L.Structure N] [Countable N] :
                FG L M → Countable (L.Embedding M N)
                source
                instance FirstOrder.Language.Structure.Fg.instCountable_embedding {L : Language} {M : Type u_1} [L.Structure M] (N : Type u_2) [L.Structure N] [Countable N] [h : FG L M] :
                Countable (L.Embedding M N)
                source
                theorem FirstOrder.Language.Structure.FG.of_finite {L : Language} {M : Type u_1} [L.Structure M] [Finite M] :
                FG L M
                source
                theorem FirstOrder.Language.Structure.FG.finite {L : Language} {M : Type u_1} [L.Structure M] [L.IsRelational] (h : FG L M) :
                Finite M
                source
                theorem FirstOrder.Language.Structure.fg_iff_finite {L : Language} {M : Type u_1} [L.Structure M] [L.IsRelational] :
                FG L M ↔ Finite M
                source
                theorem FirstOrder.Language.Structure.cg_def {L : Language} {M : Type u_1} [L.Structure M] :
                CG L M ↔ ⊤.CG
                source
                theorem FirstOrder.Language.Structure.cg_iff {L : Language} {M : Type u_1} [L.Structure M] :
                CG L M ↔ ∃ (S : Set M), S.Countable ∧ (Substructure.closure L).toFun S = ⊤

                An equivalent expression of Structure.cg.

                source
                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) :
                f.range.CG
                source
                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
                source
                theorem FirstOrder.Language.Structure.cg_iff_countable {L : Language} {M : Type u_1} [L.Structure M] [Countable ((l : ℕ) × L.Functions l)] :
                CG L M ↔ Countable M
                source
                theorem FirstOrder.Language.Structure.cg_of_countable {L : Language} {M : Type u_1} [L.Structure M] [Countable M] :
                CG L M
                source
                theorem FirstOrder.Language.Structure.FG.cg {L : Language} {M : Type u_1} [L.Structure M] (h : FG L M) :
                CG L M
                source
                @[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
                source
                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) :
                Structure.FG L M ↔ Structure.FG L N
                source
                theorem FirstOrder.Language.Substructure.fg_iff_structure_fg {L : Language} {M : Type u_1} [L.Structure M] (S : L.Substructure M) :
                S.FG ↔ Structure.FG L ↥S
                source
                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) :
                Structure.CG L M ↔ Structure.CG L N
                source
                theorem FirstOrder.Language.Substructure.cg_iff_structure_cg {L : Language} {M : Type u_1} [L.Structure M] (S : L.Substructure M) :
                S.CG ↔ Structure.CG L ↥S
                source
                theorem FirstOrder.Language.Substructure.countable_fg_substructures_of_countable {L : Language} {M : Type u_1} [L.Structure M] [Countable M] :
                Countable { S : L.Substructure M // S.FG }
                source
                instance FirstOrder.Language.Substructure.instCountable_fg_substructures_of_countable {L : Language} {M : Type u_1} [L.Structure M] [Countable M] :
                Countable { S : L.Substructure M // S.FG }