Documentation

LeanPool.DomainTheory.Neighborhood.Exercise120

Exercise 1.20 (Scott 1981, PRG-19, ยง1) โ€” the power system ๐’Ÿ' = {โ†‘X} #

For any neighbourhood system ๐’Ÿ over ฮ”, Scott takes ฮ”' = ๐’Ÿ and ๐’Ÿ' = {โ†‘X โˆฃ X โˆˆ ๐’Ÿ} where โ†‘X = {Y โˆˆ ๐’Ÿ โˆฃ Y โŠ† X} (the up-set of X inside ๐’Ÿ โ€” not the principal filter of Definition 1.7, which is the down-set {Y โˆˆ ๐’Ÿ โˆฃ X โŠ† Y}). The exercise asks to show ๐’Ÿ' is positive and that |๐’Ÿ| โ‰… |๐’Ÿ'|, with finite elements and tokens of ๐’Ÿ' in one-one correspondence.

This file (named upSet to avoid the principal/โ†‘X collision):

Note the variance: X โ†ฆ โ†‘X is inclusion-preserving (upSet_subset_iff), unlike Def 1.7's principal. Everything is [propext, Quot.sound].

source
def Domain.Neighborhood.NeighborhoodSystem.upSet {ฮฑ : Type u_1} (V : NeighborhoodSystem ฮฑ) (X : Set ฮฑ) :
Set (Set ฮฑ)

Exercise 1.20's โ†‘X = {Y โˆˆ ๐’Ÿ โˆฃ Y โŠ† X} (the up-set of X inside ๐’Ÿ).

Equations
Instances For
    source
    @[simp]
    theorem Domain.Neighborhood.NeighborhoodSystem.mem_upSet {ฮฑ : Type u_1} (V : NeighborhoodSystem ฮฑ) {X Y : Set ฮฑ} :
    Y โˆˆ V.upSet X โ†” V.mem Y โˆง Y โŠ† X
    source
    theorem Domain.Neighborhood.NeighborhoodSystem.upSet_inter {ฮฑ : Type u_1} (V : NeighborhoodSystem ฮฑ) (X Y : Set ฮฑ) :
    V.upSet X โˆฉ V.upSet Y = V.upSet (X โˆฉ Y)

    โ†‘X โˆฉ โ†‘Y = โ†‘(X โˆฉ Y) โ€” a set identity (no membership hypotheses).

    source
    theorem Domain.Neighborhood.NeighborhoodSystem.upSet_subset_iff {ฮฑ : Type u_1} (V : NeighborhoodSystem ฮฑ) {X Y : Set ฮฑ} (hX : V.mem X) :
    V.upSet X โŠ† V.upSet Y โ†” X โŠ† Y

    X โ†ฆ โ†‘X is inclusion-preserving: โ†‘X โŠ† โ†‘Y โ†” X โŠ† Y (for X โˆˆ ๐’Ÿ). โ†’ tests at X โˆˆ โ†‘X; โ† is transitivity of โŠ†.

    source
    theorem Domain.Neighborhood.NeighborhoodSystem.upSet_injective {ฮฑ : Type u_1} (V : NeighborhoodSystem ฮฑ) {X Y : Set ฮฑ} (hX : V.mem X) (hY : V.mem Y) (h : V.upSet X = V.upSet Y) :
    X = Y

    X โ†ฆ โ†‘X is one-one on ๐’Ÿ.

    source
    def Domain.Neighborhood.NeighborhoodSystem.powerSystem {ฮฑ : Type u_1} (V : NeighborhoodSystem ฮฑ) :
    NeighborhoodSystem (Set ฮฑ)

    Exercise 1.20 โ€” the power system ๐’Ÿ' = {โ†‘X โˆฃ X โˆˆ ๐’Ÿ} over the tokens ฮ”' = ๐’Ÿ. The master is โ†‘ฮ”; the intersection law uses the consistency witness Z โˆˆ โ†‘Z โŠ† โ†‘X โˆฉ โ†‘Y to get Z โŠ† X โˆฉ Y, hence X โˆฉ Y โˆˆ ๐’Ÿ and โ†‘X โˆฉ โ†‘Y = โ†‘(XโˆฉY).

    Equations
    Instances For
      source
      @[simp]
      theorem Domain.Neighborhood.NeighborhoodSystem.powerSystem_mem {ฮฑ : Type u_1} (V : NeighborhoodSystem ฮฑ) {S : Set (Set ฮฑ)} :
      V.powerSystem.mem S โ†” โˆƒ (X : Set ฮฑ), V.mem X โˆง S = V.upSet X
      source
      theorem Domain.Neighborhood.NeighborhoodSystem.powerSystem_isPositive {ฮฑ : Type u_1} (V : NeighborhoodSystem ฮฑ) :
      V.powerSystem.IsPositive

      Exercise 1.20 โ€” ๐’Ÿ' is positive. โ†‘X โˆฉ โ†‘Y = โ†‘(XโˆฉY) is a neighbourhood iff it is non-empty: a witness Z โŠ† X โˆฉ Y gives X โˆฉ Y โˆˆ ๐’Ÿ; conversely โ†‘W always contains W.

      The isomorphism |๐’Ÿ| โ‰ƒo |๐’Ÿ'|. #

      source
      def Domain.Neighborhood.NeighborhoodSystem.toPower {ฮฑ : Type u_1} (V : NeighborhoodSystem ฮฑ) (x : V.Element) :
      V.powerSystem.Element

      The element of |๐’Ÿ'| corresponding to x โˆˆ |๐’Ÿ|: the filter {โ†‘W โˆฃ W โˆˆ x}.

      Equations
      Instances For
        source
        def Domain.Neighborhood.NeighborhoodSystem.ofPower {ฮฑ : Type u_1} (V : NeighborhoodSystem ฮฑ) (y : V.powerSystem.Element) :
        V.Element

        The element of |๐’Ÿ| corresponding to y โˆˆ |๐’Ÿ'|: the filter {W โˆฃ โ†‘W โˆˆ y}.

        Equations
        • V.ofPower y = { mem := fun (W : Set ฮฑ) => V.mem W โˆง y.mem (V.upSet W), sub := โ‹ฏ, master_mem := โ‹ฏ, inter_mem := โ‹ฏ, up_mem := โ‹ฏ }
        Instances For
          source
          def Domain.Neighborhood.NeighborhoodSystem.powerIso {ฮฑ : Type u_1} (V : NeighborhoodSystem ฮฑ) :
          V.Element โ‰ƒo V.powerSystem.Element

          Exercise 1.20 (the isomorphism). toPower/ofPower are mutually inverse and preserve/reflect โŠ‘, giving |๐’Ÿ| โ‰ƒo |๐’Ÿ'|.

          Equations
          • V.powerIso = { toFun := V.toPower, invFun := V.ofPower, left_inv := โ‹ฏ, right_inv := โ‹ฏ, map_rel_iff' := โ‹ฏ }
          Instances For
            source
            theorem Domain.Neighborhood.NeighborhoodSystem.isomorphic_powerSystem {ฮฑ : Type u_1} (V : NeighborhoodSystem ฮฑ) :
            V โ‰…แดฐ V.powerSystem

            Exercise 1.20 (statement). ๐’Ÿ and its power system ๐’Ÿ' are isomorphic.

            source
            theorem Domain.Neighborhood.NeighborhoodSystem.toPower_principal {ฮฑ : Type u_1} (V : NeighborhoodSystem ฮฑ) {X : Set ฮฑ} (hX : V.mem X) :
            V.toPower (V.principal hX) = V.powerSystem.principal โ‹ฏ

            Exercise 1.20 โ€” tokens โ†” finite elements. The iso carries the finite element โ†‘X of |๐’Ÿ| (Def 1.7) to the finite element of |๐’Ÿ'| generated by the token โ†‘X, i.e. the principal filter of โ†‘X in ๐’Ÿ'. Since X โ†ฆ โ†‘X is one-one (upSet_injective), tokens of ๐’Ÿ' and its finite elements are in one-one correspondence.