Triposes.Basic

source

def HeytingHom.monotone {X Y : Type} [HeytingAlgebra X] [HeytingAlgebra Y] (f : HeytingHom X Y) :

Monotone ⇑f

Equations

⋯ = ⋯

Instances For

source

def P₀ {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} (X : 𝒞) :

HeytAlg

Equations

P₀ X = P.obj (Opposite.op X)

Instances For

source

def P₁ {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y : 𝒞} (f : X ⟶ Y) :

P₀ Y ⟶ P₀ X

Equations

P₁ = P.map ∘ Quiver.Hom.op

Instances For

source

@[simp]

theorem P₁.map_id {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X : 𝒞} :

P₁ (CategoryTheory.CategoryStruct.id X) = HeytingHom.id ↑(P₀ X)

source

@[simp]

theorem P₁.map_comp {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y Z : 𝒞} {f : X ⟶ Y} {g : Y ⟶ Z} :

P₁ (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (P₁ g) (P₁ f)

source

@[simp]

theorem P₁.map_comp_app {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y Z : 𝒞} {f : X ⟶ Y} {g : Y ⟶ Z} {z : ↑(P₀ Z)} :

(P₁ (CategoryTheory.CategoryStruct.comp f g)) z = (P₁ f) ((P₁ g) z)

source

@[simp]

theorem P₁.map_himp {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y : 𝒞} {f : X ⟶ Y} {y y' : ↑(P₀ Y)} :

(P₁ f) (y ⇨ y') = (P₁ f) y ⇨ (P₁ f) y'

source

@[simp]

theorem P₁.map_inf {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y : 𝒞} {f : X ⟶ Y} {y y' : ↑(P₀ Y)} :

(P₁ f) (y ⊓ y') = (P₁ f) y ⊓ (P₁ f) y'

source

@[simp]

theorem P₁.map_sup {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y : 𝒞} {f : X ⟶ Y} {y y' : ↑(P₀ Y)} :

(P₁ f) (y ⊔ y') = (P₁ f) y ⊔ (P₁ f) y'

source

@[simp]

theorem P₁.map_top {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y : 𝒞} {f : X ⟶ Y} :

(P₁ f) ⊤ = ⊤

source

theorem P.map_comp' {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y Z : 𝒞} {f : X ⟶ Y} {g : Y ⟶ Z} {z : ↑(P.obj (Opposite.op Z))} :

(P.map f.op) ((P.map g.op) z) = (P.map (CategoryTheory.CategoryStruct.comp g.op f.op)) z

source

theorem P₁.map_mono {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y : 𝒞} {f : X ⟶ Y} {y y' : ↑(P₀ Y)} (H : y ≤ y') :

(P₁ f) y ≤ (P₁ f) y'

source

class ChosenLeftAdjoints {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} :

Type (max (max u u_1) v)

A choice of adjoints for all morphisms

map : {X Y : 𝒞} → (X ⟶ Y) → ↑(P₀ X) →o ↑(P₀ Y)
The underlying map of the adjoint ∃_f
adj : ∀ {X Y : 𝒞} {f : X ⟶ Y} {x : ↑(P₀ X)} {y : ↑(P₀ Y)}, x ≤ (P₁ f) y ↔ (ChosenLeftAdjoints.map f) x ≤ y
The adjunction property x ≤ f* y ⇔ ∃_f x ≤ y

Instances

source

theorem ChosenLeftAdjoints.unit {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y : 𝒞} {f : X ⟶ Y} {x : ↑(P₀ X)} [𝔼 : ChosenLeftAdjoints] :

x ≤ (P₁ f) ((ChosenLeftAdjoints.map f) x)

The unit of the adjunction ∃_f ⊣ f*

source

theorem ChosenLeftAdjoints.counit {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y : 𝒞} {f : X ⟶ Y} {y : ↑(P₀ Y)} [𝔼 : ChosenLeftAdjoints] :

(ChosenLeftAdjoints.map f) ((P₁ f) y) ≤ y

The counit of the adjunction ∃_f ⊣ f*

source

theorem ChosenLeftAdjoints.id_adj_id {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X : 𝒞} [𝔼 : ChosenLeftAdjoints] :

ChosenLeftAdjoints.map (CategoryTheory.CategoryStruct.id X) = OrderHom.id

The proposition that ∃_𝟙 is the identity morphism

source

theorem ChosenLeftAdjoints.frob_left {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y : 𝒞} {f : X ⟶ Y} {x : ↑(P₀ X)} {y : ↑(P₀ Y)} [𝔼 : ChosenLeftAdjoints] :

(ChosenLeftAdjoints.map f) (x ⊓ (P₁ f) y) = (ChosenLeftAdjoints.map f) x ⊓ y

The left frobenius condition

source

theorem ChosenLeftAdjoints.frob_right {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y : 𝒞} {f : X ⟶ Y} {x : ↑(P₀ X)} {y : ↑(P₀ Y)} [𝔼 : ChosenLeftAdjoints] :

(ChosenLeftAdjoints.map f) ((P₁ f) y ⊓ x) = y ⊓ (ChosenLeftAdjoints.map f) x

The right frobenius condition

source

class ChosenRightAdjoints {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} :

Type (max (max u u_1) v)

map : {X Y : 𝒞} → (X ⟶ Y) → ↑(P₀ X) →o ↑(P₀ Y)
The underlying map of the adjoint ∀_f
adj : ∀ {X Y : 𝒞} {f : X ⟶ Y} {y : ↑(P₀ Y)} {x : ↑(P₀ X)}, (P₁ f) y ≤ x ↔ y ≤ (ChosenRightAdjoints.map f) x
The adjunction property f* x ≤ y ⇔ x ≤ ∀_f y

Instances

source

theorem ChosenRightAdjoints.unit {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y : 𝒞} {f : X ⟶ Y} {y : ↑(P₀ Y)} [𝔸 : ChosenRightAdjoints] :

y ≤ (ChosenRightAdjoints.map f) ((P₁ f) y)

The unit of the adjunction f* ⊣ ∀_f

source

theorem ChosenRightAdjoints.counit {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y : 𝒞} {f : X ⟶ Y} {x : ↑(P₀ X)} [𝔸 : ChosenRightAdjoints] :

(P₁ f) ((ChosenRightAdjoints.map f) x) ≤ x

The counit of the adjunction f* ⊣ ∀_f

source

theorem ChosenRightAdjoints.id_adj_id {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X : 𝒞} [𝔸 : ChosenRightAdjoints] :

ChosenRightAdjoints.map (CategoryTheory.CategoryStruct.id X) = OrderHom.id

The proposition that ∀_𝟙 is the identity morphism

source

theorem ChosenRightAdjoints.top_eq_top {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y : 𝒞} {f : X ⟶ Y} [𝔸 : ChosenRightAdjoints] :

(ChosenRightAdjoints.map f) ⊤ = ⊤

The proposition that ∀_f preserves the top element

source

theorem frobenius' {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} {X Y : 𝒞} {f : X ⟶ Y} {x : ↑(P₀ X)} {y : ↑(P₀ Y)} [𝔸 : ChosenRightAdjoints] [𝔼 : ChosenLeftAdjoints] :

(ChosenRightAdjoints.map f) (x ⇨ (P₁ f) y) = (ChosenLeftAdjoints.map f) x ⇨ y

The proposition that ∀_f(φ(x) ⇒ ψ) = (∃_f φ(x)) ⇒ ψ

source

class ChosenGeneric {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} :

Type (max (max u u_1) v)

The generic object

𝕊 : 𝒞
σ : ↑(P₀ (ChosenGeneric.𝕊 P))
bracket : {X : 𝒞} → ↑(P₀ X) → (X ⟶ ChosenGeneric.𝕊 P)
σIsGeneric : ∀ {X : 𝒞} (φ : ↑(P₀ X)), φ = (P₁ (ChosenGeneric.bracket φ)) ChosenGeneric.σ

Instances

source

class Tripos {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] (P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg) extends ChosenGeneric :

Type (max (max u u_1) v)

A tripos is a contravariant functor P, with chosen left and right adjoints to substitutions, the corresponding Beck-Chevalley rules, and a chosen generic object

𝕊 : 𝒞
σ : ↑(P₀ (ChosenGeneric.𝕊 P))
bracket : {X : 𝒞} → ↑(P₀ X) → (X ⟶ ChosenGeneric.𝕊 P)
σIsGeneric : ∀ {X : 𝒞} (φ : ↑(P₀ X)), φ = (P₁ (ChosenGeneric.bracket φ)) ChosenGeneric.σ
𝔼 : ChosenLeftAdjoints
The existential quantifier
𝔸 : ChosenRightAdjoints
The universal quantifier
𝔼_BeckChevalley : ∀ {X Y Z W : 𝒞} {f : X ⟶ Y} {g : X ⟶ Z} {h : Y ⟶ W} {k : Z ⟶ W} {z : ↑(P₀ Z)}, CategoryTheory.IsPullback f g h k → (ChosenLeftAdjoints.map f) ((P₁ g) z) = (P₁ h) ((ChosenLeftAdjoints.map k) z)
For the pullback square
```
X ---f---> Y
|          |
g          h
|          |
v          v
Z ---k---> W
```
the proposition ∃_f (g* z) = g* (∃_k z)
𝔸_BeckChevalley : ∀ {X Y Z W : 𝒞} {f : X ⟶ Y} {g : X ⟶ Z} {h : Y ⟶ W} {k : Z ⟶ W} {z : ↑(P₀ Z)}, CategoryTheory.IsPullback f g h k → (ChosenRightAdjoints.map f) ((P₁ g) z) = (P₁ h) ((ChosenRightAdjoints.map k) z)
For the pullback square
```
X ---f---> Y
|          |
g          h
|          |
v          v
Z ---k---> W
```
the proposition ∀_f (g* z) = g* (∀_k z)

Instances

source

theorem Tripos.frobenius {𝒞 : Type u} [CategoryTheory.Category.{v, u} 𝒞] {P : CategoryTheory.Functor 𝒞ᵒᵖ HeytAlg} [T : Tripos P] {X Y : 𝒞} {f : X ⟶ Y} {x : ↑(P₀ X)} {y : ↑(P₀ Y)} :

(ChosenRightAdjoints.map f) (x ⇨ (P₁ f) y) = (ChosenLeftAdjoints.map f) x ⇨ y

The proposition that ∀_f(φ(x) ⇒ ψ) = (∃_f φ(x)) ⇒ ψ