mathlib documentation

data.quot

Quotient types

This module extensd the core library's treatment of quotient types (init.data.quot).

Tags

quotient

theorem setoid.ext {α : Sort u_1} {s t : setoid α} :
(∀ (a b : α), setoid.r a b setoid.r a b)s = t

@[instance]
def quot.inhabited {α : Sort u_1} {ra : α → α → Prop} [inhabited α] :
inhabited (quot ra)

Equations
def quot.hrec_on₂ {α : Sort u_1} {β : Sort u_2} {ra : α → α → Prop} {rb : β → β → Prop} {φ : quot raquot rbSort u_3} (qa : quot ra) (qb : quot rb) (f : Π (a : α) (b : β), φ (quot.mk ra a) (quot.mk rb b)) :
(∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂f a₁ b == f a₂ b)(∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂f a b₁ == f a b₂)φ qa qb

Recursion on two quotient arguments a and b, result type depends on ⟦a⟧ and ⟦b⟧.

Equations
def quot.map {α : Sort u_1} {β : Sort u_2} {ra : α → α → Prop} {rb : β → β → Prop} (f : α → β) :
(ra rb) f fquot raquot rb

Map a function f : α → β such that ra x y implies rb (f x) (f y) to a map quot ra → quot rb.

Equations
  • quot.map f h = quot.lift (λ (x : α), quot.mk rb (f x)) _
def quot.map_right {α : Sort u_1} {ra ra' : α → α → Prop} :
(∀ (a₁ a₂ : α), ra a₁ a₂ra' a₁ a₂)quot raquot ra'

If ra is a subrelation of ra', then we have a natural map quot ra → quot ra'.

Equations
def quot.factor {α : Type u_1} (r s : α → α → Prop) :
(∀ (x y : α), r x ys x y)quot rquot s

weaken the relation of a quotient

Equations
theorem quot.factor_mk_eq {α : Type u_1} (r s : α → α → Prop) (h : ∀ (x y : α), r x ys x y) :
quot.factor r s h quot.mk r = quot.mk s

def quot.lift₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} (f : α → β → γ) :
(∀ (a : α) (b₁ b₂ : β), s b₁ b₂f a b₁ = f a b₂)(∀ (a₁ a₂ : α) (b : β), r a₁ a₂f a₁ b = f a₂ b)quot rquot s → γ

Descends a function f : α → β → γ to quotients of α and β.

Equations
  • quot.lift₂ f hr hs q₁ q₂ = quot.lift (λ (a : α), quot.lift (f a) _) _ q₁ q₂
@[simp]
theorem quot.lift₂_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} (a : α) (b : β) (f : α → β → γ) (hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂f a b₁ = f a b₂) (hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂f a₁ b = f a₂ b) :
quot.lift₂ f hr hs (quot.mk r a) (quot.mk s b) = f a b

def quot.lift_on₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} (p : quot r) (q : quot s) (f : α → β → γ) :
(∀ (a : α) (b₁ b₂ : β), s b₁ b₂f a b₁ = f a b₂)(∀ (a₁ a₂ : α) (b : β), r a₁ a₂f a₁ b = f a₂ b) → γ

Descends a function f : α → β → γ to quotients of α and β and applies it.

Equations
@[simp]
theorem quot.lift_on₂_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} (a : α) (b : β) (f : α → β → γ) (hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂f a b₁ = f a b₂) (hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂f a₁ b = f a₂ b) :
(quot.mk r a).lift_on₂ (quot.mk s b) f hr hs = f a b

def quot.map₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : α → β → γ) :
(∀ (a : α) (b₁ b₂ : β), s b₁ b₂t (f a b₁) (f a b₂))(∀ (a₁ a₂ : α) (b : β), r a₁ a₂t (f a₁ b) (f a₂ b))quot rquot squot t

Descends a function f : α → β → γ to quotients of α and β wih values in a quotient of γ.

Equations
@[simp]
theorem quot.map₂_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : α → β → γ) (hr : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂t (f a b₁) (f a b₂)) (hs : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂t (f a₁ b) (f a₂ b)) (a : α) (b : β) :
quot.map₂ f hr hs (quot.mk r a) (quot.mk s b) = quot.mk t (f a b)

theorem quot.induction_on₂ {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} {s : β → β → Prop} {δ : quot rquot s → Prop} (q₁ : quot r) (q₂ : quot s) :
(∀ (a : α) (b : β), δ (quot.mk r a) (quot.mk s b))δ q₁ q₂

theorem quot.induction_on₃ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} {δ : quot rquot squot t → Prop} (q₁ : quot r) (q₂ : quot s) (q₃ : quot t) :
(∀ (a : α) (b : β) (c : γ), δ (quot.mk r a) (quot.mk s b) (quot.mk t c))δ q₁ q₂ q₃

@[instance]
def quotient.inhabited {α : Sort u_1} [sa : setoid α] [inhabited α] :

Equations
def quotient.hrec_on₂ {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] {φ : quotient saquotient sbSort u_3} (qa : quotient sa) (qb : quotient sb) (f : Π (a : α) (b : β), φ a b) :
(∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂b₁ b₂f a₁ b₁ == f a₂ b₂)φ qa qb

Induction on two quotient arguments a and b, result type depends on ⟦a⟧ and ⟦b⟧.

Equations
def quotient.map {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] (f : α → β) :

Map a function f : α → β that sends equivalent elements to equivalent elements to a function quotient sa → quotient sb. Useful to define unary operations on quotients.

Equations
@[simp]
theorem quotient.map_mk {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] (f : α → β) (h : (has_equiv.equiv has_equiv.equiv) f f) (x : α) :

def quotient.map₂ {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] {γ : Sort u_4} [sc : setoid γ] (f : α → β → γ) :

Map a function f : α → β → γ that sends equivalent elements to equivalent elements to a function f : quotient sa → quotient sb → quotient sc. Useful to define binary operations on quotients.

Equations
theorem quot.eq {α : Type u_1} {r : α → α → Prop} {x y : α} :
quot.mk r x = quot.mk r y eqv_gen r x y

@[simp]
theorem quotient.eq {α : Sort u_1} [r : setoid α] {x y : α} :

theorem forall_quotient_iff {α : Type u_1} [r : setoid α] {p : quotient r → Prop} :
(∀ (a : quotient r), p a) ∀ (a : α), p a

@[simp]
theorem quotient.lift_beta {α : Sort u_1} {β : Sort u_2} [s : setoid α] (f : α → β) (h : ∀ (a b : α), a bf a = f b) (x : α) :

@[simp]
theorem quotient.lift_on_beta {α : Sort u_1} {β : Sort u_2} [s : setoid α] (f : α → β) (h : ∀ (a b : α), a bf a = f b) (x : α) :
x.lift_on f h = f x

@[simp]
theorem quotient.lift_on_beta₂ {α : Sort u_1} {β : Sort u_2} [setoid α] (f : α → α → β) (h : ∀ (a₁ a₂ b₁ b₂ : α), a₁ b₁a₂ b₂f a₁ a₂ = f b₁ b₂) (x y : α) :

theorem surjective_quot_mk {α : Sort u_1} (r : α → α → Prop) :

quot.mk r is a surjective function.

theorem surjective_quotient_mk (α : Sort u_1) [s : setoid α] :

quotient.mk is a surjective function.

def quot.out {α : Sort u_1} {r : α → α → Prop} :
quot r → α

Choose an element of the equivalence class using the axiom of choice. Sound but noncomputable.

Equations
meta def quot.unquot {α : Sort u_1} {r : α → α → Prop} :
quot r → α

Unwrap the VM representation of a quotient to obtain an element of the equivalence class. Computable but unsound.

@[simp]
theorem quot.out_eq {α : Sort u_1} {r : α → α → Prop} (q : quot r) :
quot.mk r q.out = q

def quotient.out {α : Sort u_1} [s : setoid α] :
quotient s → α

Choose an element of the equivalence class using the axiom of choice. Sound but noncomputable.

Equations
@[simp]
theorem quotient.out_eq {α : Sort u_1} [s : setoid α] (q : quotient s) :

theorem quotient.mk_out {α : Sort u_1} [s : setoid α] (a : α) :

@[instance]
def pi_setoid {ι : Sort u_1} {α : ι → Sort u_2} [Π (i : ι), setoid (α i)] :
setoid (Π (i : ι), α i)

Equations
def quotient.choice {ι : Type u_1} {α : ι → Type u_2} [S : Π (i : ι), setoid (α i)] :
(Π (i : ι), quotient (S i))quotient pi_setoid

Given a function f : Π i, quotient (S i), returns the class of functions Π i, α i sending each i to an element of the class f i.

Equations
theorem quotient.choice_eq {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), setoid (α i)] (f : Π (i : ι), α i) :
quotient.choice (λ (i : ι), f i) = f

theorem nonempty_quotient_iff {α : Sort u_1} (s : setoid α) :

def trunc  :
Sort uSort u

trunc α is the quotient of α by the always-true relation. This is related to the propositional truncation in HoTT, and is similar in effect to nonempty α, but unlike nonempty α, trunc α is data, so the VM representation is the same as α, and so this can be used to maintain computability.

Equations
theorem true_equivalence {α : Sort u_1} :
equivalence (λ (_x _x : α), true)

def trunc.mk {α : Sort u_1} :
α → trunc α

Constructor for trunc α

Equations
@[instance]
def trunc.inhabited {α : Sort u_1} [inhabited α] :

Equations
def trunc.lift {α : Sort u_1} {β : Sort u_2} (f : α → β) :
(∀ (a b : α), f a = f b)trunc α → β

Any constant function lifts to a function out of the truncation

Equations
theorem trunc.ind {α : Sort u_1} {β : trunc α → Prop} (a : ∀ (a : α), β (trunc.mk a)) (q : trunc α) :
β q

theorem trunc.lift_beta {α : Sort u_1} {β : Sort u_2} (f : α → β) (c : ∀ (a b : α), f a = f b) (a : α) :
trunc.lift f c (trunc.mk a) = f a

def trunc.lift_on {α : Sort u_1} {β : Sort u_2} (q : trunc α) (f : α → β) :
(∀ (a b : α), f a = f b) → β

Lift a constant function on q : trunc α.

Equations
theorem trunc.induction_on {α : Sort u_1} {β : trunc α → Prop} (q : trunc α) :
(∀ (a : α), β (trunc.mk a))β q

theorem trunc.exists_rep {α : Sort u_1} (q : trunc α) :
∃ (a : α), trunc.mk a = q

theorem trunc.induction_on₂ {α : Sort u_1} {β : Sort u_2} {C : trunc αtrunc β → Prop} (q₁ : trunc α) (q₂ : trunc β) :
(∀ (a : α) (b : β), C (trunc.mk a) (trunc.mk b))C q₁ q₂

theorem trunc.eq {α : Sort u_1} (a b : trunc α) :
a = b

@[instance]
def trunc.subsingleton {α : Sort u_1} :

def trunc.bind {α : Sort u_1} {β : Sort u_2} :
trunc α(α → trunc β)trunc β

The bind operator for the trunc monad.

Equations
def trunc.map {α : Sort u_1} {β : Sort u_2} :
(α → β)trunc αtrunc β

A function f : α → β defines a function map f : trunc α → trunc β.

Equations
@[instance]

Equations
def trunc.rec {α : Sort u_1} {C : trunc αSort u_3} (f : Π (a : α), C (trunc.mk a)) (h : ∀ (a b : α), eq.rec (f a) _ = f b) (q : trunc α) :
C q

Recursion/induction principle for trunc.

Equations
def trunc.rec_on {α : Sort u_1} {C : trunc αSort u_3} (q : trunc α) (f : Π (a : α), C (trunc.mk a)) :
(∀ (a b : α), eq.rec (f a) _ = f b)C q

A version of trunc.rec taking q : trunc α as the first argument.

Equations
def trunc.rec_on_subsingleton {α : Sort u_1} {C : trunc αSort u_3} [∀ (a : α), subsingleton (C (trunc.mk a))] (q : trunc α) :
(Π (a : α), C (trunc.mk a))C q

A version of trunc.rec_on assuming the codomain is a subsingleton.

Equations
def trunc.out {α : Sort u_1} :
trunc α → α

Noncomputably extract a representative of trunc α (using the axiom of choice).

Equations
@[simp]
theorem trunc.out_eq {α : Sort u_1} (q : trunc α) :

theorem nonempty_of_trunc {α : Sort u_1} :
trunc αnonempty α

def quotient.mk' {α : Sort u_1} {s₁ : setoid α} :
α → quotient s₁

A version of quotient.mk taking {s : setoid α} as an implicit argument instead of an instance argument.

Equations

quotient.mk' is a surjective function.

def quotient.lift_on' {α : Sort u_1} {φ : Sort u_4} {s₁ : setoid α} (q : quotient s₁) (f : α → φ) :
(∀ (a b : α), setoid.r a bf a = f b) → φ

A version of quotient.lift_on taking {s : setoid α} as an implicit argument instead of an instance argument.

Equations
def quotient.lift_on₂' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : setoid α} {s₂ : setoid β} (q₁ : quotient s₁) (q₂ : quotient s₂) (f : α → β → γ) :
(∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), setoid.r a₁ b₁setoid.r a₂ b₂f a₁ a₂ = f b₁ b₂) → γ

A version of quotient.lift_on₂ taking {s₁ : setoid α} {s₂ : setoid β} as implicit arguments instead of instance arguments.

Equations
theorem quotient.ind' {α : Sort u_1} {s₁ : setoid α} {p : quotient s₁ → Prop} (h : ∀ (a : α), p (quotient.mk' a)) (q : quotient s₁) :
p q

A version of quotient.ind taking {s : setoid α} as an implicit argument instead of an instance argument.

theorem quotient.ind₂' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} {p : quotient s₁quotient s₂ → Prop} (h : ∀ (a₁ : α) (a₂ : β), p (quotient.mk' a₁) (quotient.mk' a₂)) (q₁ : quotient s₁) (q₂ : quotient s₂) :
p q₁ q₂

A version of quotient.ind₂ taking {s₁ : setoid α} {s₂ : setoid β} as implicit arguments instead of instance arguments.

theorem quotient.induction_on' {α : Sort u_1} {s₁ : setoid α} {p : quotient s₁ → Prop} (q : quotient s₁) :
(∀ (a : α), p (quotient.mk' a))p q

A version of quotient.induction_on taking {s : setoid α} as an implicit argument instead of an instance argument.

theorem quotient.induction_on₂' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} {p : quotient s₁quotient s₂ → Prop} (q₁ : quotient s₁) (q₂ : quotient s₂) :
(∀ (a₁ : α) (a₂ : β), p (quotient.mk' a₁) (quotient.mk' a₂))p q₁ q₂

A version of quotient.induction_on₂ taking {s₁ : setoid α} {s₂ : setoid β} as implicit arguments instead of instance arguments.

theorem quotient.induction_on₃' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ} {p : quotient s₁quotient s₂quotient s₃ → Prop} (q₁ : quotient s₁) (q₂ : quotient s₂) (q₃ : quotient s₃) :
(∀ (a₁ : α) (a₂ : β) (a₃ : γ), p (quotient.mk' a₁) (quotient.mk' a₂) (quotient.mk' a₃))p q₁ q₂ q₃

A version of quotient.induction_on₃ taking {s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ} as implicit arguments instead of instance arguments.

def quotient.hrec_on' {α : Sort u_1} {s₁ : setoid α} {φ : quotient s₁Sort u_2} (qa : quotient s₁) (f : Π (a : α), φ (quotient.mk' a)) :
(∀ (a₁ a₂ : α), a₁ a₂f a₁ == f a₂)φ qa

Recursion on a quotient argument a, result type depends on ⟦a⟧.

Equations
@[simp]
theorem quotient.hrec_on'_mk' {α : Sort u_1} {s₁ : setoid α} {φ : quotient s₁Sort u_2} (f : Π (a : α), φ (quotient.mk' a)) (c : ∀ (a₁ a₂ : α), a₁ a₂f a₁ == f a₂) (x : α) :
(quotient.mk' x).hrec_on' f c = f x

def quotient.hrec_on₂' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} {φ : quotient s₁quotient s₂Sort u_3} (qa : quotient s₁) (qb : quotient s₂) (f : Π (a : α) (b : β), φ (quotient.mk' a) (quotient.mk' b)) :
(∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂b₁ b₂f a₁ b₁ == f a₂ b₂)φ qa qb

Recursion on two quotient arguments a and b, result type depends on ⟦a⟧ and ⟦b⟧.

Equations
@[simp]
theorem quotient.hrec_on₂'_mk' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} {φ : quotient s₁quotient s₂Sort u_3} (f : Π (a : α) (b : β), φ (quotient.mk' a) (quotient.mk' b)) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂b₁ b₂f a₁ b₁ == f a₂ b₂) (x : α) (qb : quotient s₂) :
(quotient.mk' x).hrec_on₂' qb f c = qb.hrec_on' (f x) _

def quotient.map' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} (f : α → β) :

Map a function f : α → β that sends equivalent elements to equivalent elements to a function quotient sa → quotient sb. Useful to define unary operations on quotients.

Equations
@[simp]
theorem quotient.map'_mk' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} (f : α → β) (h : (has_equiv.equiv has_equiv.equiv) f f) (x : α) :

def quotient.map₂' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ} (f : α → β → γ) :

A version of quotient.map₂ using curly braces and unification.

Equations
@[simp]
theorem quotient.map₂'_mk' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ} (f : α → β → γ) (h : (has_equiv.equiv has_equiv.equiv has_equiv.equiv) f f) (x : α) :

theorem quotient.exact' {α : Sort u_1} {s₁ : setoid α} {a b : α} :

theorem quotient.sound' {α : Sort u_1} {s₁ : setoid α} {a b : α} :

@[simp]
theorem quotient.eq' {α : Sort u_1} {s₁ : setoid α} {a b : α} :

def quotient.out' {α : Sort u_1} {s₁ : setoid α} :
quotient s₁ → α

A version of quotient.out taking {s₁ : setoid α} as an implicit argument instead of an instance argument.

Equations
@[simp]
theorem quotient.out_eq' {α : Sort u_1} {s₁ : setoid α} (q : quotient s₁) :

theorem quotient.mk_out' {α : Sort u_1} {s₁ : setoid α} (a : α) :