Quotient types

This module extends the core library's treatment of quotient types (Init.Core).

Tags

quotient

instance Setoid.instCoeFunForallForallProp_mathlib {α : Sort u_1} : CoeFun (Setoid α) fun (x : Setoid α) => α → α → Prop

When writing a lemma about someSetoid x y (which uses this instance), call it someSetoid_apply not someSetoid_r.

Equations

• Setoid.instCoeFunForallForallProp_mathlib = { coe := @Setoid.r α }

theorem Setoid.ext {α : Sort u_3} {s : Setoid α} {t : Setoid α} : (∀ (a b : α), s a b ↔ t a b) → s = t

theorem Quot.induction_on {α : Sort u_4} {r : α → α → Prop} {β : Quot r → Prop} (q : Quot r) (h : ∀ (a : α), β (Quot.mk r a)) : β q

instance Quot.instInhabited_mathlib {α : Sort u_1} (r : α → α → Prop) [Inhabited α] : Inhabited (Quot r)

Equations

• Quot.instInhabited_mathlib r = { default := Quot.mk r default }

instance Quot.Subsingleton {α : Sort u_1} {ra : α → α → Prop} [Subsingleton α] : Subsingleton (Quot ra)

Equations

• ⋯ = ⋯

@[deprecated Quot.recOn]

def Quot.recOn' {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), ⋯ ▸ f a = f b) : motive q

Alias of Quot.recOn.

---

Dependent recursion principle for Quot. This constructor can be tricky to use, so you should consider the simpler versions if they apply:

• Quot.lift, for nondependent functions
• Quot.ind, for theorems / proofs of propositions about quotients
• Quot.recOnSubsingleton, when the target type is a Subsingleton
• Quot.hrecOn, which uses HEq (f a) (f b) instead of a sound p ▸ f a = f b assummption

Equations

• @Quot.recOn' = @Quot.recOn

@[deprecated Quot.recOnSubsingleton]

def Quot.recOnSubsingleton' {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} [h : ∀ (a : α), Subsingleton (motive (Quot.mk r a))] (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) : motive q

Alias of Quot.recOnSubsingleton.

---

Dependent induction principle for a quotient, when the target type is a Subsingleton. In this case the quotient's side condition is trivial so any function can be lifted.

Equations

• @Quot.recOnSubsingleton' = @Quot.recOnSubsingleton

instance Quot.instUnique {α : Sort u_1} {ra : α → α → Prop} [Unique α] : Unique (Quot ra)

Equations

• Quot.instUnique = Unique.mk' (Quot ra)

def Quot.hrecOn₂ {α : 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₂ → HEq (f a₁ b) (f a₂ b)) (cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂ → HEq (f a b₁) (f a b₂)) : φ qa qb

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

Equations

• qa.hrecOn₂ qb f ca cb = Quot.hrecOn qa (fun (a : α) => Quot.hrecOn qb (f a) ⋯) ⋯

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 (fun (x : α) => Quot.mk rb (f x)) ⋯

def Quot.mapRight {α : Sort u_1} {ra : α → α → Prop} {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

• Quot.mapRight h = Quot.map id h

def Quot.factor {α : Type u_4} (r : α → α → Prop) (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

• Quot.factor r s h = Quot.lift (Quot.mk s) ⋯

theorem Quot.factor_mk_eq {α : Type u_4} (r : α → α → Prop) (s : α → α → Prop) (h : ∀ (x y : α), r x y → s x y) : Quot.factor r s h ∘ Quot.mk r = Quot.mk s

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

theorem Quot.liftOn_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).liftOn f h = f a

@[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

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 (fun (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} (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

def Quot.liftOn₂ {α : 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

• p.liftOn₂ q f hr hs = Quot.lift₂ f hr hs p q

@[simp]

theorem Quot.liftOn₂_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).liftOn₂ (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 : α → β → γ) (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 β with values in a quotient of γ.

Equations

• Quot.map₂ f hr hs q₁ q₂ = Quot.lift₂ (fun (a : α) (b : β) => Quot.mk t (f a b)) ⋯ ⋯ q₁ q₂

@[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)

def Quot.recOnSubsingleton₂ {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} {s : β → β → Prop} {φ : Quot r → Quot s → Sort u_5} [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.recOnSubsingleton.

Equations

• q₁.recOnSubsingleton₂ q₂ f = Quot.recOnSubsingleton q₁ fun (a : α) => Quot.recOnSubsingleton q₂ fun (b : β) => f a b

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₂

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₃

instance Quot.lift.decidablePred {α : Sort u_1} (r : α → α → Prop) (f : α → Prop) (h : ∀ (a b : α), r a b → f a = f b) [hf : DecidablePred f] : DecidablePred (Quot.lift f h)

Equations

• Quot.lift.decidablePred r f h q = Quot.recOnSubsingleton q hf

instance Quot.lift₂.decidablePred {α : 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 : α) → DecidablePred (f a)] (q₁ : Quot r) : DecidablePred (Quot.lift₂ f ha hb q₁)

Note that this provides DecidableRel (Quot.Lift₂ f ha hb) when α = β.

Equations

• Quot.lift₂.decidablePred r s f ha hb q₁ q₂ = q₁.recOnSubsingleton₂ q₂ hf

instance Quot.instDecidableLiftOnOfDecidablePred_mathlib {α : Sort u_1} (r : α → α → Prop) (q : Quot r) (f : α → Prop) (h : ∀ (a b : α), r a b → f a = f b) [DecidablePred f] : Decidable (q.liftOn f h)

Equations

• Quot.instDecidableLiftOnOfDecidablePred_mathlib r q f h = Quot.lift.decidablePred r f h q

instance Quot.instDecidableLiftOn₂OfDecidablePred {α : 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 : α) → DecidablePred (f a)] : Decidable (q₁.liftOn₂ q₂ f ha hb)

Equations

• Quot.instDecidableLiftOn₂OfDecidablePred r s q₁ q₂ f ha hb = Quot.lift₂.decidablePred r s f ha hb q₁ q₂

def Quotient.«term⟦_⟧» : Lean.ParserDescr

The canonical quotient map into a Quotient.

Equations

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

def Quotient.«term⟦_⟧».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

instance Quotient.instInhabitedQuotient {α : Sort u_1} (s : Setoid α) [Inhabited α] : Inhabited (Quotient s)

Equations

• Quotient.instInhabitedQuotient s = { default := ⟦default⟧ }

instance Quotient.instSubsingletonQuotient {α : Sort u_1} (s : Setoid α) [Subsingleton α] : Subsingleton (Quotient s)

Equations

• ⋯ = ⋯

instance Quotient.instUniqueQuotient {α : Sort u_1} (s : Setoid α) [Unique α] : Unique (Quotient s)

Equations

• Quotient.instUniqueQuotient s = Unique.mk' (Quotient s)

instance Quotient.instIsEquivEquiv {α : Type u_4} [Setoid α] : IsEquiv α fun (x1 x2 : α) => x1 ≈ x2

Equations

• ⋯ = ⋯

def Quotient.hrecOn₂ {α : 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₂ → HEq (f a₁ b₁) (f a₂ b₂)) : φ qa qb

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

Equations

• qa.hrecOn₂ qb f c = Quot.hrecOn₂ qa qb f ⋯ ⋯

def Quotient.map {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} (f : α → β) (h : ((fun (x1 x2 : α) => x1 ≈ x2) ⇒ fun (x1 x2 : β) => x1 ≈ x2) 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

• Quotient.map f h = Quot.map f h

@[simp]

theorem Quotient.map_mk {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} (f : α → β) (h : ((fun (x1 x2 : α) => x1 ≈ x2) ⇒ fun (x1 x2 : β) => x1 ≈ x2) f f) (x : α) : Quotient.map f h ⟦x⟧ = ⟦f x⟧

def Quotient.map₂ {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} {γ : Sort u_4} {sc : Setoid γ} (f : α → β → γ) (h : ((fun (x1 x2 : α) => x1 ≈ x2) ⇒ (fun (x1 x2 : β) => x1 ≈ x2) ⇒ fun (x1 x2 : γ) => x1 ≈ x2) 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

• Quotient.map₂ f h = Quotient.lift₂ (fun (x : α) (y : β) => ⟦f x y⟧) ⋯

@[simp]

theorem Quotient.map₂_mk {α : Sort u_1} {β : Sort u_2} {sa : Setoid α} {sb : Setoid β} {γ : Sort u_4} {sc : Setoid γ} (f : α → β → γ) (h : ((fun (x1 x2 : α) => x1 ≈ x2) ⇒ (fun (x1 x2 : β) => x1 ≈ x2) ⇒ fun (x1 x2 : γ) => x1 ≈ x2) f f) (x : α) (y : β) : Quotient.map₂ f h ⟦x⟧ ⟦y⟧ = ⟦f x y⟧

instance Quotient.lift.decidablePred {α : Sort u_1} {sa : Setoid α} (f : α → Prop) (h : ∀ (a b : α), a ≈ b → f a = f b) [DecidablePred f] : DecidablePred (Quotient.lift f h)

Equations

• Quotient.lift.decidablePred f h = Quot.lift.decidablePred HasEquiv.Equiv f h

instance Quotient.lift₂.decidablePred {α : 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 : α) → DecidablePred (f a)] (q₁ : Quotient sa) : DecidablePred (Quotient.lift₂ f h q₁)

Note that this provides DecidableRel (Quotient.lift₂ f h) when α = β.

Equations

• Quotient.lift₂.decidablePred f h q₁ q₂ = Quotient.recOnSubsingleton₂ q₁ q₂ hf

instance Quotient.instDecidableLiftOnOfDecidablePred_mathlib {α : Sort u_1} {sa : Setoid α} (q : Quotient sa) (f : α → Prop) (h : ∀ (a b : α), a ≈ b → f a = f b) [DecidablePred f] : Decidable (q.liftOn f h)

Equations

• q.instDecidableLiftOnOfDecidablePred_mathlib f h = Quotient.lift.decidablePred f h q

instance Quotient.instDecidableLiftOn₂OfDecidablePred_mathlib {α : 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 : α) → DecidablePred (f a)] : Decidable (q₁.liftOn₂ q₂ f h)

Equations

• q₁.instDecidableLiftOn₂OfDecidablePred_mathlib q₂ f h = Quotient.lift₂.decidablePred f h q₁ q₂

theorem Quot.eq {α : Type u_3} {r : α → α → Prop} {x : α} {y : α} : Quot.mk r x = Quot.mk r y ↔ Relation.EqvGen r x y

@[simp]

theorem Quotient.eq {α : Sort u_1} {r : Setoid α} {x : α} {y : α} : ⟦x⟧ = ⟦y⟧ ↔ r x y

theorem Quotient.eq_iff_equiv {α : Sort u_1} {r : Setoid α} {x : α} {y : α} : ⟦x⟧ = ⟦y⟧ ↔ x ≈ y

theorem Quotient.forall {α : Sort u_3} {s : Setoid α} {p : Quotient s → Prop} : (∀ (a : Quotient s), p a) ↔ ∀ (a : α), p ⟦a⟧

theorem Quotient.exists {α : Sort u_3} {s : Setoid α} {p : Quotient s → Prop} : (∃ (a : Quotient s), p a) ↔ ∃ (a : α), p ⟦a⟧

@[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

@[simp]

theorem Quotient.lift_comp_mk {α : Sort u_1} {β : Sort u_2} : ∀ {x : Setoid α} (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b), Quotient.lift f h ∘ Quotient.mk x = f

@[simp]

theorem Quotient.lift₂_mk {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} : ∀ {x : Setoid α} {x_1 : 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

theorem Quotient.liftOn_mk {α : Sort u_1} {β : Sort u_2} {s : Setoid α} (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b) (x : α) : ⟦x⟧.liftOn f h = f x

@[simp]

theorem Quotient.liftOn₂_mk {α : Sort u_3} {β : Sort u_4} : ∀ {x : Setoid α} (f : α → α → β) (h : ∀ (a₁ a₂ b₁ b₂ : α), a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) (x_1 y : α), ⟦x_1⟧.liftOn₂ ⟦y⟧ f h = f x_1 y

theorem surjective_quot_mk {α : Sort u_1} (r : α → α → Prop) : Function.Surjective (Quot.mk r)

Quot.mk r is a surjective function.

theorem surjective_quotient_mk {α : Sort u_3} (s : Setoid α) : Function.Surjective (Quotient.mk s)

Quotient.mk is a surjective function.

theorem surjective_quotient_mk' (α : Sort u_3) [s : Setoid α] : Function.Surjective Quotient.mk'

Quotient.mk' is a surjective function.

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

• q.out = Classical.choose ⋯

unsafe 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

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

• Quotient.out = Quot.out

@[simp]

theorem Quotient.out_eq {α : Sort u_1} {s : Setoid α} (q : Quotient s) : ⟦q.out⟧ = q

theorem Quotient.mk_out {α : Sort u_1} {s : Setoid α} (a : α) : s ⟦a⟧.out a

theorem Quotient.mk_eq_iff_out {α : Sort u_1} {s : Setoid α} {x : α} {y : Quotient s} : ⟦x⟧ = y ↔ x ≈ y.out

theorem Quotient.eq_mk_iff_out {α : Sort u_1} {s : Setoid α} {x : Quotient s} {y : α} : x = ⟦y⟧ ↔ x.out ≈ y

@[simp]

theorem Quotient.out_equiv_out {α : Sort u_1} {s : Setoid α} {x : Quotient s} {y : Quotient s} : x.out ≈ y.out ↔ x = y

theorem Quotient.out_injective {α : Sort u_1} {s : Setoid α} : Function.Injective Quotient.out

@[simp]

theorem Quotient.out_inj {α : Sort u_1} {s : Setoid α} {x : Quotient s} {y : Quotient s} : x.out = y.out ↔ x = y

instance piSetoid {ι : Sort u_3} {α : ι → Sort u_4} [(i : ι) → Setoid (α i)] : Setoid ((i : ι) → α i)

Equations

• piSetoid = { r := fun (a b : (i : ι) → α i) => ∀ (i : ι), a i ≈ b i, iseqv := ⋯ }

noncomputable def Quotient.choice {ι : Type u_3} {α : ι → Type u_4} {S : (i : ι) → Setoid (α i)} (f : (i : ι) → Quotient (S i)) : Quotient inferInstance

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

• Quotient.choice f = ⟦fun (i : ι) => (f i).out⟧

@[simp]

theorem Quotient.choice_eq {ι : Type u_3} {α : ι → Type u_4} {S : (i : ι) → Setoid (α i)} (f : (i : ι) → α i) : (Quotient.choice fun (i : ι) => ⟦f i⟧) = ⟦f⟧

theorem Quotient.induction_on_pi {ι : Type u_3} {α : ι → Sort u_4} {s : (i : ι) → Setoid (α i)} {p : ((i : ι) → Quotient (s i)) → Prop} (f : (i : ι) → Quotient (s i)) (h : ∀ (a : (i : ι) → α i), p fun (i : ι) => ⟦a i⟧) : p f

theorem nonempty_quotient_iff {α : Sort u_1} (s : Setoid α) : Nonempty (Quotient s) ↔ Nonempty α

Truncation

theorem true_equivalence {α : Sort u_1} : Equivalence fun (x x : α) => True

def trueSetoid {α : Sort u_1} : Setoid α

Always-true relation as a Setoid.

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

Equations

• trueSetoid = { r := fun (x x : α) => True, iseqv := ⋯ }

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

• Trunc α = Quotient trueSetoid

def Trunc.mk {α : Sort u_1} (a : α) : Trunc α

Constructor for Trunc α

Equations

• Trunc.mk a = Quot.mk (⇑trueSetoid) a

instance Trunc.instInhabited {α : Sort u_1} [Inhabited α] : Inhabited (Trunc α)

Equations

• Trunc.instInhabited = { default := Trunc.mk default }

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

• Trunc.lift f c = Quot.lift f ⋯

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

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

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

Lift a constant function on q : Trunc α.

Equations

• q.liftOn f c = Trunc.lift f c q

theorem Trunc.induction_on {α : Sort u_1} {β : Trunc α → Prop} (q : Trunc α) (h : ∀ (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 β) (h : ∀ (a : α) (b : β), C (Trunc.mk a) (Trunc.mk b)) : C q₁ q₂

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

instance Trunc.instSubsingletonTrunc {α : Sort u_1} : Subsingleton (Trunc α)

Equations

• ⋯ = ⋯

def Trunc.bind {α : Sort u_1} {β : Sort u_2} (q : Trunc α) (f : α → Trunc β) : Trunc β

The bind operator for the Trunc monad.

Equations

• q.bind f = q.liftOn f ⋯

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

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

Equations

• Trunc.map f q = q.bind (Trunc.mk ∘ f)

instance Trunc.instMonad : Monad Trunc

Equations

• Trunc.instMonad = Monad.mk

instance Trunc.instLawfulMonad : LawfulMonad Trunc

Equations

• Trunc.instLawfulMonad = ⋯

def Trunc.rec {α : Sort u_1} {C : Trunc α → Sort u_3} (f : (a : α) → C (Trunc.mk a)) (h : ∀ (a b : α), ⋯ ▸ f a = f b) (q : Trunc α) : C q

Recursion/induction principle for Trunc.

Equations

• Trunc.rec f h q = Quot.rec f ⋯ q

def Trunc.recOn {α : Sort u_1} {C : Trunc α → Sort u_3} (q : Trunc α) (f : (a : α) → C (Trunc.mk a)) (h : ∀ (a b : α), ⋯ ▸ f a = f b) : C q

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

Equations

• q.recOn f h = Trunc.rec f h q

def Trunc.recOnSubsingleton {α : 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.recOn assuming the codomain is a Subsingleton.

Equations

• q.recOnSubsingleton f = Trunc.rec f ⋯ q

noncomputable def Trunc.out {α : Sort u_1} : Trunc α → α

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

Equations

• Trunc.out = Quot.out

@[simp]

theorem Trunc.out_eq {α : Sort u_1} (q : Trunc α) : Trunc.mk q.out = q

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.

@[reducible, inline]

abbrev 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

• Quotient.mk'' a = ⟦a⟧

theorem Quotient.surjective_Quotient_mk'' {α : Sort u_1} {s₁ : Setoid α} : Function.Surjective Quotient.mk''

Quotient.mk'' is a surjective function.

def Quotient.liftOn' {α : Sort u_1} {φ : Sort u_4} {s₁ : Setoid α} (q : Quotient s₁) (f : α → φ) (h : ∀ (a b : α), s₁ a b → f a = f b) : φ

A version of Quotient.liftOn taking {s : Setoid α} as an implicit argument instead of an instance argument.

Equations

• q.liftOn' f h = q.liftOn f h

@[simp]

theorem Quotient.liftOn'_mk'' {α : Sort u_1} {φ : Sort u_4} {s₁ : Setoid α} (f : α → φ) (h : ∀ (a b : α), s₁ a b → f a = f b) (x : α) : (Quotient.mk'' x).liftOn' f h = f x

@[simp]

theorem Quotient.surjective_liftOn' {α : Sort u_1} {φ : Sort u_4} {s₁ : Setoid α} {f : α → φ} (h : ∀ (a b : α), s₁ a b → f a = f b) : (Function.Surjective fun (x : Quotient s₁) => x.liftOn' f h) ↔ Function.Surjective f

def Quotient.liftOn₂' {α : 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₂ : β), s₁ a₁ b₁ → s₂ a₂ b₂ → f a₁ a₂ = f b₁ b₂) : γ

A version of Quotient.liftOn₂ taking {s₁ : Setoid α} {s₂ : Setoid β} as implicit arguments instead of instance arguments.

Equations

• q₁.liftOn₂' q₂ f h = q₁.liftOn₂ q₂ f h

@[simp]

theorem Quotient.liftOn₂'_mk'' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : Setoid α} {s₂ : Setoid β} (f : α → β → γ) (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), s₁ a₁ b₁ → s₂ a₂ b₂ → f a₁ a₂ = f b₁ b₂) (a : α) (b : β) : (Quotient.mk'' a).liftOn₂' (Quotient.mk'' b) f h = f a b

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.inductionOn' {α : Sort u_1} {s₁ : Setoid α} {p : Quotient s₁ → Prop} (q : Quotient s₁) (h : ∀ (a : α), p (Quotient.mk'' a)) : p q

A version of Quotient.inductionOn taking {s : Setoid α} as an implicit argument instead of an instance argument.

theorem Quotient.inductionOn₂' {α : 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.inductionOn₂ taking {s₁ : Setoid α} {s₂ : Setoid β} as implicit arguments instead of instance arguments.

theorem Quotient.inductionOn₃' {α : 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.inductionOn₃ taking {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid γ} as implicit arguments instead of instance arguments.

def Quotient.recOnSubsingleton' {α : Sort u_1} {s₁ : Setoid α} {φ : Quotient s₁ → Sort u_5} [∀ (a : α), Subsingleton (φ ⟦a⟧)] (q : Quotient s₁) (f : (a : α) → φ (Quotient.mk'' a)) : φ q

A version of Quotient.recOnSubsingleton taking {s₁ : Setoid α} as an implicit argument instead of an instance argument.

Equations

• q.recOnSubsingleton' f = Quotient.recOnSubsingleton q f

def Quotient.recOnSubsingleton₂' {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} {φ : Quotient s₁ → Quotient s₂ → Sort u_5} [∀ (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.recOnSubsingleton₂ taking {s₁ : Setoid α} {s₂ : Setoid α} as implicit arguments instead of instance arguments.

Equations

• q₁.recOnSubsingleton₂' q₂ f = Quotient.recOnSubsingleton₂ q₁ q₂ f

def Quotient.hrecOn' {α : Sort u_1} {s₁ : Setoid α} {φ : Quotient s₁ → Sort u_5} (qa : Quotient s₁) (f : (a : α) → φ (Quotient.mk'' a)) (c : ∀ (a₁ a₂ : α), a₁ ≈ a₂ → HEq (f a₁) (f a₂)) : φ qa

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

Equations

• qa.hrecOn' f c = Quot.hrecOn qa f c

@[simp]

theorem Quotient.hrecOn'_mk'' {α : Sort u_1} {s₁ : Setoid α} {φ : Quotient s₁ → Sort u_5} (f : (a : α) → φ (Quotient.mk'' a)) (c : ∀ (a₁ a₂ : α), a₁ ≈ a₂ → HEq (f a₁) (f a₂)) (x : α) : (Quotient.mk'' x).hrecOn' f c = f x

def Quotient.hrecOn₂' {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} {φ : Quotient s₁ → Quotient s₂ → Sort u_5} (qa : Quotient s₁) (qb : Quotient s₂) (f : (a : α) → (b : β) → φ (Quotient.mk'' a) (Quotient.mk'' b)) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → HEq (f a₁ b₁) (f a₂ b₂)) : φ qa qb

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

Equations

• qa.hrecOn₂' qb f c = qa.hrecOn₂ qb f c

@[simp]

theorem Quotient.hrecOn₂'_mk'' {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} {φ : Quotient s₁ → Quotient s₂ → Sort u_5} (f : (a : α) → (b : β) → φ (Quotient.mk'' a) (Quotient.mk'' b)) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → HEq (f a₁ b₁) (f a₂ b₂)) (x : α) (qb : Quotient s₂) : (Quotient.mk'' x).hrecOn₂' qb f c = qb.hrecOn' (f x) ⋯

def Quotient.map' {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} (f : α → β) (h : (⇑s₁ ⇒ ⇑s₂) 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

• Quotient.map' f h = Quot.map f h

@[simp]

theorem Quotient.map'_mk'' {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} (f : α → β) (h : (⇑s₁ ⇒ ⇑s₂) f f) (x : α) : Quotient.map' f h (Quotient.mk'' x) = Quotient.mk'' (f x)

def Quotient.map₂' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid γ} (f : α → β → γ) (h : (⇑s₁ ⇒ ⇑s₂ ⇒ ⇑s₃) f f) : Quotient s₁ → Quotient s₂ → Quotient s₃

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

Equations

• Quotient.map₂' f h = Quotient.map₂ f h

@[simp]

theorem Quotient.map₂'_mk'' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid γ} (f : α → β → γ) (h : (⇑s₁ ⇒ ⇑s₂ ⇒ ⇑s₃) f f) (x : α) : Quotient.map₂' f h (Quotient.mk'' x) = Quotient.map' (f x) ⋯

theorem Quotient.exact' {α : Sort u_1} {s₁ : Setoid α} {a : α} {b : α} : Quotient.mk'' a = Quotient.mk'' b → s₁ a b

theorem Quotient.sound' {α : Sort u_1} {s₁ : Setoid α} {a : α} {b : α} : s₁ a b → Quotient.mk'' a = Quotient.mk'' b

@[simp]

theorem Quotient.eq' {α : Sort u_1} {s₁ : Setoid α} {a : α} {b : α} : Quotient.mk' a = Quotient.mk' b ↔ s₁ a b

theorem Quotient.eq'' {α : Sort u_1} {s₁ : Setoid α} {a : α} {b : α} : Quotient.mk'' a = Quotient.mk'' b ↔ s₁ a b

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

• a.out' = a.out

@[simp]

theorem Quotient.out_eq' {α : Sort u_1} {s₁ : Setoid α} (q : Quotient s₁) : Quotient.mk'' q.out' = q

theorem Quotient.mk_out' {α : Sort u_1} {s₁ : Setoid α} (a : α) : s₁ (Quotient.mk'' a).out' a

theorem Quotient.mk''_eq_mk {α : Sort u_1} {s : Setoid α} : Quotient.mk'' = Quotient.mk s

@[simp]

theorem Quotient.liftOn'_mk {α : Sort u_1} {β : Sort u_2} {s : Setoid α} (x : α) (f : α → β) (h : ∀ (a b : α), s a b → f a = f b) : ⟦x⟧.liftOn' f h = f x

@[simp]

theorem Quotient.liftOn₂'_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s : Setoid α} {t : Setoid β} (f : α → β → γ) (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), s a₁ b₁ → t a₂ b₂ → f a₁ a₂ = f b₁ b₂) (a : α) (b : β) : ⟦a⟧.liftOn₂' ⟦b⟧ f h = f a b

theorem Quotient.map'_mk {α : Sort u_1} {β : Sort u_2} {s : Setoid α} {t : Setoid β} (f : α → β) (h : (⇑s ⇒ ⇑t) f f) (x : α) : Quotient.map' f h ⟦x⟧ = ⟦f x⟧

instance Quotient.instDecidableLiftOn'OfDecidablePred {α : Sort u_1} {s₁ : Setoid α} (q : Quotient s₁) (f : α → Prop) (h : ∀ (a b : α), s₁ a b → f a = f b) [DecidablePred f] : Decidable (q.liftOn' f h)

Equations

• q.instDecidableLiftOn'OfDecidablePred f h = Quotient.lift.decidablePred f h q

instance Quotient.instDecidableLiftOn₂'OfDecidablePred {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → Prop) (h : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), s₁ a₁ a₂ → s₂ b₁ b₂ → f a₁ b₁ = f a₂ b₂) [(a : α) → DecidablePred (f a)] : Decidable (q₁.liftOn₂' q₂ f h)

Equations

• q₁.instDecidableLiftOn₂'OfDecidablePred q₂ f h = Quotient.lift₂.decidablePred f h q₁ q₂

@[simp]

theorem Equivalence.quot_mk_eq_iff {α : Type u_3} {r : α → α → Prop} (h : Equivalence r) (x : α) (y : α) : Quot.mk r x = Quot.mk r y ↔ r x y