mathlib3 documentation

data.quot

Quotient types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Tags #

quotient

source
theorem setoid.ext {α : Sort u_1} {s t : setoid α} :
(∀ (a b : α), setoid.r a b ↔ setoid.r a b) → s = t
source
@[protected, instance]
def quot.inhabited {α : Sort u_1} (r : α → α → Prop) [inhabited α] :
inhabited (quot r)
Equations
source
@[protected, instance]
def quot.subsingleton {α : Sort u_1} {ra : α → α → Prop} [subsingleton α] :
subsingleton (quot ra)
source
@[protected]
def quot.hrec_on₂ {α : Sort u_1} {β : Sort u_2} {ra : α → α → Prop} {rb : β → β → Prop} {φ : quot ra → quot rb → Sort u_3} (qa : quot ra) (qb : quot rb) (f : Π (a : α) (b : β), φ (quot.mk ra a) (quot.mk rb b)) (ca : ∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂ → f a₁ b == f a₂ b) (cb : ∀ {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
source
@[protected]
def quot.map {α : Sort u_1} {β : Sort u_2} {ra : α → α → Prop} {rb : β → β → Prop} (f : α → β) (h : (ra ⇒ rb) f f) :
quot ra → quot 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)) _
source
@[protected]
def quot.map_right {α : Sort u_1} {ra ra' : α → α → Prop} (h : ∀ (a₁ a₂ : α), ra a₁ a₂ → ra' a₁ a₂) :
quot ra → quot ra'

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

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

Weaken the relation of a quotient. This is the same as quot.map id.

Equations
source
theorem quot.factor_mk_eq {α : Type u_1} (r s : α → α → Prop) (h : ∀ (x y : α), r x y → s x y) :
quot.factor r s h ∘ quot.mk r = quot.mk s
source
theorem quot.lift_mk {α : Sort u_1} {γ : Sort u_4} {r : α → α → Prop} (f : α → γ) (h : ∀ (a₁ a₂ : α), r a₁ a₂ → f a₁ = f a₂) (a : α) :
quot.lift f h (quot.mk r a) = f a

Alias of quot.lift_beta.

source
@[simp]
theorem quot.lift_on_mk {α : Sort u_1} {γ : Sort u_4} {r : α → α → Prop} (a : α) (f : α → γ) (h : ∀ (a₁ a₂ : α), r a₁ a₂ → f a₁ = f a₂) :
(quot.mk r a).lift_on f h = f a
source
@[simp]
theorem quot.surjective_lift {α : Sort u_1} {γ : Sort u_4} {r : α → α → Prop} {f : α → γ} (h : ∀ (a₁ a₂ : α), r a₁ a₂ → f a₁ = f a₂) :
function.surjective (quot.lift f h) ↔ function.surjective f
source
@[protected, reducible]
def quot.lift₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} (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) (q₁ : quot r) (q₂ : quot 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₂
source
@[simp]
theorem quot.lift₂_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} (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) (a : α) (b : β) :
quot.lift₂ f hr hs (quot.mk r a) (quot.mk s b) = f a b
source
@[protected, reducible]
def quot.lift_on₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} (p : quot r) (q : quot s) (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) :
γ

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

Equations
source
@[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
source
@[protected]
def quot.map₂ {α : 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)) (q₁ : quot r) (q₂ : quot s) :
quot t

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

Equations
source
@[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)
source
@[protected, reducible]
def quot.rec_on_subsingleton₂ {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} {s : β → β → Prop} {φ : quot r → quot s → Sort u_3} [h : ∀ (a : α) (b : β), subsingleton (φ (quot.mk r a) (quot.mk s b))] (q₁ : quot r) (q₂ : quot s) (f : Π (a : α) (b : β), φ (quot.mk r a) (quot.mk s b)) :
φ q₁ q₂

A binary version of quot.rec_on_subsingleton.

Equations
source
@[protected]
theorem quot.induction_on₂ {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} {s : β → β → Prop} {δ : quot r → quot s → Prop} (q₁ : quot r) (q₂ : quot s) (h : ∀ (a : α) (b : β), δ (quot.mk r a) (quot.mk s b)) :
δ q₁ q₂
source
@[protected]
theorem quot.induction_on₃ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} {δ : quot r → quot s → quot t → Prop} (q₁ : quot r) (q₂ : quot s) (q₃ : quot t) (h : ∀ (a : α) (b : β) (c : γ), δ (quot.mk r a) (quot.mk s b) (quot.mk t c)) :
δ q₁ q₂ q₃
source
@[protected, instance]
def quot.lift.decidable_pred {α : Sort u_1} (r : α → α → Prop) (f : α → Prop) (h : ∀ (a b : α), r a b → f a = f b) [hf : decidable_pred f] :
decidable_pred (quot.lift f h)
Equations
source
@[protected, instance]
def quot.lift₂.decidable_pred {α : Sort u_1} {β : Sort u_2} (r : α → α → Prop) (s : β → β → Prop) (f : α → β → Prop) (ha : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → f a b₁ = f a b₂) (hb : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → f a₁ b = f a₂ b) [hf : Π (a : α), decidable_pred (f a)] (q₁ : quot r) :
decidable_pred (quot.lift₂ f ha hb q₁)

Note that this provides decidable_rel (quot.lift₂ f ha hb) when α = β.

Equations
source
@[protected, instance]
def quot.lift_on.decidable {α : Sort u_1} (r : α → α → Prop) (q : quot r) (f : α → Prop) (h : ∀ (a b : α), r a b → f a = f b) [decidable_pred f] :
decidable (q.lift_on f h)
Equations
source
@[protected, instance]
def quot.lift_on₂.decidable {α : Sort u_1} {β : Sort u_2} (r : α → α → Prop) (s : β → β → Prop) (q₁ : quot r) (q₂ : quot s) (f : α → β → Prop) (ha : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → f a b₁ = f a b₂) (hb : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → f a₁ b = f a₂ b) [Π (a : α), decidable_pred (f a)] :
decidable (q₁.lift_on₂ q₂ f ha hb)
Equations
source
@[protected, instance]
def quotient.inhabited {α : Sort u_1} (s : setoid α) [inhabited α] :
inhabited (quotient s)
Equations
source
@[protected, instance]
def quotient.subsingleton {α : Sort u_1} (s : setoid α) [subsingleton α] :
subsingleton (quotient s)
source
@[protected, instance]
def quotient.has_equiv.equiv.is_equiv {α : Type u_1} [setoid α] :
is_equiv α has_equiv.equiv
source
@[protected]
def quotient.hrec_on₂ {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] {φ : quotient sa → quotient sb → Sort u_3} (qa : quotient sa) (qb : quotient sb) (f : Π (a : α) (b : β), φ ⟦a⟧ ⟦b⟧) (c : ∀ (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
source
@[protected]
def quotient.map {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] (f : α → β) (h : (has_equiv.equiv ⇒ has_equiv.equiv) f f) :
quotient sa → quotient sb

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
source
@[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 : α) :
quotient.map f h ⟦x⟧ = ⟦f x⟧
source
@[protected]
def quotient.map₂ {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] {γ : Sort u_4} [sc : setoid γ] (f : α → β → γ) (h : (has_equiv.equiv ⇒ has_equiv.equiv ⇒ has_equiv.equiv) f f) :
quotient sa → quotient sb → quotient sc

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
source
@[simp]
theorem quotient.map₂_mk {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] {γ : Sort u_4} [sc : setoid γ] (f : α → β → γ) (h : (has_equiv.equiv ⇒ has_equiv.equiv ⇒ has_equiv.equiv) f f) (x : α) (y : β) :
quotient.map₂ f h ⟦x⟧ ⟦y⟧ = ⟦f x y⟧
source
@[protected, instance]
def quotient.lift.decidable_pred {α : Sort u_1} [sa : setoid α] (f : α → Prop) (h : ∀ (a b : α), a ≈ b → f a = f b) [decidable_pred f] :
decidable_pred (quotient.lift f h)
Equations
source
@[protected, instance]
def quotient.lift₂.decidable_pred {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] (f : α → β → Prop) (h : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) [hf : Π (a : α), decidable_pred (f a)] (q₁ : quotient sa) :
decidable_pred (quotient.lift₂ f h q₁)

Note that this provides decidable_rel (quotient.lift₂ f h) when α = β.

Equations
source
@[protected, instance]
def quotient.lift_on.decidable {α : Sort u_1} [sa : setoid α] (q : quotient sa) (f : α → Prop) (h : ∀ (a b : α), a ≈ b → f a = f b) [decidable_pred f] :
decidable (q.lift_on f h)
Equations
source
@[protected, instance]
def quotient.lift_on₂.decidable {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] (q₁ : quotient sa) (q₂ : quotient sb) (f : α → β → Prop) (h : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) [Π (a : α), decidable_pred (f a)] :
decidable (q₁.lift_on₂ q₂ f h)
Equations
source
theorem quot.eq {α : Type u_1} {r : α → α → Prop} {x y : α} :
quot.mk r x = quot.mk r y ↔ eqv_gen r x y
source
@[simp]
theorem quotient.eq {α : Sort u_1} [r : setoid α] {x y : α} :
⟦x⟧ = ⟦y⟧ ↔ x ≈ y
source
theorem forall_quotient_iff {α : Type u_1} [r : setoid α] {p : quotient r → Prop} :
(∀ (a : quotient r), p a) ↔ ∀ (a : α), p ⟦a⟧
source
@[simp]
theorem quotient.lift_mk {α : Sort u_1} {β : Sort u_2} [s : setoid α] (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b) (x : α) :
quotient.lift f h ⟦x⟧ = f x
source
@[simp]
theorem quotient.lift_comp_mk {α : Sort u_1} {β : Sort u_2} [setoid α] (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b) :
quotient.lift f h ∘ quotient.mk = f
source
@[simp]
theorem quotient.lift₂_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [setoid α] [setoid β] (f : α → β → γ) (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) (a : α) (b : β) :
quotient.lift₂ f h ⟦a⟧ ⟦b⟧ = f a b
source
@[simp]
theorem quotient.lift_on_mk {α : Sort u_1} {β : Sort u_2} [s : setoid α] (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b) (x : α) :
⟦x⟧.lift_on f h = f x
source
@[simp]
theorem quotient.lift_on₂_mk {α : 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 : α) :
⟦x⟧.lift_on₂ ⟦y⟧ f h = f x y
source
theorem surjective_quot_mk {α : Sort u_1} (r : α → α → Prop) :
function.surjective (quot.mk r)

quot.mk r is a surjective function.

source
theorem surjective_quotient_mk (α : Sort u_1) [s : setoid α] :
function.surjective quotient.mk

quotient.mk is a surjective function.

source
noncomputable def quot.out {α : Sort u_1} {r : α → α → Prop} (q : quot r) :
α

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

Equations
source
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.

source
@[simp]
theorem quot.out_eq {α : Sort u_1} {r : α → α → Prop} (q : quot r) :
quot.mk r q.out = q
source
noncomputable 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
source
@[simp]
theorem quotient.out_eq {α : Sort u_1} [s : setoid α] (q : quotient s) :
⟦q.out⟧ = q
source
theorem quotient.mk_out {α : Sort u_1} [s : setoid α] (a : α) :
⟦a⟧.out ≈ a
source
theorem quotient.mk_eq_iff_out {α : Sort u_1} [s : setoid α] {x : α} {y : quotient s} :
⟦x⟧ = y ↔ x ≈ y.out
source
theorem quotient.eq_mk_iff_out {α : Sort u_1} [s : setoid α] {x : quotient s} {y : α} :
x = ⟦y⟧ ↔ x.out ≈ y
source
@[simp]
theorem quotient.out_equiv_out {α : Sort u_1} {s : setoid α} {x y : quotient s} :
x.out ≈ y.out ↔ x = y
source
theorem quotient.out_injective {α : Sort u_1} {s : setoid α} :
function.injective quotient.out
source
@[simp]
theorem quotient.out_inj {α : Sort u_1} {s : setoid α} {x y : quotient s} :
x.out = y.out ↔ x = y
source
@[protected, instance]
def pi_setoid {ι : Sort u_1} {α : ι → Sort u_2} [Π (i : ι), setoid (α i)] :
setoid (Π (i : ι), α i)
Equations
source
noncomputable def quotient.choice {ι : Type u_1} {α : ι → Type u_2} [S : Π (i : ι), setoid (α i)] (f : Π (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
source
@[simp]
theorem quotient.choice_eq {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), setoid (α i)] (f : Π (i : ι), α i) :
quotient.choice (λ (i : ι), ⟦f i⟧) = ⟦f⟧
source
theorem quotient.induction_on_pi {ι : Type u_1} {α : ι → Sort u_2} [s : Π (i : ι), setoid (α i)] {p : (Π (i : ι), quotient (s i)) → Prop} (f : Π (i : ι), quotient (s i)) (h : ∀ (a : Π (i : ι), α i), p (λ (i : ι), ⟦a i⟧)) :
p f
source
theorem nonempty_quotient_iff {α : Sort u_1} (s : setoid α) :
nonempty (quotient s) ↔ nonempty α

Truncation #

source
theorem true_equivalence {α : Sort u_1} :
equivalence (λ (_x _x : α), true)
source
def true_setoid {α : Sort u_1} :
setoid α

Always-true relation as a setoid.

Note that in later files the preferred spelling is ⊤ : setoid α.

Equations
source
def trunc (α : Sort u) :
Sort 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
Instances for trunc
source
def trunc.mk {α : Sort u_1} (a : α) :
trunc α

Constructor for trunc α

Equations
source
@[protected, instance]
def trunc.inhabited {α : Sort u_1} [inhabited α] :
inhabited (trunc α)
Equations
source
def trunc.lift {α : Sort u_1} {β : Sort u_2} (f : α → β) (c : ∀ (a b : α), f a = f b) :
trunc α → β

Any constant function lifts to a function out of the truncation

Equations
source
theorem trunc.ind {α : Sort u_1} {β : trunc α → Prop} :
(∀ (a : α), β (trunc.mk a)) → ∀ (q : trunc α), β q
source
@[protected]
theorem trunc.lift_mk {α : Sort u_1} {β : Sort u_2} (f : α → β) (c : ∀ (a b : α), f a = f b) (a : α) :
trunc.lift f c (trunc.mk a) = f a
source
@[protected, reducible]
def trunc.lift_on {α : Sort u_1} {β : Sort u_2} (q : trunc α) (f : α → β) (c : ∀ (a b : α), f a = f b) :
β

Lift a constant function on q : trunc α.

Equations
source
@[protected]
theorem trunc.induction_on {α : Sort u_1} {β : trunc α → Prop} (q : trunc α) (h : ∀ (a : α), β (trunc.mk a)) :
β q
source
theorem trunc.exists_rep {α : Sort u_1} (q : trunc α) :
∃ (a : α), trunc.mk a = q
source
@[protected]
theorem trunc.induction_on₂ {α : Sort u_1} {β : Sort u_2} {C : trunc α → trunc β → Prop} (q₁ : trunc α) (q₂ : trunc β) (h : ∀ (a : α) (b : β), C (trunc.mk a) (trunc.mk b)) :
C q₁ q₂
source
@[protected]
theorem trunc.eq {α : Sort u_1} (a b : trunc α) :
a = b
source
@[protected, instance]
def trunc.subsingleton {α : Sort u_1} :
subsingleton (trunc α)
source
def trunc.bind {α : Sort u_1} {β : Sort u_2} (q : trunc α) (f : α → trunc β) :
trunc β

The bind operator for the trunc monad.

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

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

Equations
source
@[protected, instance]
def trunc.monad  :
monad trunc
Equations
source
@[protected, instance]
def trunc.is_lawful_monad  :
is_lawful_monad trunc
source
@[protected, reducible]
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
source
@[protected, reducible]
def trunc.rec_on {α : Sort u_1} {C : trunc α → Sort u_3} (q : trunc α) (f : Π (a : α), C (trunc.mk a)) (h : ∀ (a b : α), eq.rec (f a) _ = f b) :
C q

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

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

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

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

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

Equations
source
@[simp]
theorem trunc.out_eq {α : Sort u_1} (q : trunc α) :
trunc.mk q.out = q
source
@[protected]
theorem trunc.nonempty {α : Sort u_1} (q : trunc α) :
nonempty α

quotient with implicit setoid #

Versions of quotient definitions and lemmas ending in ' use unification instead of typeclass inference for inferring the setoid argument. This is useful when there are several different quotient relations on a type, for example quotient groups, rings and modules.

source
@[protected]
def quotient.mk' {α : Sort u_1} {s₁ : setoid α} (a : α) :
quotient s₁

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

Equations
source
theorem quotient.surjective_quotient_mk' {α : Sort u_1} {s₁ : setoid α} :
function.surjective quotient.mk'

quotient.mk' is a surjective function.

source
@[protected, reducible]
def quotient.lift_on' {α : Sort u_1} {φ : Sort u_4} {s₁ : setoid α} (q : quotient s₁) (f : α → φ) (h : ∀ (a b : α), setoid.r a b → f a = f b) :
φ

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

Equations
source
@[protected, simp]
theorem quotient.lift_on'_mk' {α : Sort u_1} {φ : Sort u_4} {s₁ : setoid α} (f : α → φ) (h : ∀ (a b : α), setoid.r a b → f a = f b) (x : α) :
(quotient.mk' x).lift_on' f h = f x
source
@[simp]
theorem quotient.surjective_lift_on' {α : Sort u_1} {φ : Sort u_4} {s₁ : setoid α} {f : α → φ} (h : ∀ (a b : α), setoid.r a b → f a = f b) :
function.surjective (λ (x : quotient s₁), x.lift_on' f h) ↔ function.surjective f
source
@[protected, reducible]
def quotient.lift_on₂' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : setoid α} {s₂ : setoid β} (q₁ : quotient s₁) (q₂ : quotient s₂) (f : α → β → γ) (h : ∀ (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
source
@[protected, simp]
theorem quotient.lift_on₂'_mk' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : setoid α} {s₂ : setoid β} (f : α → β → γ) (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), setoid.r a₁ b₁ → setoid.r a₂ b₂ → f a₁ a₂ = f b₁ b₂) (a : α) (b : β) :
(quotient.mk' a).lift_on₂' (quotient.mk' b) f h = f a b
source
@[protected]
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.

source
@[protected]
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.

source
@[protected]
theorem quotient.induction_on' {α : Sort u_1} {s₁ : setoid α} {p : quotient s₁ → Prop} (q : quotient s₁) (h : ∀ (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.

source
@[protected]
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₂) (h : ∀ (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.

source
@[protected]
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₃) (h : ∀ (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.

source
@[protected]
def quotient.rec_on_subsingleton' {α : Sort u_1} {s₁ : setoid α} {φ : quotient s₁ → Sort u_2} [h : ∀ (a : α), subsingleton (φ ⟦a⟧)] (q : quotient s₁) (f : Π (a : α), φ (quotient.mk' a)) :
φ q

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

Equations
source
@[protected, reducible]
def quotient.rec_on_subsingleton₂' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} {φ : quotient s₁ → quotient s₂ → Sort u_3} [h : ∀ (a : α) (b : β), subsingleton (φ ⟦a⟧ ⟦b⟧)] (q₁ : quotient s₁) (q₂ : quotient s₂) (f : Π (a₁ : α) (a₂ : β), φ (quotient.mk' a₁) (quotient.mk' a₂)) :
φ q₁ q₂

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

Equations
source
@[protected]
def quotient.hrec_on' {α : Sort u_1} {s₁ : setoid α} {φ : quotient s₁ → Sort u_2} (qa : quotient s₁) (f : Π (a : α), φ (quotient.mk' a)) (c : ∀ (a₁ a₂ : α), a₁ ≈ a₂ → f a₁ == f a₂) :
φ qa

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

Equations
source
@[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
source
@[protected]
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)) (c : ∀ (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
source
@[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) _
source
@[protected]
def quotient.map' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} (f : α → β) (h : (setoid.r ⇒ setoid.r) f f) :
quotient s₁ → quotient s₂

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
source
@[simp]
theorem quotient.map'_mk' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} (f : α → β) (h : (setoid.r ⇒ setoid.r) f f) (x : α) :
quotient.map' f h (quotient.mk' x) = quotient.mk' (f x)
source
@[protected]
def quotient.map₂' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ} (f : α → β → γ) (h : (setoid.r ⇒ setoid.r ⇒ setoid.r) f f) :
quotient s₁ → quotient s₂ → quotient s₃

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

Equations
source
@[simp]
theorem quotient.map₂'_mk' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ} (f : α → β → γ) (h : (setoid.r ⇒ setoid.r ⇒ setoid.r) f f) (x : α) :
quotient.map₂' f h (quotient.mk' x) = quotient.map' (f x) _
source
theorem quotient.exact' {α : Sort u_1} {s₁ : setoid α} {a b : α} :
quotient.mk' a = quotient.mk' b → setoid.r a b
source
theorem quotient.sound' {α : Sort u_1} {s₁ : setoid α} {a b : α} :
setoid.r a b → quotient.mk' a = quotient.mk' b
source
@[protected, simp]
theorem quotient.eq' {α : Sort u_1} {s₁ : setoid α} {a b : α} :
quotient.mk' a = quotient.mk' b ↔ setoid.r a b
source
noncomputable def quotient.out' {α : Sort u_1} {s₁ : setoid α} (a : quotient s₁) :
α

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

Equations
source
@[simp]
theorem quotient.out_eq' {α : Sort u_1} {s₁ : setoid α} (q : quotient s₁) :
quotient.mk' q.out' = q
source
theorem quotient.mk_out' {α : Sort u_1} {s₁ : setoid α} (a : α) :
setoid.r (quotient.mk' a).out' a
source
@[protected]
theorem quotient.mk'_eq_mk {α : Sort u_1} [setoid α] (x : α) :
quotient.mk' x = ⟦x⟧
source
@[protected, simp]
theorem quotient.lift_on'_mk {α : Sort u_1} {β : Sort u_2} [setoid α] (x : α) (f : α → β) (h : ∀ (a b : α), setoid.r a b → f a = f b) :
⟦x⟧.lift_on' f h = f x
source
@[protected, simp]
theorem quotient.lift_on₂'_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [setoid α] [setoid β] (f : α → β → γ) (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), setoid.r a₁ b₁ → setoid.r a₂ b₂ → f a₁ a₂ = f b₁ b₂) (a : α) (b : β) :
⟦a⟧.lift_on₂' ⟦b⟧ f h = f a b
source
@[simp]
theorem quotient.map'_mk {α : Sort u_1} {β : Sort u_2} [setoid α] [setoid β] (f : α → β) (h : (setoid.r ⇒ setoid.r) f f) (x : α) :
quotient.map' f h ⟦x⟧ = ⟦f x⟧
source
@[protected, instance]
def quotient.lift_on'.decidable {α : Sort u_1} {s₁ : setoid α} (q : quotient s₁) (f : α → Prop) (h : ∀ (a b : α), setoid.r a b → f a = f b) [decidable_pred f] :
decidable (q.lift_on' f h)
Equations
source
@[protected, instance]
def quotient.lift_on₂'.decidable {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} (q₁ : quotient s₁) (q₂ : quotient s₂) (f : α → β → Prop) (h : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), setoid.r a₁ a₂ → setoid.r b₁ b₂ → f a₁ b₁ = f a₂ b₂) [Π (a : α), decidable_pred (f a)] :
decidable (q₁.lift_on₂' q₂ f h)
Equations