Quotient types

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

Tags

quotient

ink

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

ink

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

ink

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

Equations

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

ink

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

Equations

• @Quot.Subsingleton = @Quot.Subsingleton.proof_1

ink

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

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

ink

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→ Quot rb.

Equations

• Quot.map f h = Quot.lift (fun x => Quot.mk rb (f x)) (_ : ∀ (x y : α), ra x y → Quot.mk rb (f x) = Quot.mk rb (f y))

ink

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'→ Quot ra'.

Equations

• Quot.mapRight h = Quot.map id h

ink

def Quot.factor {α : Type u_1} (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) (_ : ∀ (x y : α), r x y → Quot.mk s x = Quot.mk s y)

ink

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

ink

theorem Quot.lift_mk {α : Sort u_2} {γ : Sort u_1} {r : α → α → Prop} (f : α → γ) (h : ∀ (a₁ a₂ : α), r a₁ a₂ → f a₁ = f a₂) (a : α) : Quot.lift f h (Quot.mk r a) = f a

ink

theorem Quot.liftOn_mk {α : Sort u_2} {γ : Sort u_1} {r : α → α → Prop} (a : α) (f : α → γ) (h : ∀ (a₁ a₂ : α), r a₁ a₂ → f a₁ = f a₂) : Quot.liftOn (Quot.mk r a) f h = f a

ink

@[simp]

theorem Quot.surjective_lift {α : Sort u_2} {γ : Sort u_1} {r : α → α → Prop} {f : α → γ} (h : ∀ (a₁ a₂ : α), r a₁ a₂ → f a₁ = f a₂) : Function.Surjective (Quot.lift f h) ↔ Function.Surjective f

ink

def Quot.lift₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {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

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

ink

@[simp]

theorem Quot.lift₂_mk {α : Sort u_2} {β : Sort u_3} {γ : Sort u_1} {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

ink

def Quot.liftOn₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {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

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

ink

@[simp]

theorem Quot.liftOn₂_mk {α : Sort u_2} {β : Sort u_3} {γ : Sort u_1} {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.liftOn₂ (Quot.mk r a) (Quot.mk s b) f hr hs = f a b

ink

def Quot.map₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {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

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

ink

@[simp]

theorem Quot.map₂_mk {α : Sort u_2} {β : Sort u_3} {γ : Sort u_1} {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)

ink

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

Equations

• Quot.recOnSubsingleton₂ q₁ q₂ f = Quot.recOnSubsingleton q₁ fun a => Quot.recOnSubsingleton q₂ fun b => f a b

ink

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₂

ink

theorem Quot.induction_on₃ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {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₃

ink

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

ink

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₂ = Quot.recOnSubsingleton₂ q₁ q₂ hf

ink

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

Equations

• Quot.instDecidableLiftOnProp r q f h = Quot.lift.decidablePred (fun a b => r a b) f h q

ink

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

Equations

• Quot.instDecidableLiftOn₂Prop r s q₁ q₂ f ha hb = Quot.lift₂.decidablePred (fun a₁ a₂ => r a₁ a₂) (fun b₁ b₂ => s b₁ b₂) f ha hb q₁ q₂

ink

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.

ink

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

Equations

• Quotient.instInhabitedQuotient s = { default := Quotient.mk s default }

ink

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

Equations

• @Quotient.instSubsingletonQuotient = @Quotient.instSubsingletonQuotient.proof_1

ink

instance Quotient.instIsEquivEquivInstHasEquiv {α : Type u_1} [inst : Setoid α] : IsEquiv α fun x x_1 => x ≈ x_1

Equations

• @Quotient.instIsEquivEquivInstHasEquiv = @Quotient.instIsEquivEquivInstHasEquiv.proof_1

ink

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 : β) → φ (Quotient.mk sa a) (Quotient.mk sb 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

• Quotient.hrecOn₂ qa qb f c = Quot.hrecOn₂ qa qb f (_ : ∀ {b : β} {a₁ a₂ : α}, Setoid.r a₁ a₂ → HEq (f a₁ b) (f a₂ b)) (_ : ∀ {a : α} {b₁ b₂ : β}, Setoid.r b₁ b₂ → HEq (f a b₁) (f a b₂))

ink

def Quotient.map {α : Sort u_1} {β : Sort u_2} [sa : Setoid α] [sb : Setoid β] (f : α → β) (h : ((fun x x_1 => x ≈ x_1) ⇒ fun x x_1 => x ≈ x_1) f f) : Quotient sa → Quotient sb

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

Equations

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

ink

@[simp]

theorem Quotient.map_mk {α : Sort u_1} {β : Sort u_2} [sa : Setoid α] [sb : Setoid β] (f : α → β) (h : ((fun x x_1 => x ≈ x_1) ⇒ fun x x_1 => x ≈ x_1) f f) (x : α) : Quotient.map f h (Quotient.mk sa x) = Quotient.mk sb (f x)

ink

def Quotient.map₂ {α : Sort u_1} {β : Sort u_2} [sa : Setoid α] [sb : Setoid β] {γ : Sort u_3} [sc : Setoid γ] (f : α → β → γ) (h : ((fun x x_1 => x ≈ x_1) ⇒ (fun x x_1 => x ≈ x_1) ⇒ fun x x_1 => x ≈ x_1) 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→ Quotient sb → Quotient sc→ Quotient sc. Useful to define binary operations on quotients.

Equations

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

ink

@[simp]

theorem Quotient.map₂_mk {α : Sort u_1} {β : Sort u_2} [sa : Setoid α] [sb : Setoid β] {γ : Sort u_3} [sc : Setoid γ] (f : α → β → γ) (h : ((fun x x_1 => x ≈ x_1) ⇒ (fun x x_1 => x ≈ x_1) ⇒ fun x x_1 => x ≈ x_1) f f) (x : α) (y : β) : Quotient.map₂ f h (Quotient.mk sa x) (Quotient.mk sb y) = Quotient.mk sc (f x y)

ink

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

Equations

• Quotient.lift.decidablePred f h = Quot.lift.decidablePred (fun a b => a ≈ b) f h

ink

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

ink

@[simp]

theorem Quotient.eq {α : Sort u_1} [r : Setoid α] {x : α} {y : α} : Quotient.mk r x = Quotient.mk r y ↔ x ≈ y

ink

theorem forall_quotient_iff {α : Type u_1} [r : Setoid α] {p : Quotient r → Prop} : ((a : Quotient r) → p a) ↔ (a : α) → p (Quotient.mk r a)

ink

@[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 (Quotient.mk s x) = f x

ink

@[simp]

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

ink

@[simp]

theorem Quotient.lift₂_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [inst : Setoid α] [inst : Setoid β] (f : α → β → γ) (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) (a : α) (b : β) : Quotient.lift₂ f h (Quotient.mk inst a) (Quotient.mk inst b) = f a b

ink

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

ink

@[simp]

theorem Quotient.liftOn₂_mk {α : Sort u_1} {β : Sort u_2} [inst : Setoid α] (f : α → α → β) (h : ∀ (a₁ a₂ b₁ b₂ : α), a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) (x : α) (y : α) : Quotient.liftOn₂ (Quotient.mk inst x) (Quotient.mk inst y) f h = f x y

ink

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

Quot.mk r is a surjective function.

ink

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

Quotient.mk is a surjective function.

ink

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

• Quot.out q = Classical.choose (_ : ∃ a, Quot.mk r a = q)

ink

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.

Equations

• Quot.unquot = cast (_ : Quot r = α)

ink

@[simp]

theorem Quot.out_eq {α : Sort u_1} {r : α → α → Prop} (q : Quot r) : Quot.mk r (Quot.out q) = q

ink

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

ink

@[simp]

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

ink

theorem Quotient.mk_out {α : Sort u_1} [inst : Setoid α] (a : α) : Quotient.out (Quotient.mk inst a) ≈ a

ink

theorem Quotient.mk_eq_iff_out {α : Sort u_1} [s : Setoid α] {x : α} {y : Quotient s} : Quotient.mk s x = y ↔ x ≈ Quotient.out y

ink

theorem Quotient.eq_mk_iff_out {α : Sort u_1} [s : Setoid α] {x : Quotient s} {y : α} : x = Quotient.mk s y ↔ Quotient.out x ≈ y

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

instance piSetoid {ι : Sort u_1} {α : ι → Sort u_2} [inst : (i : ι) → Setoid (α i)] : Setoid ((i : ι) → α i)

Equations

• piSetoid = { r := fun a b => ∀ (i : ι), a i ≈ b i, iseqv := (_ : Equivalence fun a b => ∀ (i : ι), a i ≈ b i) }

ink

noncomputable def Quotient.choice {ι : Type u_1} {α : ι → Type u_2} [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 = Quotient.mk inferInstance fun i => Quotient.out (f i)

ink

@[simp]

theorem Quotient.choice_eq {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Setoid (α i)] (f : (i : ι) → α i) : (Quotient.choice fun i => Quotient.mk (inst i) (f i)) = Quotient.mk inferInstance f

ink

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 fun i => Quotient.mk (s i) (a i)) : p f

ink

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

Truncation

ink

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

ink

def trueSetoid {α : Sort u_1} : Setoid α

Always-true relation as a Setoid.

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

Equations

• trueSetoid = { r := fun x x => True, iseqv := (_ : Equivalence fun x x => True) }

ink

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

ink

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

Constructor for Trunc α

Equations

• Trunc.mk a = Quot.mk Setoid.r a

ink

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

Equations

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

ink

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 (_ : ∀ (a b : α), Setoid.r a b → f a = f b)

ink

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

ink

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

ink

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

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

ink

theorem Trunc.induction_on {α : Sort u_1} {β : Trunc α → Prop} (q : Trunc α) (h : (a : α) → β (Trunc.mk a)) : β q

ink

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

ink

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₂

ink

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

ink

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

Equations

• @Trunc.instSubsingletonTrunc = @Trunc.instSubsingletonTrunc.proof_1

ink

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

The bind operator for the Trunc monad.

Equations

• Trunc.bind q f = Trunc.liftOn q f (_ : ∀ (x x_1 : α), f x = f x_1)

ink

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

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

Equations

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

ink

instance Trunc.instMonadTrunc : Monad Trunc

Equations

• Trunc.instMonadTrunc = Monad.mk

ink

instance Trunc.instLawfulMonadTruncInstMonadTrunc : LawfulMonad Trunc

Equations

• Trunc.instLawfulMonadTruncInstMonadTrunc = Trunc.instLawfulMonadTruncInstMonadTrunc.proof_1

ink

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

Recursion/induction principle for Trunc.

Equations

• Trunc.rec f h q = Quot.rec f (_ : ∀ (a b : α), Setoid.r a b → (_ : Trunc.mk a = Trunc.mk b) ▸ f a = f b) q

ink

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

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

Equations

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

ink

def Trunc.recOnSubsingleton {α : Sort u_1} {C : Trunc α → Sort u_2} [inst : ∀ (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

• Trunc.recOnSubsingleton q f = Trunc.rec f (_ : ∀ (x b : α), (_ : Trunc.mk x = Trunc.mk b) ▸ f x = f b) q

ink

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

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

Equations

• Trunc.out = Quot.out

ink

@[simp]

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

ink

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.

ink

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

• Quotient.mk'' a = Quot.mk Setoid.r a

ink

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

Quotient.mk'' is a surjective function.

ink

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

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

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

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₂ : β), Setoid.r a₁ b₁ → Setoid.r 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

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

ink

@[simp]

theorem Quotient.liftOn₂'_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.liftOn₂' (Quotient.mk'' a) (Quotient.mk'' b) f h = f a b

ink

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.

ink

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.

ink

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.

ink

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.

ink

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.

ink

def Quotient.recOnSubsingleton' {α : Sort u_1} {s₁ : Setoid α} {φ : Quotient s₁ → Sort u_2} [inst : ∀ (a : α), Subsingleton (φ (Quotient.mk s₁ 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

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

ink

def Quotient.recOnSubsingleton₂' {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} {φ : Quotient s₁ → Quotient s₂ → Sort u_3} [inst : ∀ (a : α) (b : β), Subsingleton (φ (Quotient.mk s₁ a) (Quotient.mk s₂ 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

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

ink

def Quotient.hrecOn' {α : Sort u_1} {s₁ : Setoid α} {φ : Quotient s₁ → Sort u_2} (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

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

ink

@[simp]

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

ink

def Quotient.hrecOn₂' {α : 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₂ → 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

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

ink

@[simp]

theorem Quotient.hrecOn₂'_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₂ → HEq (f a₁ b₁) (f a₂ b₂)) (x : α) (qb : Quotient s₂) : Quotient.hrecOn₂' (Quotient.mk'' x) qb f c = Quotient.hrecOn' qb (f x) fun x x_1 => c x x x x_1 (_ : x ≈ x)

ink

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→ Quotient sb. Useful to define unary operations on quotients.

Equations

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

ink

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

ink

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

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

ink

@[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) (h x x (_ : x ≈ x))

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

• Quotient.out' a = Quotient.out a

ink

@[simp]

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

ink

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

ink

theorem Quotient.mk''_eq_mk {α : Sort u_1} [s : Setoid α] (x : α) : Quotient.mk'' x = Quotient.mk s x

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

theorem Quotient.map'_mk {α : Sort u_2} {β : Sort u_1} [s : Setoid α] [t : Setoid β] (f : α → β) (h : (Setoid.r ⇒ Setoid.r) f f) (x : α) : Quotient.map' f h (Quotient.mk s x) = Quotient.mk t (f x)

ink

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

Equations

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

ink

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

Equations

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