Documentation

InfinitaryLogic.Descriptive.InvariantMeasurableSpace

The invariant σ-algebras on the structure space (issue #28, commit 1) #

Two σ-algebras of invariant measurable classes of coded structures, and their equality.

Everything here is elementary: no Polishness and no symbol-countability hypothesis is used — the invariance predicates are closed under complement and countable union on the nose, and the σ-algebra equality is a pointwise membership equivalence. ([L.IsRelational] is needed only for the isomorphism-invariant side and the equality, since IsomorphismInvariant is defined via decoded structures.) Measurability of concrete classes such as ModelsOf φ is the compatibility commit.

The generic invariant σ-algebra #

source
@[reducible]
def MeasurableSpace.smulInvariant (G : Type u_1) {X : Type u_2} [SMul G X] (m : MeasurableSpace X) :
MeasurableSpace X

The generic invariant σ-algebra. For an SMul G X action and an explicitly supplied base MeasurableSpace X, the measurable G-invariant sets form a σ-algebra (a sub-σ-algebra of m). The base measurable space is explicit so specializing never triggers recursive instance search.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MeasurableSpace.measurableSet_smulInvariant {G : Type u_1} {X : Type u_2} [SMul G X] {m : MeasurableSpace X} {B : Set X} :
    MeasurableSet B ↔ MeasurableSet B ∧ ∀ (g : G) (x : X), x ∈ B ↔ g • x ∈ B

    Membership in the generic invariant σ-algebra: measurable and invariant.

    Closure of the invariance predicates #

    source
    theorem FirstOrder.Language.ActionInvariant.compl {L : Language} {B : Set L.StructureSpace} (h : ActionInvariant B) :
    ActionInvariant Bᶜ

    Action invariance is closed under complement.

    source
    theorem FirstOrder.Language.ActionInvariant.iUnion {L : Language} {f : ℕ → Set L.StructureSpace} (h : ∀ (n : ℕ), ActionInvariant (f n)) :
    ActionInvariant (⋃ (n : ℕ), f n)

    Action invariance is closed under countable union.

    source
    theorem FirstOrder.Language.actionInvariant_empty {L : Language} :
    ActionInvariant ∅
    source
    theorem FirstOrder.Language.IsomorphismInvariant.compl {L : Language} [L.IsRelational] {B : Set L.StructureSpace} (h : IsomorphismInvariant B) :
    IsomorphismInvariant Bᶜ

    Isomorphism invariance is closed under complement.

    source
    theorem FirstOrder.Language.IsomorphismInvariant.iUnion {L : Language} [L.IsRelational] {f : ℕ → Set L.StructureSpace} (h : ∀ (n : ℕ), IsomorphismInvariant (f n)) :
    IsomorphismInvariant (⋃ (n : ℕ), f n)

    Isomorphism invariance is closed under countable union.

    source
    theorem FirstOrder.Language.isomorphismInvariant_empty {L : Language} [L.IsRelational] :
    IsomorphismInvariant ∅

    The two named invariant σ-algebras #

    source
    @[reducible]
    def FirstOrder.Language.isoInvariantMeasurableSpace {L : Language} [L.IsRelational] :
    MeasurableSpace L.StructureSpace

    The σ-algebra of measurable isomorphism-invariant classes of coded structures.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[reducible]
      def FirstOrder.Language.actionInvariantMeasurableSpace {L : Language} :
      MeasurableSpace L.StructureSpace

      The σ-algebra of measurable action-invariant classes, i.e. the generic invariant σ-algebra for the S∞-action on StructureSpace L over the product σ-algebra. Needs no relationality.

      Equations
      Instances For

        Membership iff lemmas #

        source
        theorem FirstOrder.Language.measurableSet_actionInvariantMeasurableSpace {L : Language} {B : Set L.StructureSpace} :
        MeasurableSet B ↔ MeasurableSet B ∧ ActionInvariant B

        A class is actionInvariantMeasurableSpace-measurable iff it is measurable and action-invariant.

        source
        theorem FirstOrder.Language.measurableSet_isoInvariantMeasurableSpace {L : Language} [L.IsRelational] {B : Set L.StructureSpace} :
        MeasurableSet B ↔ MeasurableSet B ∧ IsomorphismInvariant B

        A class is isoInvariantMeasurableSpace-measurable iff it is measurable and isomorphism-invariant.

        The two σ-algebras coincide #

        source
        theorem FirstOrder.Language.actionInvariantMeasurableSpace_eq_isoInvariantMeasurableSpace {L : Language} [L.IsRelational] :
        actionInvariantMeasurableSpace = isoInvariantMeasurableSpace

        The invariant σ-algebras coincide. Action invariance and isomorphism invariance define the same measurable classes, by actionInvariant_iff_isomorphismInvariant. No Polishness or symbol-countability hypothesis is used.