AbstractInterpretation.GaloisConnection

source

structure GaloisConnection {L : Type u_1} {M : Type u_2} [Poset L] [Poset M] (alpha : L → M) (gamma : M → L) :

Prop

alpha_mon : monotone alpha
gamma_mon : monotone gamma
unit (l : L) : Poset.le l (gamma (alpha l))
counit (m : M) : Poset.le (alpha (gamma m)) m

Instances For

source

structure Adjunction {L : Type u_1} {M : Type u_2} [Poset L] [Poset M] (alpha : L → M) (gamma : M → L) :

Prop

adj (l : L) (m : M) : Poset.le l (gamma m) ↔ Poset.le (alpha l) m

Instances For

source

theorem galois_to_adjunction {L : Type u_1} {M : Type u_2} [Poset L] [Poset M] {alpha : L → M} {gamma : M → L} (gc : GaloisConnection alpha gamma) :

Adjunction alpha gamma

source

theorem adjunction_to_unit {L : Type u_1} {M : Type u_2} [Poset L] [Poset M] {alpha : L → M} {gamma : M → L} (adj : Adjunction alpha gamma) (l : L) :

Poset.le l (gamma (alpha l))

source

theorem adjunction_to_counit {L : Type u_1} {M : Type u_2} [Poset L] [Poset M] {alpha : L → M} {gamma : M → L} (adj : Adjunction alpha gamma) (m : M) :

Poset.le (alpha (gamma m)) m

source

theorem adjunction_to_galois {L : Type u_1} {M : Type u_2} [Poset L] [Poset M] {alpha : L → M} {gamma : M → L} (adj : Adjunction alpha gamma) :

GaloisConnection alpha gamma

source

theorem adjunction_iff_galois {L : Type u_1} {M : Type u_2} [Poset L] [Poset M] {alpha : L → M} {gamma : M → L} :

Adjunction alpha gamma ↔ GaloisConnection alpha gamma

source

theorem galois_alpha_idem {L : Type u_1} {M : Type u_2} [Poset L] [Poset M] {alpha : L → M} {gamma : M → L} (gc : GaloisConnection alpha gamma) (l : L) :

alpha (gamma (alpha l)) = alpha l

source

theorem galois_gamma_idem {L : Type u_1} {M : Type u_2} [Poset L] [Poset M] {alpha : L → M} {gamma : M → L} (gc : GaloisConnection alpha gamma) (m : M) :

gamma (alpha (gamma m)) = gamma m

source

theorem alpha_preserve_ub {L : Type u_1} {M : Type u_2} [CompleteLattice L] [CompleteLattice M] {alpha : L → M} {gamma : M → L} (gc : GaloisConnection alpha gamma) (ub : M) (L' : Set L) :

Poset.le (alpha (⊔L')) ub ↔ Poset.le (⊔alpha '' L') ub

source

theorem galois_to_alpha_is_additive {L : Type u_1} {M : Type u_2} [CompleteLattice L] [CompleteLattice M] {alpha : L → M} {gamma : M → L} (gc : GaloisConnection alpha gamma) (L' : Set L) :

alpha (⊔L') = (⊔alpha '' L')

source

theorem galois_gamma_uniqueness {L : Type u_1} {M : Type u_2} [Poset L] [Poset M] {alpha : L → M} {gamma1 gamma2 : M → L} (gc1 : GaloisConnection alpha gamma1) (gc2 : GaloisConnection alpha gamma2) (m : M) :

gamma1 m = gamma2 m

source

def gamma_by_alpha {L : Type u_1} {M : Type u_2} [CompleteLattice L] [CompleteLattice M] (alpha : L → M) :

M → L

Equations

gamma_by_alpha alpha m = (⊔{l : L | Poset.le (alpha l) m})

Instances For

source

theorem gamma_by_alpha_mono {L : Type u_1} {M : Type u_2} [CompleteLattice L] [CompleteLattice M] (alpha : L → M) :

monotone (gamma_by_alpha alpha)

source

theorem gamma_by_alpha_unit {L : Type u_1} {M : Type u_2} [CompleteLattice L] [CompleteLattice M] (alpha : L → M) (l : L) :

Poset.le l (gamma_by_alpha alpha (alpha l))

source

def determine_gamma_by_alpha {L : Type u_1} {M : Type u_2} [CompleteLattice L] [CompleteLattice M] {alpha : L → M} {gamma : M → L} (gc : GaloisConnection alpha gamma) :

GaloisConnection alpha (gamma_by_alpha alpha)

Equations

⋯ = ⋯

Instances For

source

theorem galois_gamma_by_alpha {L : Type u_1} {M : Type u_2} [CompleteLattice L] [CompleteLattice M] {alpha : L → M} {gamma : M → L} (gc : GaloisConnection alpha gamma) (m : M) :

gamma m = gamma_by_alpha alpha m

source

theorem alpha_additive_to_galois {L : Type u_1} {M : Type u_2} [CompleteLattice L] [CompleteLattice M] {alpha : L → M} (alpha_additive : ∀ (L' : Set L), alpha (⊔L') = (⊔alpha '' L')) :

GaloisConnection alpha (gamma_by_alpha alpha)

source

theorem galois_exists_if_alpha_is_additive {L : Type u_1} {M : Type u_2} [CompleteLattice L] [CompleteLattice M] {alpha : L → M} (alpha_additive : ∀ (L' : Set L), alpha (⊔L') = (⊔alpha '' L')) :

∃ (gamma : M → L), GaloisConnection alpha gamma

source

theorem galois_iff_alpha_is_additive {L : Type u_1} {M : Type u_2} [CompleteLattice L] [CompleteLattice M] {alpha : L → M} :

(∃ (gamma : M → L), GaloisConnection alpha gamma) ↔ ∀ (L' : Set L), alpha (⊔L') = (⊔alpha '' L')

source

theorem galois_connection_dual {L : Type u_1} {M : Type u_2} [instL : Poset L] [instM : Poset M] {alpha : L → M} {gamma : M → L} (gc : GaloisConnection alpha gamma) :

have instL' := { le := fun (x y : L) => Poset.le y x, le_refl := ⋯, le_trans := ⋯, le_antisym := ⋯ }; have instM' := { le := fun (x y : M) => Poset.le y x, le_refl := ⋯, le_trans := ⋯, le_antisym := ⋯ }; GaloisConnection gamma alpha