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

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

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

Equations

• R.leftDual J = {b : β | ∀ ⦃a : α⦄, a ∈ J → R a b}

def Rel.rightDual {α : Type u_1} {β : Type u_2} (R : Rel α β) (I : Set β) : Set α

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

Equations

• R.rightDual I = {a : α | ∀ ⦃b : β⦄, b ∈ I → R a b}

theorem Rel.gc_leftDual_rightDual {α : Type u_1} {β : Type u_2} (R : Rel α β) : 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

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

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

Equations

• R.leftFixedPoints = {J : Set α | R.rightDual (R.leftDual J) = J}

def Rel.rightFixedPoints {α : Type u_1} {β : Type u_2} (R : Rel α β) : Set (Set β)

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

Equations

• R.rightFixedPoints = {I : Set β | R.leftDual (R.rightDual I) = I}

theorem Rel.leftDual_mem_rightFixedPoint {α : Type u_1} {β : Type u_2} (R : Rel α β) (J : Set α) : R.leftDual J ∈ R.rightFixedPoints

leftDual maps every element J to rightFixedPoints.

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

rightDual maps every element I to leftFixedPoints.

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

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

Equations

• One or more equations did not get rendered due to their size.

theorem Rel.rightDual_leftDual_le_of_le {α : Type u_1} {β : Type u_2} (R : Rel α β) {J : Set α} {J' : Set α} (h : J' ∈ R.leftFixedPoints) (h₁ : J ≤ J') : R.rightDual (R.leftDual J) ≤ J'

theorem Rel.leftDual_rightDual_le_of_le {α : Type u_1} {β : Type u_2} (R : Rel α β) {I : Set β} {I' : Set β} (h : I' ∈ R.rightFixedPoints) (h₁ : I ≤ I') : R.leftDual (R.rightDual I) ≤ I'