Documentation

Mathlib.Order.Rel.GaloisConnection

The Galois Connection Induced by a Relation #

In this file, we show that an arbitrary relation R between a pair of types α and β defines a pair toDual ∘ R.leftDual and R.rightDual ∘ ofDual of adjoint order-preserving maps between the corresponding posets Set α and (Set β)ᵒᵈ. We define R.leftFixedPoints (resp. R.rightFixedPoints) as the set of fixed points J (resp. I) of Set α (resp. Set β) such that rightDual (leftDual J) = J (resp. leftDual (rightDual I) = I).

Main Results #

⋆ Rel.gc_leftDual_rightDual: we prove that the maps toDual ∘ R.leftDual and R.rightDual ∘ ofDual form a Galois connection. ⋆ Rel.equivFixedPoints: we prove that the maps R.leftDual and R.rightDual induce inverse bijections between the sets of fixed points.

References #

⋆ Engendrement de topologies, démontrabilité et opérations sur les sous-topos, Olivia Caramello and Laurent Lafforgue (in preparation)

Tags #

relation, Galois connection, induced bijection, fixed points

Pairs of adjoint maps defined by relations #

source
def SetRel.leftDual {α : Type u_1} {β : Type u_2} (R : SetRel α β) (J : Set α) :
Set β

leftDual maps any set J of elements of type α to the set {b : β | ∀ a ∈ J, a ~[R] b} of elements b of type β such that a ~[R] b for every element a of J.

Equations
    Instances For
      source
      def SetRel.rightDual {α : Type u_1} {β : Type u_2} (R : SetRel α β) (I : Set β) :
      Set α

      rightDual maps any set I of elements of type β to the set {a : α | ∀ b ∈ I, a ~[R] b} of elements a of type α such that a ~[R] b for every element b of I.

      Equations
        Instances For
          source
          theorem SetRel.gc_leftDual_rightDual {α : Type u_1} {β : Type u_2} (R : SetRel α β) :
          GaloisConnection (⇑OrderDual.toDual ∘ R.leftDual) (R.rightDual ∘ ⇑OrderDual.ofDual)

          The pair of functions toDual ∘ leftDual and rightDual ∘ ofDual forms a Galois connection.

          Induced equivalences between fixed points #

          source
          def SetRel.leftFixedPoints {α : Type u_1} {β : Type u_2} (R : SetRel α β) :
          Set (Set α)

          leftFixedPoints is the set of elements J : Set α satisfying rightDual (leftDual J) = J.

          Equations
            Instances For
              source
              def SetRel.rightFixedPoints {α : Type u_1} {β : Type u_2} (R : SetRel α β) :
              Set (Set β)

              rightFixedPoints is the set of elements I : Set β satisfying leftDual (rightDual I) = I.

              Equations
                Instances For
                  source
                  theorem SetRel.leftDual_mem_rightFixedPoint {α : Type u_1} {β : Type u_2} (R : SetRel α β) (J : Set α) :
                  R.leftDual J ∈ R.rightFixedPoints

                  leftDual maps every element J to rightFixedPoints.

                  source
                  theorem SetRel.rightDual_mem_leftFixedPoint {α : Type u_1} {β : Type u_2} (R : SetRel α β) (I : Set β) :
                  R.rightDual I ∈ R.leftFixedPoints

                  rightDual maps every element I to leftFixedPoints.

                  source
                  def SetRel.equivFixedPoints {α : Type u_1} {β : Type u_2} (R : SetRel α β) :
                  ↑R.leftFixedPoints ≃ ↑R.rightFixedPoints

                  The maps leftDual and rightDual induce inverse bijections between the sets of fixed points.

                  Equations
                    Instances For
                      source
                      theorem SetRel.rightDual_leftDual_le_of_le {α : Type u_1} {β : Type u_2} (R : SetRel α β) {J J' : Set α} (h : J' ∈ R.leftFixedPoints) (h₁ : J ≤ J') :
                      R.rightDual (R.leftDual J) ≤ J'
                      source
                      theorem SetRel.leftDual_rightDual_le_of_le {α : Type u_1} {β : Type u_2} (R : SetRel α β) {I I' : Set β} (h : I' ∈ R.rightFixedPoints) (h₁ : I ≤ I') :
                      R.leftDual (R.rightDual I) ≤ I'