Mathlib.Logic.Equiv.Defs

Equiv structure

(α : Sort*) (β : Sort _)

Full source

/-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/
structure Equiv (α : Sort*) (β : Sort _) where
  protected toFun : α → β
  protected invFun : β → α
  protected left_inv : LeftInverse invFun toFun
  protected right_inv : RightInverse invFun toFun

Type Equivalence (Bijection with Inverse)

Informal description

The structure `Equiv α β`, also denoted as `α ≃ β`, represents a bijective map between types `α` and `β` bundled with its inverse map. It consists of a function `f : α → β` and its two-sided inverse `g : β → α`, such that `g ∘ f = id` and `f ∘ g = id`.

term_≃_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
infixl:25 " ≃ " => Equiv

Type equivalence notation

Informal description

The infix notation `≃` is defined as a shorthand for `Equiv`, representing type equivalences (bijective maps with their inverses).

EquivLike.toEquiv definition

{F} [EquivLike F α β] (f : F) : α ≃ β

Full source

/-- Turn an element of a type `F` satisfying `EquivLike F α β` into an actual
`Equiv`. This is declared as the default coercion from `F` to `α ≃ β`. -/
@[coe]
def EquivLike.toEquiv {F} [EquivLike F α β] (f : F) : α ≃ β where
  toFun := f
  invFun := EquivLike.inv f
  left_inv := EquivLike.left_inv f
  right_inv := EquivLike.right_inv f

Conversion from Equiv-like to explicit equivalence

Informal description

Given a type `F` that satisfies `EquivLike F α β` (i.e., elements of `F` can be coerced to bijections between types `α` and `β`), the function `EquivLike.toEquiv` converts an element `f : F` into an explicit equivalence `α ≃ β`. This equivalence consists of: - A forward map `f : α → β`, - An inverse map `EquivLike.inv f : β → α`, - Proof that the inverse is a left inverse: `EquivLike.left_inv f`, - Proof that the inverse is a right inverse: `EquivLike.right_inv f`. This is declared as the default coercion from `F` to `α ≃ β`.

instCoeTCEquivOfEquivLike instance

{F} [EquivLike F α β] : CoeTC F (α ≃ β)

Full source

/-- Any type satisfying `EquivLike` can be cast into `Equiv` via `EquivLike.toEquiv`. -/
instance {F} [EquivLike F α β] : CoeTC F (α ≃ β) :=
  ⟨EquivLike.toEquiv⟩

Canonical Interpretation of Equiv-like as Equivalence

Informal description

For any type `F` that satisfies `EquivLike F α β` (i.e., elements of `F` can be coerced to bijections between types `α` and `β`), there is a canonical way to interpret an element `f : F` as an explicit equivalence `α ≃ β`. This equivalence consists of a bijective map from `α` to `β` with its two-sided inverse.

Equiv.Perm abbrev

(α : Sort*)

Full source

/-- `Perm α` is the type of bijections from `α` to itself. -/
abbrev Equiv.Perm (α : Sort*) :=
  Equiv α α

Permutation Type of a Given Type

Informal description

The type `Perm α` represents the set of all bijective maps (permutations) from a type `α` to itself.

Equiv.instEquivLike instance

: EquivLike (α ≃ β) α β

Full source

instance : EquivLike (α ≃ β) α β where
  coe := Equiv.toFun
  inv := Equiv.invFun
  left_inv := Equiv.left_inv
  right_inv := Equiv.right_inv
  coe_injective' e₁ e₂ h₁ h₂ := by cases e₁; cases e₂; congr

Equivalence Types as EquivLike Structures

Informal description

For any types $\alpha$ and $\beta$, the type $\alpha \simeq \beta$ of equivalences (bijections with inverses) between $\alpha$ and $\beta$ satisfies the properties of an `EquivLike` structure, meaning it can be treated as a class of bijective coercions between $\alpha$ and $\beta$.

Equiv.instFunLike instance

: FunLike (α ≃ β) α β

Full source

/-- Helper instance when inference gets stuck on following the normal chain
`EquivLike → FunLike`.

TODO: this instance doesn't appear to be necessary: remove it (after benchmarking?)
-/
instance : FunLike (α ≃ β) α β where
  coe := Equiv.toFun
  coe_injective' := DFunLike.coe_injective

Equivalence as Function-Like Object

Informal description

For any types $\alpha$ and $\beta$, an equivalence $\alpha \simeq \beta$ can be treated as a function-like object from $\alpha$ to $\beta$.

EquivLike.coe_coe theorem

{F} [EquivLike F α β] (e : F) : ((e : α ≃ β) : α → β) = e

Full source

@[simp, norm_cast]
lemma _root_.EquivLike.coe_coe {F} [EquivLike F α β] (e : F) :
    ((e : α ≃ β) : α → β) = e := rfl

Coercion Consistency for Equivalence-like Types

Informal description

For any type `F` that satisfies `EquivLike F α β` (i.e., elements of `F` can be coerced to bijections between types `α` and `β`), and for any element `e : F`, the underlying function of the equivalence obtained by coercing `e` to `α ≃ β` is equal to `e` itself as a function from `α` to `β`.

Equiv.coe_fn_mk theorem

(f : α → β) (g l r) : (Equiv.mk f g l r : α → β) = f

Full source

@[simp] theorem coe_fn_mk (f : α → β) (g l r) : (Equiv.mk f g l r : α → β) = f :=
  rfl

Underlying Function of Constructed Equivalence

Informal description

For any functions $f : \alpha \to \beta$, $g : \beta \to \alpha$, and proofs $l$, $r$ that $g$ is a left and right inverse of $f$ respectively, the underlying function of the equivalence $\text{Equiv.mk}\ f\ g\ l\ r$ is equal to $f$.

Equiv.coe_fn_injective theorem

: @Function.Injective (α ≃ β) (α → β) (fun e => e)

Full source

/-- The map `(r ≃ s) → (r → s)` is injective. -/
theorem coe_fn_injective : @Function.Injective (α ≃ β) (α → β) (fun e => e) :=
  DFunLike.coe_injective'

Injectivity of the Underlying Function Map for Equivalences

Informal description

The function that maps an equivalence $e : \alpha \simeq \beta$ to its underlying function $e : \alpha \to \beta$ is injective. In other words, if two equivalences $e_1, e_2 : \alpha \simeq \beta$ have the same underlying function ($e_1 = e_2$ as functions), then $e_1 = e_2$ as equivalences.

Equiv.coe_inj theorem

{e₁ e₂ : α ≃ β} : (e₁ : α → β) = e₂ ↔ e₁ = e₂

Full source

protected theorem coe_inj {e₁ e₂ : α ≃ β} : (e₁ : α → β) = e₂ ↔ e₁ = e₂ :=
  @DFunLike.coe_fn_eq _ _ _ _ e₁ e₂

Equality of Equivalences via Underlying Functions

Informal description

For any two equivalences $e_1, e_2 : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the underlying functions $e_1$ and $e_2$ are equal if and only if $e_1 = e_2$ as equivalences.

Equiv.ext theorem

{f g : Equiv α β} (H : ∀ x, f x = g x) : f = g

Full source

@[ext] theorem ext {f g : Equiv α β} (H : ∀ x, f x = g x) : f = g := DFunLike.ext f g H

Extensionality of Equivalences: Pointwise Equality Implies Equality

Informal description

For any two equivalences (bijective maps with inverses) $f, g : \alpha \simeq \beta$, if $f(x) = g(x)$ for all $x \in \alpha$, then $f = g$ as equivalences.

Equiv.congr_arg theorem

{f : Equiv α β} {x x' : α} : x = x' → f x = f x'

Full source

protected theorem congr_arg {f : Equiv α β} {x x' : α} : x = x' → f x = f x' :=
  DFunLike.congr_arg f

Equivalence Preserves Equality: $x = x' \implies f(x) = f(x')$

Informal description

For any equivalence $f : \alpha \simeq \beta$ and elements $x, x' \in \alpha$, if $x = x'$, then $f(x) = f(x')$.

Equiv.congr_fun theorem

{f g : Equiv α β} (h : f = g) (x : α) : f x = g x

Full source

protected theorem congr_fun {f g : Equiv α β} (h : f = g) (x : α) : f x = g x :=
  DFunLike.congr_fun h x

Pointwise Equality of Equivalences

Informal description

For any two equivalences $f, g : \alpha \simeq \beta$, if $f = g$, then for all $x \in \alpha$, we have $f(x) = g(x)$.

Equiv.Perm.ext theorem

{σ τ : Equiv.Perm α} (H : ∀ x, σ x = τ x) : σ = τ

Full source

@[ext] theorem Perm.ext {σ τ : Equiv.Perm α} (H : ∀ x, σ x = τ x) : σ = τ := Equiv.ext H

Extensionality of Permutations: Pointwise Equality Implies Equality

Informal description

For any two permutations $\sigma, \tau : \alpha \simeq \alpha$, if $\sigma(x) = \tau(x)$ for all $x \in \alpha$, then $\sigma = \tau$.

Equiv.Perm.congr_arg theorem

{f : Equiv.Perm α} {x x' : α} : x = x' → f x = f x'

Full source

protected theorem Perm.congr_arg {f : Equiv.Perm α} {x x' : α} : x = x' → f x = f x' :=
  Equiv.congr_arg

Permutation Preserves Equality: $x = x' \implies f(x) = f(x')$

Informal description

For any permutation $f : \alpha \simeq \alpha$ and elements $x, x' \in \alpha$, if $x = x'$, then $f(x) = f(x')$.

Equiv.Perm.congr_fun theorem

{f g : Equiv.Perm α} (h : f = g) (x : α) : f x = g x

Full source

protected theorem Perm.congr_fun {f g : Equiv.Perm α} (h : f = g) (x : α) : f x = g x :=
  Equiv.congr_fun h x

Pointwise Equality of Permutations

Informal description

For any two permutations $f, g : \alpha \simeq \alpha$, if $f = g$, then for all $x \in \alpha$, we have $f(x) = g(x)$.

Equiv.refl definition

(α : Sort*) : α ≃ α

Full source

/-- Any type is equivalent to itself. -/
@[refl] protected def refl (α : Sort*) : α ≃ α := ⟨id, id, fun _ => rfl, fun _ => rfl⟩

Identity equivalence

Informal description

The identity equivalence on a type $\alpha$, which is the bijection from $\alpha$ to itself given by the identity function, with its inverse also being the identity function.

Equiv.inhabited' instance

: Inhabited (α ≃ α)

Full source

instance inhabited' : Inhabited (α ≃ α) := ⟨Equiv.refl α⟩

Inhabited Type of Self-Equivalences

Informal description

For any type $\alpha$, the type of self-equivalences $\alpha \simeq \alpha$ is inhabited (i.e., contains at least one element).

Equiv.symm definition

(e : α ≃ β) : β ≃ α

Full source

/-- Inverse of an equivalence `e : α ≃ β`. -/
@[symm]
protected def symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun, e.right_inv, e.left_inv⟩

Inverse of an equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$, the inverse equivalence $e^{-1} : \beta \simeq \alpha$ is defined by swapping the forward and inverse functions of $e$, ensuring that $e^{-1}$ is a bijection with $e$ as its inverse.

Equiv.Simps.symm_apply definition

(e : α ≃ β) : β → α

Full source

/-- See Note [custom simps projection] -/
def Simps.symm_apply (e : α ≃ β) : β → α := e.symm

Inverse function of an equivalence

Informal description

For an equivalence $e : \alpha \simeq \beta$, the function maps an element $y \in \beta$ to its preimage $x \in \alpha$ under the equivalence $e$, i.e., $x = e^{-1}(y)$ where $e^{-1}$ is the inverse function of $e$.

Equiv.left_inv' theorem

(e : α ≃ β) : Function.LeftInverse e.symm e

Full source

/-- Restatement of `Equiv.left_inv` in terms of `Function.LeftInverse`. -/
theorem left_inv' (e : α ≃ β) : Function.LeftInverse e.symm e := e.left_inv

Left Inverse Property of Equivalence Inverses

Informal description

For any equivalence $e : \alpha \simeq \beta$, the inverse equivalence $e^{-1} : \beta \simeq \alpha$ is a left inverse of $e$, meaning that for all $x \in \alpha$, we have $e^{-1}(e(x)) = x$.

Equiv.right_inv' theorem

(e : α ≃ β) : Function.RightInverse e.symm e

Full source

/-- Restatement of `Equiv.right_inv` in terms of `Function.RightInverse`. -/
theorem right_inv' (e : α ≃ β) : Function.RightInverse e.symm e := e.right_inv

Right Inverse Property of Equivalence Inverses

Informal description

For any equivalence $e : \alpha \simeq \beta$, the inverse equivalence $e^{-1} : \beta \simeq \alpha$ is a right inverse of $e$, meaning that for all $y \in \beta$, we have $e(e^{-1}(y)) = y$.

Equiv.trans definition

(e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ

Full source

/-- Composition of equivalences `e₁ : α ≃ β` and `e₂ : β ≃ γ`. -/
@[trans]
protected def trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
  ⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm, e₂.left_inv.comp e₁.left_inv, e₂.right_inv.comp e₁.right_inv⟩

Composition of equivalences

Informal description

Given two equivalences $e₁ : α ≃ β$ and $e₂ : β ≃ γ$, their composition $e₂ ∘ e₁$ forms an equivalence $α ≃ γ$, where the inverse is given by the composition of the inverses $e₁^{-1} ∘ e₂^{-1}$.

Equiv.instTrans instance

: Trans Equiv Equiv Equiv

Full source

@[simps]
instance : Trans Equiv Equiv Equiv where
  trans := Equiv.trans

Transitivity of Type Equivalences

Informal description

The composition of equivalences (bijections with inverses) between types is transitive. That is, given equivalences $e₁ : α ≃ β$ and $e₂ : β ≃ γ$, their composition $e₂ ∘ e₁$ forms an equivalence $α ≃ γ$.

Equiv.toFun_as_coe theorem

(e : α ≃ β) : e.toFun = e

Full source

@[simp, mfld_simps] theorem toFun_as_coe (e : α ≃ β) : e.toFun = e := rfl

Underlying Function of Equivalence is the Equivalence Itself

Informal description

For any equivalence $e : \alpha \simeq \beta$, the underlying function $e.\text{toFun}$ is equal to $e$ itself when viewed as a function.

Equiv.invFun_as_coe theorem

(e : α ≃ β) : e.invFun = e.symm

Full source

@[simp, mfld_simps] theorem invFun_as_coe (e : α ≃ β) : e.invFun = e.symm := rfl

Inverse Function of Equivalence Equals Symmetric Equivalence

Informal description

For any equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the inverse function $e^{-1}$ of $e$ is equal to the symmetric equivalence $e^{-1} : \beta \simeq \alpha$.

Equiv.injective theorem

(e : α ≃ β) : Injective e

Full source

protected theorem injective (e : α ≃ β) : Injective e := EquivLike.injective e

Injectivity of Equivalence Maps

Informal description

For any equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the function $e : \alpha \to \beta$ is injective.

Equiv.surjective theorem

(e : α ≃ β) : Surjective e

Full source

protected theorem surjective (e : α ≃ β) : Surjective e := EquivLike.surjective e

Surjectivity of Equivalence Maps

Informal description

For any equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the function $e : \alpha \to \beta$ is surjective.

Equiv.bijective theorem

(e : α ≃ β) : Bijective e

Full source

protected theorem bijective (e : α ≃ β) : Bijective e := EquivLike.bijective e

Bijectivity of Equivalence Maps

Informal description

For any equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the function $e : \alpha \to \beta$ is bijective.

Equiv.subsingleton theorem

(e : α ≃ β) [Subsingleton β] : Subsingleton α

Full source

protected theorem subsingleton (e : α ≃ β) [Subsingleton β] : Subsingleton α :=
  e.injective.subsingleton

Subsingleton Property Transfer via Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, if $\beta$ is a subsingleton (i.e., all elements of $\beta$ are equal), then $\alpha$ is also a subsingleton.

Equiv.subsingleton.symm theorem

(e : α ≃ β) [Subsingleton α] : Subsingleton β

Full source

protected theorem subsingleton.symm (e : α ≃ β) [Subsingleton α] : Subsingleton β :=
  e.symm.injective.subsingleton

Subsingleton Property Preserved by Equivalence Symmetry

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, if $\alpha$ is a subsingleton (i.e., has at most one element), then $\beta$ is also a subsingleton.

Equiv.subsingleton_congr theorem

(e : α ≃ β) : Subsingleton α ↔ Subsingleton β

Full source

theorem subsingleton_congr (e : α ≃ β) : SubsingletonSubsingleton α ↔ Subsingleton β :=
  ⟨fun _ => e.symm.subsingleton, fun _ => e.subsingleton⟩

Subsingleton Equivalence: $\text{Subsingleton}(\alpha) \leftrightarrow \text{Subsingleton}(\beta)$ via $e : \alpha \simeq \beta$

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the type $\alpha$ is a subsingleton (i.e., has at most one element) if and only if $\beta$ is a subsingleton.

Equiv.equiv_subsingleton_cod instance

[Subsingleton β] : Subsingleton (α ≃ β)

Full source

instance equiv_subsingleton_cod [Subsingleton β] : Subsingleton (α ≃ β) :=
  ⟨fun _ _ => Equiv.ext fun _ => Subsingleton.elim _ _⟩

Equivalences to a Subsingleton Form a Subsingleton

Informal description

For any type $\beta$ that is a subsingleton (i.e., has at most one element), the type of equivalences $\alpha \simeq \beta$ is also a subsingleton.

Equiv.equiv_subsingleton_dom instance

[Subsingleton α] : Subsingleton (α ≃ β)

Full source

instance equiv_subsingleton_dom [Subsingleton α] : Subsingleton (α ≃ β) :=
  ⟨fun f _ => Equiv.ext fun _ => @Subsingleton.elim _ (Equiv.subsingleton.symm f) _ _⟩

Equivalences from a Subsingleton Form a Subsingleton

Informal description

For any type $\alpha$ that is a subsingleton (i.e., has at most one element), the type of equivalences $\alpha \simeq \beta$ is also a subsingleton.

Equiv.permUnique instance

[Subsingleton α] : Unique (Perm α)

Full source

instance permUnique [Subsingleton α] : Unique (Perm α) :=
  uniqueOfSubsingleton (Equiv.refl α)

Unique Permutation Type for Subsingleton

Informal description

For any type $\alpha$ that is a subsingleton (i.e., has at most one element), the type of permutations $\text{Perm}(\alpha)$ is uniquely determined by the identity equivalence.

Equiv.Perm.subsingleton_eq_refl theorem

[Subsingleton α] (e : Perm α) : e = Equiv.refl α

Full source

theorem Perm.subsingleton_eq_refl [Subsingleton α] (e : Perm α) : e = Equiv.refl α :=
  Subsingleton.elim _ _

All Permutations of a Subsingleton are the Identity

Informal description

For any subsingleton type $\alpha$ (i.e., a type with at most one element), every permutation $e$ of $\alpha$ is equal to the identity equivalence $\text{refl}_\alpha$.

Equiv.nontrivial theorem

{α β} (e : α ≃ β) [Nontrivial β] : Nontrivial α

Full source

protected theorem nontrivial {α β} (e : α ≃ β) [Nontrivial β] : Nontrivial α :=
  e.surjective.nontrivial

Nontriviality Preservation under Type Equivalence

Informal description

Given types $\alpha$ and $\beta$ and an equivalence $e : \alpha \simeq \beta$, if $\beta$ is nontrivial (i.e., contains at least two distinct elements), then $\alpha$ is also nontrivial.

Equiv.nontrivial_congr theorem

{α β} (e : α ≃ β) : Nontrivial α ↔ Nontrivial β

Full source

theorem nontrivial_congr {α β} (e : α ≃ β) : NontrivialNontrivial α ↔ Nontrivial β :=
  ⟨fun _ ↦ e.symm.nontrivial, fun _ ↦ e.nontrivial⟩

Nontriviality Equivalence under Bijection: $\text{Nontrivial}(\alpha) \leftrightarrow \text{Nontrivial}(\beta)$

Informal description

For any types $\alpha$ and $\beta$ and a bijection $e : \alpha \simeq \beta$, the type $\alpha$ is nontrivial (contains at least two distinct elements) if and only if $\beta$ is nontrivial.

Equiv.decidableEq definition

(e : α ≃ β) [DecidableEq β] : DecidableEq α

Full source

/-- Transfer `DecidableEq` across an equivalence. -/
protected def decidableEq (e : α ≃ β) [DecidableEq β] : DecidableEq α :=
  e.injective.decidableEq

Decidable equality transfer via equivalence

Informal description

Given an equivalence $e \colon \alpha \simeq \beta$ between types $\alpha$ and $\beta$, if $\beta$ has decidable equality, then $\alpha$ also has decidable equality. Specifically, for any $x, y \in \alpha$, the equality $x = y$ is decided by checking $e(x) = e(y)$.

Equiv.nonempty_congr theorem

(e : α ≃ β) : Nonempty α ↔ Nonempty β

Full source

theorem nonempty_congr (e : α ≃ β) : NonemptyNonempty α ↔ Nonempty β := Nonempty.congr e e.symm

Nonempty Types are Equivalent under Equivalence

Informal description

For any types $\alpha$ and $\beta$ and an equivalence $e : \alpha \simeq \beta$, the type $\alpha$ is nonempty if and only if $\beta$ is nonempty.

Equiv.nonempty theorem

(e : α ≃ β) [Nonempty β] : Nonempty α

Full source

protected theorem nonempty (e : α ≃ β) [Nonempty β] : Nonempty α := e.nonempty_congr.mpr ‹_›

Nonempty Transfer Along Equivalence

Informal description

Given an equivalence $e \colon \alpha \simeq \beta$ between types $\alpha$ and $\beta$, if $\beta$ is nonempty (i.e., there exists an element of type $\beta$), then $\alpha$ is also nonempty.

Equiv.inhabited definition

[Inhabited β] (e : α ≃ β) : Inhabited α

Full source

/-- If `α ≃ β` and `β` is inhabited, then so is `α`. -/
protected def inhabited [Inhabited β] (e : α ≃ β) : Inhabited α := ⟨e.symm default⟩

Transfer of inhabitedness along an equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ and an inhabited type $\beta$ (i.e., $\beta$ has a default element), the type $\alpha$ is also inhabited, with the default element obtained by applying the inverse equivalence $e^{-1}$ to the default element of $\beta$.

Equiv.unique definition

[Unique β] (e : α ≃ β) : Unique α

Full source

/-- If `α ≃ β` and `β` is a singleton type, then so is `α`. -/
protected def unique [Unique β] (e : α ≃ β) : Unique α := e.symm.surjective.unique

Transfer of uniqueness along an equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ and a unique element in $\beta$, the type $\alpha$ also has a unique element. Specifically, if $\beta$ has exactly one element (i.e., is a singleton type), then $\alpha$ is also a singleton type via the inverse equivalence $e^{-1} : \beta \simeq \alpha$.

Equiv.cast definition

{α β : Sort _} (h : α = β) : α ≃ β

Full source

/-- Equivalence between equal types. -/
protected def cast {α β : Sort _} (h : α = β) : α ≃ β :=
  ⟨cast h, cast h.symm, fun _ => by cases h; rfl, fun _ => by cases h; rfl⟩

Equivalence by Type Casting

Informal description

Given two types $\alpha$ and $\beta$ and a proof $h$ that $\alpha = \beta$, the function `Equiv.cast` constructs an equivalence $\alpha \simeq \beta$ where the forward and backward maps are both given by casting along $h$ and its symmetry. Specifically, it consists of: - A function $\alpha \to \beta$ defined by casting along $h$ - An inverse function $\beta \to \alpha$ defined by casting along $h^{-1}$ - Proofs that these functions are mutual inverses (omitted in informal statement)

Equiv.coe_fn_symm_mk theorem

(f : α → β) (g l r) : ((Equiv.mk f g l r).symm : β → α) = g

Full source

@[simp] theorem coe_fn_symm_mk (f : α → β) (g l r) : ((Equiv.mk f g l r).symm : β → α) = g := rfl

Inverse of Constructed Equivalence Acts as Given Right Inverse

Informal description

For any functions $f : \alpha \to \beta$ and $g : \beta \to \alpha$ with proofs $l$ that $g$ is a left inverse of $f$ and $r$ that $g$ is a right inverse of $f$, the underlying function of the inverse equivalence $\text{Equiv.mk}\ f\ g\ l\ r$.symm is equal to $g$. In other words, the inverse of the constructed equivalence $(f, g, l, r)$ acts as $g$ when viewed as a function.

Equiv.coe_refl theorem

: (Equiv.refl α : α → α) = id

Full source

@[simp] theorem coe_refl : (Equiv.refl α : α → α) = id := rfl

Identity Equivalence as Identity Function

Informal description

The underlying function of the identity equivalence $\text{refl}_\alpha$ on a type $\alpha$ is equal to the identity function $\text{id} : \alpha \to \alpha$.

Equiv.Perm.coe_subsingleton theorem

{α : Type*} [Subsingleton α] (e : Perm α) : (e : α → α) = id

Full source

/-- This cannot be a `simp` lemmas as it incorrectly matches against `e : α ≃ synonym α`, when
`synonym α` is semireducible. This makes a mess of `Multiplicative.ofAdd` etc. -/
theorem Perm.coe_subsingleton {α : Type*} [Subsingleton α] (e : Perm α) : (e : α → α) = id := by
  rw [Perm.subsingleton_eq_refl e, coe_refl]

Permutation on Subsingleton is Identity Function

Informal description

For any subsingleton type $\alpha$ (i.e., a type with at most one element) and any permutation $e$ of $\alpha$, the underlying function of $e$ is equal to the identity function $\text{id} : \alpha \to \alpha$.

Equiv.refl_apply theorem

(x : α) : Equiv.refl α x = x

Full source

@[simp] theorem refl_apply (x : α) : Equiv.refl α x = x := rfl

Identity Equivalence Acts as Identity Function

Informal description

For any element $x$ of type $\alpha$, the identity equivalence $\text{refl}_\alpha$ applied to $x$ returns $x$ itself, i.e., $\text{refl}_\alpha(x) = x$.

Equiv.coe_trans theorem

(f : α ≃ β) (g : β ≃ γ) : (f.trans g : α → γ) = g ∘ f

Full source

@[simp] theorem coe_trans (f : α ≃ β) (g : β ≃ γ) : (f.trans g : α → γ) = g ∘ f := rfl

Composition of Equivalences as Function Composition

Informal description

For any equivalences $f : \alpha \simeq \beta$ and $g : \beta \simeq \gamma$, the underlying function of the composed equivalence $f \circ g : \alpha \simeq \gamma$ is equal to the composition $g \circ f$ as functions from $\alpha$ to $\gamma$.

Equiv.trans_apply theorem

(f : α ≃ β) (g : β ≃ γ) (a : α) : (f.trans g) a = g (f a)

Full source

@[simp] theorem trans_apply (f : α ≃ β) (g : β ≃ γ) (a : α) : (f.trans g) a = g (f a) := rfl

Composition of Equivalences Acts as Function Composition

Informal description

For any equivalences $f \colon \alpha \simeq \beta$ and $g \colon \beta \simeq \gamma$, and any element $a \in \alpha$, the composition $f \circ g$ evaluated at $a$ equals $g(f(a))$.

Equiv.apply_symm_apply theorem

(e : α ≃ β) (x : β) : e (e.symm x) = x

Full source

@[simp] theorem apply_symm_apply (e : α ≃ β) (x : β) : e (e.symm x) = x := e.right_inv x

Equivalence Recovery: $e(e^{-1}(x)) = x$

Informal description

For any equivalence $e : \alpha \simeq \beta$ and any element $x \in \beta$, applying $e$ to the inverse image $e^{-1}(x)$ recovers the original element $x$, i.e., $e(e^{-1}(x)) = x$.

Equiv.symm_apply_apply theorem

(e : α ≃ β) (x : α) : e.symm (e x) = x

Full source

@[simp] theorem symm_apply_apply (e : α ≃ β) (x : α) : e.symm (e x) = x := e.left_inv x

Inverse Equivalence Recovers Original Element

Informal description

For any equivalence $e : \alpha \simeq \beta$ and any element $x \in \alpha$, applying the inverse equivalence $e^{-1}$ to the image $e(x)$ recovers the original element $x$, i.e., $e^{-1}(e(x)) = x$.

Equiv.symm_comp_self theorem

(e : α ≃ β) : e.symm ∘ e = id

Full source

@[simp] theorem symm_comp_self (e : α ≃ β) : e.symm ∘ e = id := funext e.symm_apply_apply

Inverse Composition with Equivalence Yields Identity

Informal description

For any equivalence $e : \alpha \simeq \beta$, the composition of the inverse equivalence $e^{-1}$ with $e$ is equal to the identity function on $\alpha$, i.e., $e^{-1} \circ e = \text{id}_\alpha$.

Equiv.self_comp_symm theorem

(e : α ≃ β) : e ∘ e.symm = id

Full source

@[simp] theorem self_comp_symm (e : α ≃ β) : e ∘ e.symm = id := funext e.apply_symm_apply

Composition of Equivalence with its Inverse Yields Identity: $e \circ e^{-1} = \text{id}_\beta$

Informal description

For any equivalence $e : \alpha \simeq \beta$, the composition of $e$ with its inverse $e^{-1}$ is equal to the identity function on $\beta$, i.e., $e \circ e^{-1} = \text{id}_\beta$.

EquivLike.apply_coe_symm_apply theorem

{F} [EquivLike F α β] (e : F) (x : β) : e ((e : α ≃ β).symm x) = x

Full source

@[simp] lemma _root_.EquivLike.apply_coe_symm_apply {F} [EquivLike F α β] (e : F) (x : β) :
    e ((e : α ≃ β).symm x) = x :=
  (e : α ≃ β).apply_symm_apply x

Recovery of Element via Equivalence-like Coercion: $e(e^{-1}(x)) = x$

Informal description

For any type `F` that can be coerced to a bijection between types `α` and `β` (i.e., `[EquivLike F α β]`), and for any element `e : F` and `x : β`, applying `e` to the inverse image of `x` under the equivalence `(e : α ≃ β).symm` recovers `x`, i.e., $e(e^{-1}(x)) = x$.

EquivLike.coe_symm_apply_apply theorem

{F} [EquivLike F α β] (e : F) (x : α) : (e : α ≃ β).symm (e x) = x

Full source

@[simp] lemma _root_.EquivLike.coe_symm_apply_apply {F} [EquivLike F α β] (e : F) (x : α) :
    (e : α ≃ β).symm (e x) = x :=
  (e : α ≃ β).symm_apply_apply x

Inverse Equivalence Recovers Original Element via Coercion

Informal description

For any type `F` that satisfies `EquivLike F α β` (i.e., elements of `F` can be coerced to bijections between types `α` and `β`), and for any element `e : F` and any `x : α`, the inverse of the equivalence `(e : α ≃ β)` applied to `e(x)` recovers the original element `x`. In other words, $e^{-1}(e(x)) = x$.

EquivLike.coe_symm_comp_self theorem

{F} [EquivLike F α β] (e : F) : (e : α ≃ β).symm ∘ e = id

Full source

@[simp] lemma _root_.EquivLike.coe_symm_comp_self {F} [EquivLike F α β] (e : F) :
    (e : α ≃ β).symm ∘ e = id :=
  (e : α ≃ β).symm_comp_self

Inverse Composition with Equivalence Yields Identity

Informal description

For any type `F` that can be coerced to a bijection between types `α` and `β` (i.e., `[EquivLike F α β]`), and for any element `e : F`, the composition of the inverse equivalence `(e : α ≃ β).symm` with `e` is equal to the identity function on `α`, i.e., $e^{-1} \circ e = \text{id}_\alpha$.

EquivLike.self_comp_coe_symm theorem

{F} [EquivLike F α β] (e : F) : e ∘ (e : α ≃ β).symm = id

Full source

@[simp] lemma _root_.EquivLike.self_comp_coe_symm {F} [EquivLike F α β] (e : F) :
    e ∘ (e : α ≃ β).symm = id :=
  (e : α ≃ β).self_comp_symm

Composition of Equivalence-like Element with its Inverse Yields Identity: $e \circ e^{-1} = \text{id}_\beta$

Informal description

For any type `F` that satisfies `EquivLike F α β` (i.e., elements of `F` can be coerced to bijections between types `α` and `β`), and for any element `e : F`, the composition of `e` with the inverse of the coerced equivalence `(e : α ≃ β).symm` equals the identity function on `β`. In other words, $e \circ e^{-1} = \text{id}_\beta$.

Equiv.symm_trans_apply theorem

(f : α ≃ β) (g : β ≃ γ) (a : γ) : (f.trans g).symm a = f.symm (g.symm a)

Full source

@[simp] theorem symm_trans_apply (f : α ≃ β) (g : β ≃ γ) (a : γ) :
    (f.trans g).symm a = f.symm (g.symm a) := rfl

Inverse of Composition of Equivalences

Informal description

For any equivalences $f : \alpha \simeq \beta$ and $g : \beta \simeq \gamma$, and any element $a \in \gamma$, the inverse of the composition $f \circ g$ applied to $a$ equals the composition of the inverses $f^{-1} \circ g^{-1}$ applied to $a$, i.e., $(f \circ g)^{-1}(a) = f^{-1}(g^{-1}(a))$.

Equiv.symm_symm_apply theorem

(f : α ≃ β) (b : α) : f.symm.symm b = f b

Full source

theorem symm_symm_apply (f : α ≃ β) (b : α) : f.symm.symm b = f b := rfl

Double Inverse of Equivalence Preserves Original Function

Informal description

For any equivalence $f : \alpha \simeq \beta$ and any element $b \in \alpha$, applying the inverse of the inverse of $f$ to $b$ yields the same result as applying $f$ to $b$, i.e., $f^{-1^{-1}}(b) = f(b)$.

Equiv.apply_eq_iff_eq theorem

(f : α ≃ β) {x y : α} : f x = f y ↔ x = y

Full source

theorem apply_eq_iff_eq (f : α ≃ β) {x y : α} : f x = f y ↔ x = y := EquivLike.apply_eq_iff_eq f

Equivalence Preserves Equality: $f(x) = f(y) \leftrightarrow x = y$

Informal description

For any equivalence $f : \alpha \simeq \beta$ and any elements $x, y \in \alpha$, the equality $f(x) = f(y)$ holds if and only if $x = y$.

Equiv.apply_eq_iff_eq_symm_apply theorem

{x : α} {y : β} (f : α ≃ β) : f x = y ↔ x = f.symm y

Full source

theorem apply_eq_iff_eq_symm_apply {x : α} {y : β} (f : α ≃ β) : f x = y ↔ x = f.symm y := by
  conv_lhs => rw [← apply_symm_apply f y]
  rw [apply_eq_iff_eq]

Equivalence Application Equality: $f(x) = y \leftrightarrow x = f^{-1}(y)$

Informal description

For any equivalence $f : \alpha \simeq \beta$ and elements $x \in \alpha$, $y \in \beta$, the equality $f(x) = y$ holds if and only if $x = f^{-1}(y)$.

Equiv.cast_apply theorem

{α β} (h : α = β) (x : α) : Equiv.cast h x = cast h x

Full source

@[simp] theorem cast_apply {α β} (h : α = β) (x : α) : Equiv.cast h x = cast h x := rfl

Equivalence Cast Application Equals Type Cast

Informal description

For any types $\alpha$ and $\beta$, given a proof $h$ that $\alpha = \beta$, the application of the equivalence $\text{Equiv.cast } h$ to an element $x : \alpha$ is equal to casting $x$ along $h$, i.e., $\text{Equiv.cast } h (x) = \text{cast } h (x)$.

Equiv.cast_symm theorem

{α β} (h : α = β) : (Equiv.cast h).symm = Equiv.cast h.symm

Full source

@[simp] theorem cast_symm {α β} (h : α = β) : (Equiv.cast h).symm = Equiv.cast h.symm := rfl

Inverse of Type Cast Equivalence Equals Symmetric Cast

Informal description

For any types $\alpha$ and $\beta$ and a proof $h$ that $\alpha = \beta$, the inverse of the equivalence $\text{Equiv.cast } h$ is equal to the equivalence $\text{Equiv.cast } h^{-1}$, where $h^{-1}$ is the symmetry of $h$.

Equiv.cast_trans theorem

{α β γ} (h : α = β) (h2 : β = γ) : (Equiv.cast h).trans (Equiv.cast h2) = Equiv.cast (h.trans h2)

Full source

@[simp] theorem cast_trans {α β γ} (h : α = β) (h2 : β = γ) :
    (Equiv.cast h).trans (Equiv.cast h2) = Equiv.cast (h.trans h2) :=
  ext fun x => by substs h h2; rfl

Composition of Cast Equivalences Equals Cast of Transitive Equality

Informal description

For any types $\alpha$, $\beta$, and $\gamma$, given proofs $h : \alpha = \beta$ and $h2 : \beta = \gamma$, the composition of the equivalences $\text{Equiv.cast } h$ and $\text{Equiv.cast } h2$ is equal to the equivalence $\text{Equiv.cast } (h \cdot h2)$, where $h \cdot h2$ denotes the transitivity of equality proofs.

Equiv.cast_eq_iff_heq theorem

{α β} (h : α = β) {a : α} {b : β} : Equiv.cast h a = b ↔ HEq a b

Full source

theorem cast_eq_iff_heq {α β} (h : α = β) {a : α} {b : β} : Equiv.castEquiv.cast h a = b ↔ HEq a b := by
  subst h; simp [coe_refl]

Equivalence of Cast Equality and Hereditary Equality

Informal description

Given types $\alpha$ and $\beta$ with a proof $h$ that $\alpha = \beta$, for any elements $a : \alpha$ and $b : \beta$, the equality $\text{cast}_h(a) = b$ holds if and only if $a$ and $b$ are hereditarily equal (denoted $a \approx b$).

Equiv.symm_apply_eq theorem

{α β} (e : α ≃ β) {x y} : e.symm x = y ↔ x = e y

Full source

theorem symm_apply_eq {α β} (e : α ≃ β) {x y} : e.symm x = y ↔ x = e y :=
  ⟨fun H => by simp [H.symm], fun H => by simp [H]⟩

Inverse Equivalence Characterization: $e^{-1}(x) = y \leftrightarrow x = e(y)$

Informal description

For any equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and for any elements $x \in \beta$ and $y \in \alpha$, the equality $e^{-1}(x) = y$ holds if and only if $x = e(y)$.

Equiv.symm_symm theorem

(e : α ≃ β) : e.symm.symm = e

Full source

@[simp] theorem symm_symm (e : α ≃ β) : e.symm.symm = e := rfl

Double Inverse of Equivalence is Identity

Informal description

For any equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the double inverse of $e$ is equal to $e$ itself, i.e., $(e^{-1})^{-1} = e$.

Equiv.symm_bijective theorem

: Function.Bijective (Equiv.symm : (α ≃ β) → β ≃ α)

Full source

theorem symm_bijective : Function.Bijective (Equiv.symm : (α ≃ β) → β ≃ α) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Bijectivity of the Equivalence Inverse Operation

Informal description

The function $\text{symm} : (\alpha \simeq \beta) \to (\beta \simeq \alpha)$, which maps each equivalence to its inverse, is bijective. That is, it is both injective (distinct equivalences have distinct inverses) and surjective (every equivalence $\beta \simeq \alpha$ is the inverse of some equivalence $\alpha \simeq \beta$).

Equiv.trans_refl theorem

(e : α ≃ β) : e.trans (Equiv.refl β) = e

Full source

@[simp] theorem trans_refl (e : α ≃ β) : e.trans (Equiv.refl β) = e := by cases e; rfl

Right Identity Law for Equivalence Composition

Informal description

For any equivalence $e : \alpha \simeq \beta$, the composition of $e$ with the identity equivalence on $\beta$ is equal to $e$ itself, i.e., $e \circ \text{id}_\beta = e$.

Equiv.refl_symm theorem

: (Equiv.refl α).symm = Equiv.refl α

Full source

@[simp] theorem refl_symm : (Equiv.refl α).symm = Equiv.refl α := rfl

Inverse of Identity Equivalence is Identity

Informal description

The inverse of the identity equivalence on a type $\alpha$ is equal to the identity equivalence on $\alpha$, i.e., $(\text{refl}_\alpha)^{-1} = \text{refl}_\alpha$.

Equiv.refl_trans theorem

(e : α ≃ β) : (Equiv.refl α).trans e = e

Full source

@[simp] theorem refl_trans (e : α ≃ β) : (Equiv.refl α).trans e = e := by cases e; rfl

Identity Equivalence is Left Neutral for Composition

Informal description

For any equivalence $e : \alpha \simeq \beta$, the composition of the identity equivalence on $\alpha$ with $e$ is equal to $e$ itself, i.e., $(\text{refl}_\alpha) \circ e = e$.

Equiv.symm_trans_self theorem

(e : α ≃ β) : e.symm.trans e = Equiv.refl β

Full source

@[simp] theorem symm_trans_self (e : α ≃ β) : e.symm.trans e = Equiv.refl β := ext <| by simp

Inverse-Then-Forward Composition Yields Identity: $e^{-1} \circ e = \text{id}_\beta$

Informal description

For any equivalence $e : \alpha \simeq \beta$, the composition of its inverse $e^{-1} : \beta \simeq \alpha$ with $e$ itself yields the identity equivalence on $\beta$, i.e., $e^{-1} \circ e = \text{id}_\beta$.

Equiv.self_trans_symm theorem

(e : α ≃ β) : e.trans e.symm = Equiv.refl α

Full source

@[simp] theorem self_trans_symm (e : α ≃ β) : e.trans e.symm = Equiv.refl α := ext <| by simp

Composition of Equivalence with its Inverse Yields Identity

Informal description

For any equivalence $e : \alpha \simeq \beta$, the composition of $e$ with its inverse $e^{-1}$ yields the identity equivalence on $\alpha$, i.e., $e \circ e^{-1} = \text{id}_\alpha$.

Equiv.trans_assoc theorem

{δ} (ab : α ≃ β) (bc : β ≃ γ) (cd : γ ≃ δ) : (ab.trans bc).trans cd = ab.trans (bc.trans cd)

Full source

theorem trans_assoc {δ} (ab : α ≃ β) (bc : β ≃ γ) (cd : γ ≃ δ) :
    (ab.trans bc).trans cd = ab.trans (bc.trans cd) := Equiv.ext fun _ => rfl

Associativity of Equivalence Composition

Informal description

For any types $\alpha, \beta, \gamma, \delta$ and equivalences $ab : \alpha \simeq \beta$, $bc : \beta \simeq \gamma$, $cd : \gamma \simeq \delta$, the composition of equivalences is associative, i.e., $(ab \circ bc) \circ cd = ab \circ (bc \circ cd)$.

Equiv.leftInverse_symm theorem

(f : Equiv α β) : LeftInverse f.symm f

Full source

theorem leftInverse_symm (f : Equiv α β) : LeftInverse f.symm f := f.left_inv

Inverse of Equivalence is Left Inverse

Informal description

For any equivalence $f : \alpha \simeq \beta$, the inverse equivalence $f^{-1} : \beta \simeq \alpha$ is a left inverse of $f$, meaning that $f^{-1} \circ f = \text{id}_\alpha$.

Equiv.rightInverse_symm theorem

(f : Equiv α β) : Function.RightInverse f.symm f

Full source

theorem rightInverse_symm (f : Equiv α β) : Function.RightInverse f.symm f := f.right_inv

Inverse of Equivalence is Right Inverse

Informal description

For any equivalence $f : \alpha \simeq \beta$, the inverse equivalence $f^{-1} : \beta \simeq \alpha$ is a right inverse of $f$, meaning that $f \circ f^{-1} = \text{id}_\beta$.

Equiv.injective_comp theorem

(e : α ≃ β) (f : β → γ) : Injective (f ∘ e) ↔ Injective f

Full source

theorem injective_comp (e : α ≃ β) (f : β → γ) : InjectiveInjective (f ∘ e) ↔ Injective f :=
  EquivLike.injective_comp e f

Injectivity of Composition with Equivalence: $f \circ e$ is injective $\leftrightarrow$ $f$ is injective

Informal description

For any equivalence $e : \alpha \simeq \beta$ and any function $f : \beta \to \gamma$, the composition $f \circ e$ is injective if and only if $f$ is injective.

Equiv.comp_injective theorem

(f : α → β) (e : β ≃ γ) : Injective (e ∘ f) ↔ Injective f

Full source

theorem comp_injective (f : α → β) (e : β ≃ γ) : InjectiveInjective (e ∘ f) ↔ Injective f :=
  EquivLike.comp_injective f e

Injectivity of Composition with Equivalence: $e \circ f$ injective $\leftrightarrow$ $f$ injective

Informal description

For any function $f \colon \alpha \to \beta$ and any equivalence $e \colon \beta \simeq \gamma$, the composition $e \circ f$ is injective if and only if $f$ is injective.

Equiv.surjective_comp theorem

(e : α ≃ β) (f : β → γ) : Surjective (f ∘ e) ↔ Surjective f

Full source

theorem surjective_comp (e : α ≃ β) (f : β → γ) : SurjectiveSurjective (f ∘ e) ↔ Surjective f :=
  EquivLike.surjective_comp e f

Surjectivity of Composition with Equivalence

Informal description

For any equivalence $e : \alpha \simeq \beta$ and any function $f : \beta \to \gamma$, the composition $f \circ e$ is surjective if and only if $f$ is surjective.

Equiv.comp_surjective theorem

(f : α → β) (e : β ≃ γ) : Surjective (e ∘ f) ↔ Surjective f

Full source

theorem comp_surjective (f : α → β) (e : β ≃ γ) : SurjectiveSurjective (e ∘ f) ↔ Surjective f :=
  EquivLike.comp_surjective f e

Surjectivity of Composition with Equivalence: $e \circ f$ surjective $\leftrightarrow$ $f$ surjective

Informal description

For any function $f \colon \alpha \to \beta$ and any equivalence $e \colon \beta \simeq \gamma$, the composition $e \circ f$ is surjective if and only if $f$ is surjective.

Equiv.bijective_comp theorem

(e : α ≃ β) (f : β → γ) : Bijective (f ∘ e) ↔ Bijective f

Full source

theorem bijective_comp (e : α ≃ β) (f : β → γ) : BijectiveBijective (f ∘ e) ↔ Bijective f :=
  EquivLike.bijective_comp e f

Bijectivity of Composition with Equivalence: $f \circ e$ is bijective iff $f$ is bijective

Informal description

For any equivalence $e : \alpha \simeq \beta$ and any function $f : \beta \to \gamma$, the composition $f \circ e$ is bijective if and only if $f$ is bijective.

Equiv.comp_bijective theorem

(f : α → β) (e : β ≃ γ) : Bijective (e ∘ f) ↔ Bijective f

Full source

theorem comp_bijective (f : α → β) (e : β ≃ γ) : BijectiveBijective (e ∘ f) ↔ Bijective f :=
  EquivLike.comp_bijective f e

Bijectivity Preservation under Composition with Equivalence: $e \circ f$ bijective $\leftrightarrow$ $f$ bijective

Informal description

For any function $f \colon \alpha \to \beta$ and any equivalence $e \colon \beta \simeq \gamma$, the composition $e \circ f$ is bijective if and only if $f$ is bijective.

Equiv.equivCongr definition

{δ : Sort*} (ab : α ≃ β) (cd : γ ≃ δ) : (α ≃ γ) ≃ (β ≃ δ)

Full source

/-- If `α` is equivalent to `β` and `γ` is equivalent to `δ`, then the type of equivalences `α ≃ γ`
is equivalent to the type of equivalences `β ≃ δ`. -/
def equivCongr {δ : Sort*} (ab : α ≃ β) (cd : γ ≃ δ) : (α ≃ γ) ≃ (β ≃ δ) where
  toFun ac := (ab.symm.trans ac).trans cd
  invFun bd := ab.trans <| bd.trans <| cd.symm
  left_inv ac := by ext x; simp only [trans_apply, comp_apply, symm_apply_apply]
  right_inv ac := by ext x; simp only [trans_apply, comp_apply, apply_symm_apply]

Equivalence of Equivalence Types

Informal description

Given equivalences $ab : \alpha \simeq \beta$ and $cd : \gamma \simeq \delta$, the function `Equiv.equivCongr` constructs an equivalence between the types of equivalences $\alpha \simeq \gamma$ and $\beta \simeq \delta$. Specifically: - The forward map takes an equivalence $ac : \alpha \simeq \gamma$ and returns the equivalence $\beta \simeq \delta$ obtained by composing $ab^{-1}$, $ac$, and $cd$. - The inverse map takes an equivalence $bd : \beta \simeq \delta$ and returns the equivalence $\alpha \simeq \gamma$ obtained by composing $ab$, $bd$, and $cd^{-1}$.

Equiv.equivCongr_refl theorem

{α β} : (Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β)

Full source

@[simp] theorem equivCongr_refl {α β} :
    (Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β) := by ext; rfl

Identity Equivalence Construction via `equivCongr` Yields Identity

Informal description

For any types $\alpha$ and $\beta$, the equivalence obtained by applying `equivCongr` to the identity equivalences on $\alpha$ and $\beta$ is equal to the identity equivalence on the type of equivalences $\alpha \simeq \beta$. In other words, if we construct an equivalence between $\alpha \simeq \gamma$ and $\beta \simeq \delta$ using the identity equivalences $\text{refl}_\alpha$ and $\text{refl}_\beta$, the result is the identity equivalence on $\alpha \simeq \beta$.

Equiv.equivCongr_symm theorem

{δ} (ab : α ≃ β) (cd : γ ≃ δ) : (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm

Full source

@[simp] theorem equivCongr_symm {δ} (ab : α ≃ β) (cd : γ ≃ δ) :
    (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm := by ext; rfl

Inverse of Equivalence Congruence is Congruence of Inverses

Informal description

Given equivalences $ab : \alpha \simeq \beta$ and $cd : \gamma \simeq \delta$, the inverse of the equivalence $ab.equivCongr\ cd : (\alpha \simeq \gamma) \simeq (\beta \simeq \delta)$ is equal to the equivalence constructed by applying $equivCongr$ to the inverses $ab.symm$ and $cd.symm$, i.e., $(ab.equivCongr\ cd).symm = ab.symm.equivCongr\ cd.symm$.

Equiv.equivCongr_trans theorem

 {δ ε ζ} (ab : α ≃ β) (de : δ ≃ ε) (bc : β ≃ γ) (ef : ε ≃ ζ) :
  (ab.equivCongr de).trans (bc.equivCongr ef) = (ab.trans bc).equivCongr (de.trans ef)

Full source

@[simp] theorem equivCongr_trans {δ ε ζ} (ab : α ≃ β) (de : δ ≃ ε) (bc : β ≃ γ) (ef : ε ≃ ζ) :
    (ab.equivCongr de).trans (bc.equivCongr ef) = (ab.trans bc).equivCongr (de.trans ef) := by
  ext; rfl

Composition of Equivalence Congruences

Informal description

Given equivalences $ab : \alpha \simeq \beta$, $de : \delta \simeq \varepsilon$, $bc : \beta \simeq \gamma$, and $ef : \varepsilon \simeq \zeta$, the composition of the equivalences $(ab.\text{equivCongr}\ de)$ and $(bc.\text{equivCongr}\ ef)$ is equal to the equivalence obtained by applying $\text{equivCongr}$ to the compositions $ab \circ bc$ and $de \circ ef$. In other words: $$(ab.\text{equivCongr}\ de) \circ (bc.\text{equivCongr}\ ef) = (ab \circ bc).\text{equivCongr}\ (de \circ ef)$$

Equiv.equivCongr_refl_left theorem

{α β γ} (bg : β ≃ γ) (e : α ≃ β) : (Equiv.refl α).equivCongr bg e = e.trans bg

Full source

@[simp] theorem equivCongr_refl_left {α β γ} (bg : β ≃ γ) (e : α ≃ β) :
    (Equiv.refl α).equivCongr bg e = e.trans bg := rfl

Left Identity Property of Equivalence Composition via `equivCongr`

Informal description

For any types $\alpha$, $\beta$, and $\gamma$, given an equivalence $bg : \beta \simeq \gamma$ and an equivalence $e : \alpha \simeq \beta$, the composition of the identity equivalence on $\alpha$ with $bg$ applied to $e$ is equal to the composition of $e$ with $bg$. In other words: $$(\mathrm{id}_\alpha).\mathrm{equivCongr}\, bg\, e = e \circ bg$$ where $\mathrm{id}_\alpha$ denotes the identity equivalence on $\alpha$ and $\circ$ denotes composition of equivalences.

Equiv.equivCongr_refl_right theorem

{α β} (ab e : α ≃ β) : ab.equivCongr (Equiv.refl β) e = ab.symm.trans e

Full source

@[simp] theorem equivCongr_refl_right {α β} (ab e : α ≃ β) :
    ab.equivCongr (Equiv.refl β) e = ab.symm.trans e := rfl

Right Identity Law for Equivalence Composition

Informal description

For any equivalences $ab, e : \alpha \simeq \beta$, the composition of $ab$ with the identity equivalence on $\beta$ applied to $e$ is equal to the composition of the inverse of $ab$ with $e$, i.e., \[ ab.\text{equivCongr}(\text{refl}_\beta)(e) = ab^{-1} \circ e. \]

Equiv.equivCongr_apply_apply theorem

{δ} (ab : α ≃ β) (cd : γ ≃ δ) (e : α ≃ γ) (x) : ab.equivCongr cd e x = cd (e (ab.symm x))

Full source

@[simp] theorem equivCongr_apply_apply {δ} (ab : α ≃ β) (cd : γ ≃ δ) (e : α ≃ γ) (x) :
    ab.equivCongr cd e x = cd (e (ab.symm x)) := rfl

Commutativity of Equivalence Congruence Application

Informal description

Given equivalences $ab : \alpha \simeq \beta$ and $cd : \gamma \simeq \delta$, and an equivalence $e : \alpha \simeq \gamma$, for any element $x \in \beta$, the application of the equivalence $ab.equivCongr\ cd\ e$ to $x$ is equal to $cd(e(ab^{-1}(x)))$. In other words, the following diagram commutes: \[ \begin{CD} \beta @>{ab.equivCongr\ cd\ e}>> \delta \\ @A{ab^{-1}}AA @VV{cd}V \\ \alpha @>>{e}> \gamma \end{CD} \]

Equiv.permCongr definition

: Perm α' ≃ Perm β'

Full source

/-- If `α` is equivalent to `β`, then `Perm α` is equivalent to `Perm β`. -/
def permCongr : PermPerm α' ≃ Perm β' := equivCongr e e

Permutation conjugation by equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$, the function `Equiv.permCongr` constructs an equivalence between the permutation groups `Perm α` and `Perm β`. Specifically, it maps a permutation $p$ of $\alpha$ to the permutation of $\beta$ obtained by conjugating $p$ with $e$, i.e., $e \circ p \circ e^{-1}$.

Equiv.permCongr_def theorem

(p : Equiv.Perm α') : e.permCongr p = (e.symm.trans p).trans e

Full source

theorem permCongr_def (p : Equiv.Perm α') : e.permCongr p = (e.symm.trans p).trans e := rfl

Definition of Permutation Conjugation via Equivalence Composition

Informal description

For any permutation $p$ of a type $\alpha$ and any equivalence $e : \alpha \simeq \beta$, the conjugation of $p$ by $e$ is equal to the composition of equivalences $e^{-1} \circ p \circ e$, i.e., \[ e.permCongr\ p = e^{-1} \circ p \circ e. \]

Equiv.permCongr_refl theorem

: e.permCongr (Equiv.refl _) = Equiv.refl _

Full source

@[simp] theorem permCongr_refl : e.permCongr (Equiv.refl _) = Equiv.refl _ := by
  simp [permCongr_def]

Conjugation of Identity Permutation Yields Identity

Informal description

Given an equivalence $e : \alpha \simeq \beta$, the conjugation of the identity permutation on $\alpha$ by $e$ yields the identity permutation on $\beta$, i.e., $e \circ \text{id}_\alpha \circ e^{-1} = \text{id}_\beta$.

Equiv.permCongr_symm theorem

: e.permCongr.symm = e.symm.permCongr

Full source

@[simp] theorem permCongr_symm : e.permCongr.symm = e.symm.permCongr := rfl

Inverse of Permutation Conjugation by Equivalence

Informal description

For any equivalence $e : \alpha \simeq \beta$, the inverse of the permutation conjugation map $e.\text{permCongr}$ is equal to the permutation conjugation map of the inverse equivalence $e^{-1}.\text{permCongr}$.

Equiv.permCongr_apply theorem

(p : Equiv.Perm α') (x) : e.permCongr p x = e (p (e.symm x))

Full source

@[simp] theorem permCongr_apply (p : Equiv.Perm α') (x) : e.permCongr p x = e (p (e.symm x)) := rfl

Action of Conjugated Permutation via Equivalence

Informal description

For any equivalence $e : \alpha \simeq \beta$, permutation $p$ of $\alpha$, and element $x \in \beta$, the action of the conjugated permutation $e.permCongr\, p$ on $x$ is given by $e(p(e^{-1}(x)))$, where $e^{-1}$ is the inverse of $e$.

Equiv.permCongr_symm_apply theorem

(p : Equiv.Perm β') (x) : e.permCongr.symm p x = e.symm (p (e x))

Full source

theorem permCongr_symm_apply (p : Equiv.Perm β') (x) :
    e.permCongr.symm p x = e.symm (p (e x)) := rfl

Inverse Permutation Conjugation Formula via Equivalence

Informal description

For any equivalence $e : \alpha \simeq \beta$, permutation $p$ of $\beta$, and element $x \in \alpha$, the action of the inverse of the permutation conjugation $e.\text{permCongr}$ on $p$ at $x$ is given by $(e.\text{permCongr})^{-1}(p)(x) = e^{-1}(p(e(x)))$.

Equiv.permCongr_trans theorem

(p p' : Equiv.Perm α') : (e.permCongr p).trans (e.permCongr p') = e.permCongr (p.trans p')

Full source

theorem permCongr_trans (p p' : Equiv.Perm α') :
    (e.permCongr p).trans (e.permCongr p') = e.permCongr (p.trans p') := by
  ext; simp only [trans_apply, comp_apply, permCongr_apply, symm_apply_apply]

Composition of Conjugated Permutations Equals Conjugation of Compositions

Informal description

Given an equivalence $e : \alpha \simeq \beta$ and two permutations $p, p'$ of $\alpha$, the composition of the conjugated permutations $e \circ p \circ e^{-1}$ and $e \circ p' \circ e^{-1}$ is equal to the conjugation of the composition $p \circ p'$, i.e., $(e \circ p \circ e^{-1}) \circ (e \circ p' \circ e^{-1}) = e \circ (p \circ p') \circ e^{-1}$.

Equiv.equivOfIsEmpty definition

(α β : Sort*) [IsEmpty α] [IsEmpty β] : α ≃ β

Full source

/-- Two empty types are equivalent. -/
def equivOfIsEmpty (α β : Sort*) [IsEmpty α] [IsEmpty β] : α ≃ β :=
  ⟨isEmptyElim, isEmptyElim, isEmptyElim, isEmptyElim⟩

Equivalence between empty types

Informal description

Given two empty types $\alpha$ and $\beta$, there exists a bijection between them, represented as an equivalence $\alpha \simeq \beta$. This equivalence is constructed using the elimination principle for empty types.

Equiv.equivEmpty definition

(α : Sort u) [IsEmpty α] : α ≃ Empty

Full source

/-- If `α` is an empty type, then it is equivalent to the `Empty` type. -/
def equivEmpty (α : Sort u) [IsEmpty α] : α ≃ Empty := equivOfIsEmpty α _

Equivalence between an empty type and the empty type

Informal description

For any empty type $\alpha$, there exists a bijection between $\alpha$ and the empty type `Empty`. This equivalence is constructed using the elimination principle for empty types.

Equiv.equivPEmpty definition

(α : Sort v) [IsEmpty α] : α ≃ PEmpty.{u}

Full source

/-- If `α` is an empty type, then it is equivalent to the `PEmpty` type in any universe. -/
def equivPEmpty (α : Sort v) [IsEmpty α] : α ≃ PEmpty.{u} := equivOfIsEmpty α _

Equivalence between an empty type and the polymorphic empty type

Informal description

For any empty type $\alpha$ in universe `v`, there exists a bijection between $\alpha$ and the polymorphic empty type `PEmpty` in universe `u$. This equivalence is constructed using the elimination principle for empty types.

Equiv.equivEmptyEquiv definition

(α : Sort u) : α ≃ Empty ≃ IsEmpty α

Full source

/-- `α` is equivalent to an empty type iff `α` is empty. -/
def equivEmptyEquiv (α : Sort u) : α ≃ Emptyα ≃ Empty ≃ IsEmpty α :=
  ⟨fun e => Function.isEmpty e, @equivEmpty α, fun e => ext fun x => (e x).elim, fun _ => rfl⟩

Equivalence between a type and the empty type is equivalent to the type being empty

Informal description

For any type $\alpha$, the existence of a bijection between $\alpha$ and the empty type `Empty` is equivalent to $\alpha$ being empty.

Equiv.propEquivPEmpty definition

{p : Prop} (h : ¬p) : p ≃ PEmpty

Full source

/-- The `Sort` of proofs of a false proposition is equivalent to `PEmpty`. -/
def propEquivPEmpty {p : Prop} (h : ¬p) : p ≃ PEmpty := @equivPEmpty p <| IsEmpty.prop_iff.2 h

Bijection between false proposition and empty type

Informal description

For any false proposition $p$, there exists a bijection between the type of proofs of $p$ and the polymorphic empty type `PEmpty`. This equivalence is constructed using the fact that a proposition is false if and only if its proof type is empty.

Equiv.ofUnique definition

(α β : Sort _) [Unique.{u} α] [Unique.{v} β] : α ≃ β

Full source

/-- If both `α` and `β` have a unique element, then `α ≃ β`. -/
def ofUnique (α β : Sort _) [Unique.{u} α] [Unique.{v} β] : α ≃ β where
  toFun := default
  invFun := default
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

Bijection between types with unique elements

Informal description

Given two types $\alpha$ and $\beta$ each with a unique element, there exists a bijection between them. The bijection maps the unique element of $\alpha$ to the unique element of $\beta$ and vice versa.

Equiv.equivPUnit definition

(α : Sort u) [Unique α] : α ≃ PUnit.{v}

Full source

/-- If `α` has a unique element, then it is equivalent to any `PUnit`. -/
def equivPUnit (α : Sort u) [Unique α] : α ≃ PUnit.{v} := ofUnique α _

Bijection between a unique type and the singleton type

Informal description

For any type $\alpha$ with a unique element, there exists a bijection between $\alpha$ and the singleton type `PUnit.{v}`. This bijection maps the unique element of $\alpha$ to the unique element of `PUnit` and vice versa.

Equiv.propEquivPUnit definition

{p : Prop} (h : p) : p ≃ PUnit.{0}

Full source

/-- The `Sort` of proofs of a true proposition is equivalent to `PUnit`. -/
def propEquivPUnit {p : Prop} (h : p) : p ≃ PUnit.{0} := @equivPUnit p <| uniqueProp h

Bijection between proofs of a true proposition and the singleton type

Informal description

For any true proposition $p$, there exists a bijection between the type of proofs of $p$ and the singleton type `PUnit`. This bijection maps any proof of $p$ to the unique element of `PUnit` and vice versa.

Equiv.ulift definition

{α : Type v} : ULift.{u} α ≃ α

Full source

/-- `ULift α` is equivalent to `α`. -/
@[simps -fullyApplied apply]
protected def ulift {α : Type v} : ULiftULift.{u} α ≃ α :=
  ⟨ULift.down, ULift.up, ULift.up_down, ULift.down_up.{v, u}⟩

Equivalence between `ULift α` and `α`

Informal description

The equivalence `Equiv.ulift` establishes a bijection between the type `ULift α` and `α`, where `ULift.down` maps an element of `ULift α` to its underlying value in `α`, and `ULift.up` maps an element of `α` back to `ULift α`. These maps are mutual inverses, satisfying `ULift.up_down` and `ULift.down_up`.

Equiv.plift definition

: PLift α ≃ α

Full source

/-- `PLift α` is equivalent to `α`. -/
@[simps -fullyApplied apply]
protected def plift : PLiftPLift α ≃ α := ⟨PLift.down, PLift.up, PLift.up_down, PLift.down_up⟩

Equivalence between `PLift α` and `α`

Informal description

The equivalence `Equiv.plift` establishes a bijection between the type `PLift α` and `α`, where `PLift.down` maps an element of `PLift α` to its underlying value in `α`, and `PLift.up` maps an element of `α` back to `PLift α`. These maps are mutual inverses, satisfying `PLift.up_down` and `PLift.down_up`.

Equiv.ofIff definition

{P Q : Prop} (h : P ↔ Q) : P ≃ Q

Full source

/-- equivalence of propositions is the same as iff -/
def ofIff {P Q : Prop} (h : P ↔ Q) : P ≃ Q := ⟨h.mp, h.mpr, fun _ => rfl, fun _ => rfl⟩

Equivalence of Propositions via Logical Equivalence

Informal description

Given two propositions $ P $ and $ Q $ and a proof $ h $ that $ P $ is logically equivalent to $ Q $, the function `Equiv.ofIff` constructs an equivalence $ P \simeq Q $ between the types corresponding to these propositions. This equivalence consists of the forward implication $ h $.mp from $ P $ to $ Q $, the backward implication $ h $.mpr from $ Q $ to $ P $, and proofs that these functions are mutual inverses.

Equiv.arrowCongr definition

 {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (α₁ → β₁) ≃ (α₂ → β₂)

Full source

/-- If `α₁` is equivalent to `α₂` and `β₁` is equivalent to `β₂`, then the type of maps `α₁ → β₁`
is equivalent to the type of maps `α₂ → β₂`. -/
@[simps apply]
def arrowCongr {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (α₁ → β₁) ≃ (α₂ → β₂) where
  toFun f := e₂ ∘ f ∘ e₁.symm
  invFun f := e₂.symm ∘ f ∘ e₁
  left_inv f := funext fun x => by simp only [comp_apply, symm_apply_apply]
  right_inv f := funext fun x => by simp only [comp_apply, apply_symm_apply]

Equivalence of function spaces via domain and codomain equivalences

Informal description

Given equivalences $e₁ : α₁ ≃ α₂$ and $e₂ : β₁ ≃ β₂$, the function `Equiv.arrowCongr` constructs an equivalence $(α₁ → β₁) ≃ (α₂ → β₂)$ between function types. Specifically: - The forward map sends $f : α₁ → β₁$ to $e₂ ∘ f ∘ e₁^{-1} : α₂ → β₂$ - The inverse map sends $g : α₂ → β₂$ to $e₂^{-1} ∘ g ∘ e₁ : α₁ → β₁$ These maps are mutual inverses, establishing a bijection between the function spaces.

Equiv.arrowCongr_comp theorem

 {α₁ β₁ γ₁ α₂ β₂ γ₂ : Sort*} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (ec : γ₁ ≃ γ₂) (f : α₁ → β₁) (g : β₁ → γ₁) :
  arrowCongr ea ec (g ∘ f) = arrowCongr eb ec g ∘ arrowCongr ea eb f

Full source

theorem arrowCongr_comp {α₁ β₁ γ₁ α₂ β₂ γ₂ : Sort*} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (ec : γ₁ ≃ γ₂)
    (f : α₁ → β₁) (g : β₁ → γ₁) :
    arrowCongr ea ec (g ∘ f) = arrowCongrarrowCongr eb ec g ∘ arrowCongr ea eb f := by
  ext; simp only [comp, arrowCongr_apply, eb.symm_apply_apply]

Composition of Function Space Equivalences via $\text{arrowCongr}$

Informal description

For any equivalences $e_a : \alpha_1 \simeq \alpha_2$, $e_b : \beta_1 \simeq \beta_2$, and $e_c : \gamma_1 \simeq \gamma_2$, and any functions $f : \alpha_1 \to \beta_1$ and $g : \beta_1 \to \gamma_1$, the following equality holds: \[ \text{arrowCongr } e_a e_c (g \circ f) = (\text{arrowCongr } e_b e_c g) \circ (\text{arrowCongr } e_a e_b f) \] Here, $\text{arrowCongr}$ constructs an equivalence between function spaces using the given equivalences on domains and codomains, and $\circ$ denotes function composition.

Equiv.arrowCongr_refl theorem

{α β : Sort*} : arrowCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α → β)

Full source

@[simp] theorem arrowCongr_refl {α β : Sort*} :
    arrowCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α → β) := rfl

Identity Equivalence Induces Identity on Function Spaces

Informal description

For any types $\alpha$ and $\beta$, the equivalence `arrowCongr` constructed from the identity equivalences on $\alpha$ and $\beta$ is equal to the identity equivalence on the function type $\alpha \to \beta$. In other words, the equivalence of function spaces induced by identity equivalences is itself an identity equivalence.

Equiv.arrowCongr_trans theorem

 {α₁ α₂ α₃ β₁ β₂ β₃ : Sort*} (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) :
  arrowCongr (e₁.trans e₂) (e₁'.trans e₂') = (arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂')

Full source

@[simp] theorem arrowCongr_trans {α₁ α₂ α₃ β₁ β₂ β₃ : Sort*}
    (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) :
    arrowCongr (e₁.trans e₂) (e₁'.trans e₂') = (arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂') := rfl

Composition Law for Function Space Equivalences via Domain and Codomain Equivalences

Informal description

For any types $α₁, α₂, α₃, β₁, β₂, β₃$ and equivalences $e₁ : α₁ ≃ α₂$, $e₁' : β₁ ≃ β₂$, $e₂ : α₂ ≃ α₃$, $e₂' : β₂ ≃ β₃$, the following equality holds: \[ \text{arrowCongr}(e₁ \circ e₂, e₁' \circ e₂') = \text{arrowCongr}(e₁, e₁') \circ \text{arrowCongr}(e₂, e₂') \] Here, $\text{arrowCongr}$ constructs an equivalence between function spaces, and $\circ$ denotes the composition of equivalences.

Equiv.arrowCongr_symm theorem

 {α₁ α₂ β₁ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (arrowCongr e₁ e₂).symm = arrowCongr e₁.symm e₂.symm

Full source

@[simp] theorem arrowCongr_symm {α₁ α₂ β₁ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
    (arrowCongr e₁ e₂).symm = arrowCongr e₁.symm e₂.symm := rfl

Inverse of Function Space Equivalence via Domain and Codomain Inverses

Informal description

For any types $\alpha_1, \alpha_2, \beta_1, \beta_2$ and equivalences $e_1 : \alpha_1 \simeq \alpha_2$, $e_2 : \beta_1 \simeq \beta_2$, the inverse of the function space equivalence $\text{arrowCongr}(e_1, e_2)$ is equal to the function space equivalence constructed from the inverses of $e_1$ and $e_2$, i.e., \[ (\text{arrowCongr}(e_1, e_2))^{-1} = \text{arrowCongr}(e_1^{-1}, e_2^{-1}). \]

Equiv.arrowCongr' definition

 {α₁ β₁ α₂ β₂ : Type*} (hα : α₁ ≃ α₂) (hβ : β₁ ≃ β₂) : (α₁ → β₁) ≃ (α₂ → β₂)

Full source

/-- A version of `Equiv.arrowCongr` in `Type`, rather than `Sort`.

The `equiv_rw` tactic is not able to use the default `Sort` level `Equiv.arrowCongr`,
because Lean's universe rules will not unify `?l_1` with `imax (1 ?m_1)`.
-/
@[simps! apply]
def arrowCongr' {α₁ β₁ α₂ β₂ : Type*} (hα : α₁ ≃ α₂) (hβ : β₁ ≃ β₂) : (α₁ → β₁) ≃ (α₂ → β₂) :=
  Equiv.arrowCongr hα hβ

Type-level equivalence of function spaces via domain and codomain equivalences

Informal description

Given equivalences $h_\alpha : \alpha_1 \simeq \alpha_2$ and $h_\beta : \beta_1 \simeq \beta_2$ between types, the function `Equiv.arrowCongr'` constructs an equivalence $(\alpha_1 \to \beta_1) \simeq (\alpha_2 \to \beta_2)$ between the corresponding function types. Specifically: - The forward map sends $f : \alpha_1 \to \beta_1$ to $h_\beta \circ f \circ h_\alpha^{-1} : \alpha_2 \to \beta_2$ - The inverse map sends $g : \alpha_2 \to \beta_2$ to $h_\beta^{-1} \circ g \circ h_\alpha : \alpha_1 \to \beta_1$ These maps are mutual inverses, establishing a bijection between the function spaces.

Equiv.arrowCongr'_refl theorem

{α β : Type*} : arrowCongr' (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α → β)

Full source

@[simp] theorem arrowCongr'_refl {α β : Type*} :
    arrowCongr' (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α → β) := rfl

Identity Function Space Equivalence via Identity Domain and Codomain Equivalences

Informal description

For any types $\alpha$ and $\beta$, the function space equivalence constructed from the identity equivalences on $\alpha$ and $\beta$ is equal to the identity equivalence on the function type $\alpha \to \beta$. In other words, the equivalence $\text{arrowCongr'}(\text{refl}\,\alpha, \text{refl}\,\beta)$ is exactly $\text{refl}(\alpha \to \beta)$.

Equiv.arrowCongr'_trans theorem

 {α₁ α₂ β₁ β₂ α₃ β₃ : Type*} (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) :
  arrowCongr' (e₁.trans e₂) (e₁'.trans e₂') = (arrowCongr' e₁ e₁').trans (arrowCongr' e₂ e₂')

Full source

@[simp] theorem arrowCongr'_trans {α₁ α₂ β₁ β₂ α₃ β₃ : Type*}
    (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) :
    arrowCongr' (e₁.trans e₂) (e₁'.trans e₂') = (arrowCongr' e₁ e₁').trans (arrowCongr' e₂ e₂') :=
  rfl

Composition Property of Function Space Equivalence via Domain and Codomain Equivalences

Informal description

For any types $\alpha_1, \alpha_2, \alpha_3, \beta_1, \beta_2, \beta_3$ and equivalences $e_1 : \alpha_1 \simeq \alpha_2$, $e_1' : \beta_1 \simeq \beta_2$, $e_2 : \alpha_2 \simeq \alpha_3$, $e_2' : \beta_2 \simeq \beta_3$, the following equality holds: $$\text{arrowCongr'}\, (e_1 \circ e_2)\, (e_1' \circ e_2') = (\text{arrowCongr'}\, e_1\, e_1') \circ (\text{arrowCongr'}\, e_2\, e_2').$$ Here, $\text{arrowCongr'}$ constructs an equivalence between function spaces, and $\circ$ denotes composition of equivalences.

Equiv.arrowCongr'_symm theorem

 {α₁ α₂ β₁ β₂ : Type*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (arrowCongr' e₁ e₂).symm = arrowCongr' e₁.symm e₂.symm

Full source

@[simp] theorem arrowCongr'_symm {α₁ α₂ β₁ β₂ : Type*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
    (arrowCongr' e₁ e₂).symm = arrowCongr' e₁.symm e₂.symm := rfl

Inverse of Function Space Equivalence via Domain and Codomain Inverses

Informal description

For any types $\alpha_1, \alpha_2, \beta_1, \beta_2$ and equivalences $e_1 : \alpha_1 \simeq \alpha_2$ and $e_2 : \beta_1 \simeq \beta_2$, the inverse of the function space equivalence $\text{arrowCongr'}\, e_1\, e_2$ is equal to the function space equivalence constructed from the inverses, i.e., $$(\text{arrowCongr'}\, e_1\, e_2)^{-1} = \text{arrowCongr'}\, e_1^{-1}\, e_2^{-1}.$$

Equiv.conj definition

(e : α ≃ β) : (α → α) ≃ (β → β)

Full source

/-- Conjugate a map `f : α → α` by an equivalence `α ≃ β`. -/
@[simps! apply] def conj (e : α ≃ β) : (α → α) ≃ (β → β) := arrowCongr e e

Conjugation of endomorphisms by an equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$, the function `Equiv.conj` constructs an equivalence $(\alpha \to \alpha) \simeq (\beta \to \beta)$ between endomorphism types by conjugating with $e$. Specifically: - The forward map sends $f : \alpha \to \alpha$ to $e \circ f \circ e^{-1} : \beta \to \beta$ - The inverse map sends $g : \beta \to \beta$ to $e^{-1} \circ g \circ e : \alpha \to \alpha$ These maps are mutual inverses, establishing a bijection between the endomorphism spaces.

Equiv.conj_refl theorem

: conj (Equiv.refl α) = Equiv.refl (α → α)

Full source

@[simp] theorem conj_refl : conj (Equiv.refl α) = Equiv.refl (α → α) := rfl

Conjugation of Identity Equivalence Yields Identity on Endomorphisms

Informal description

The conjugation of the identity equivalence $\text{refl}_\alpha$ on a type $\alpha$ is equal to the identity equivalence on the endomorphism space $\alpha \to \alpha$, i.e., $\text{conj}(\text{refl}_\alpha) = \text{refl}_{\alpha \to \alpha}$.

Equiv.conj_symm theorem

(e : α ≃ β) : e.conj.symm = e.symm.conj

Full source

@[simp] theorem conj_symm (e : α ≃ β) : e.conj.symm = e.symm.conj := rfl

Inverse of Conjugation Equivalence Equals Conjugation of Inverse

Informal description

For any equivalence $e : \alpha \simeq \beta$, the inverse of the conjugation equivalence $e.\text{conj} : (\alpha \to \alpha) \simeq (\beta \to \beta)$ is equal to the conjugation equivalence of the inverse $e^{-1} : \beta \simeq \alpha$. That is, $(e.\text{conj})^{-1} = e^{-1}.\text{conj}$.

Equiv.conj_trans theorem

(e₁ : α ≃ β) (e₂ : β ≃ γ) : (e₁.trans e₂).conj = e₁.conj.trans e₂.conj

Full source

@[simp] theorem conj_trans (e₁ : α ≃ β) (e₂ : β ≃ γ) :
    (e₁.trans e₂).conj = e₁.conj.trans e₂.conj := rfl

Compatibility of Conjugation with Composition of Equivalences

Informal description

Given equivalences $e₁ : \alpha \simeq \beta$ and $e₂ : \beta \simeq \gamma$, the conjugation of their composition $(e₁ \circ e₂).\text{conj}$ is equal to the composition of their conjugations $e₁.\text{conj} \circ e₂.\text{conj}$ as equivalences between function spaces $(\alpha \to \alpha) \simeq (\gamma \to \gamma)$.

Equiv.conj_comp theorem

(e : α ≃ β) (f₁ f₂ : α → α) : e.conj (f₁ ∘ f₂) = e.conj f₁ ∘ e.conj f₂

Full source

theorem conj_comp (e : α ≃ β) (f₁ f₂ : α → α) : e.conj (f₁ ∘ f₂) = e.conj f₁ ∘ e.conj f₂ := by
  apply arrowCongr_comp

Conjugation Preserves Function Composition under Equivalence

Informal description

For any equivalence $e : \alpha \simeq \beta$ and any functions $f_1, f_2 : \alpha \to \alpha$, the conjugation of the composition $f_1 \circ f_2$ under $e$ equals the composition of the conjugations of $f_1$ and $f_2$ under $e$. That is, \[ e_{\text{conj}}(f_1 \circ f_2) = e_{\text{conj}}(f_1) \circ e_{\text{conj}}(f_2), \] where $e_{\text{conj}}$ denotes the conjugation operation by $e$.

Equiv.comp_symm_eq theorem

{α β γ} (e : α ≃ β) (f : β → γ) (g : α → γ) : g ∘ e.symm = f ↔ g = f ∘ e

Full source

theorem comp_symm_eq {α β γ} (e : α ≃ β) (f : β → γ) (g : α → γ) : g ∘ e.symmg ∘ e.symm = f ↔ g = f ∘ e :=
  (e.arrowCongr (Equiv.refl γ)).eq_symm_apply.symm

Composition with Inverse Equivalence Condition

Informal description

For any types $\alpha$, $\beta$, and $\gamma$, given an equivalence $e : \alpha \simeq \beta$ and functions $f : \beta \to \gamma$ and $g : \alpha \to \gamma$, the composition $g \circ e^{-1}$ equals $f$ if and only if $g$ equals $f \circ e$.

Equiv.symm_comp_eq theorem

{α β γ} (e : α ≃ β) (f : γ → α) (g : γ → β) : e.symm ∘ g = f ↔ g = e ∘ f

Full source

theorem symm_comp_eq {α β γ} (e : α ≃ β) (f : γ → α) (g : γ → β) : e.symm ∘ ge.symm ∘ g = f ↔ g = e ∘ f :=
  ((Equiv.refl γ).arrowCongr e).symm_apply_eq

Composition with Inverse Equivalence Characterization: $e^{-1} \circ g = f \leftrightarrow g = e \circ f$

Informal description

For any types $\alpha$, $\beta$, and $\gamma$, given an equivalence $e : \alpha \simeq \beta$ and functions $f : \gamma \to \alpha$ and $g : \gamma \to \beta$, the composition $e^{-1} \circ g$ equals $f$ if and only if $g$ equals $e \circ f$.

Equiv.trans_eq_refl_iff_eq_symm theorem

{f : α ≃ β} {g : β ≃ α} : f.trans g = Equiv.refl α ↔ f = g.symm

Full source

theorem trans_eq_refl_iff_eq_symm {f : α ≃ β} {g : β ≃ α} :
    f.trans g = Equiv.refl α ↔ f = g.symm := by
  rw [← Equiv.coe_inj, coe_trans, coe_refl, ← eq_symm_comp, comp_id, Equiv.coe_inj]

Composition with Identity Condition for Equivalences: $f \circ g = \text{id}_\alpha \leftrightarrow f = g^{-1}$

Informal description

For any equivalences $f : \alpha \simeq \beta$ and $g : \beta \simeq \alpha$, the composition $f \circ g$ is equal to the identity equivalence on $\alpha$ if and only if $f$ is equal to the inverse of $g$.

Equiv.trans_eq_refl_iff_symm_eq theorem

{f : α ≃ β} {g : β ≃ α} : f.trans g = Equiv.refl α ↔ f.symm = g

Full source

theorem trans_eq_refl_iff_symm_eq {f : α ≃ β} {g : β ≃ α} :
    f.trans g = Equiv.refl α ↔ f.symm = g := by
  rw [trans_eq_refl_iff_eq_symm]
  exact ⟨fun h ↦ h ▸ rfl, fun h ↦ h ▸ rfl⟩

Composition Yields Identity iff Inverse Equals Second Equivalence

Informal description

For any equivalences $f : \alpha \simeq \beta$ and $g : \beta \simeq \alpha$, the composition $f \circ g$ is equal to the identity equivalence on $\alpha$ if and only if the inverse of $f$ is equal to $g$.

Equiv.symm_eq_iff_trans_eq_refl theorem

{f : α ≃ β} {g : β ≃ α} : f.symm = g ↔ f.trans g = Equiv.refl α

Full source

theorem symm_eq_iff_trans_eq_refl {f : α ≃ β} {g : β ≃ α} :
    f.symm = g ↔ f.trans g = Equiv.refl α :=
  trans_eq_refl_iff_symm_eq.symm

Inverse Equals Second Equivalence iff Composition Yields Identity

Informal description

For any equivalences $f : \alpha \simeq \beta$ and $g : \beta \simeq \alpha$, the inverse of $f$ is equal to $g$ if and only if the composition $f \circ g$ is equal to the identity equivalence on $\alpha$.

Equiv.punitEquivPUnit definition

: PUnit.{v} ≃ PUnit.{w}

Full source

/-- `PUnit` sorts in any two universes are equivalent. -/
def punitEquivPUnit : PUnitPUnit.{v}PUnit.{v} ≃ PUnit.{w} :=
  ⟨fun _ => .unit, fun _ => .unit, fun ⟨⟩ => rfl, fun ⟨⟩ => rfl⟩

Equivalence between singleton types in different universes

Informal description

The equivalence between the singleton types `PUnit.{v}` and `PUnit.{w}` in different universes, defined by mapping the unique element of each type to the unique element of the other type. Specifically, the forward map sends the element `unit` of `PUnit.{v}` to the element `unit` of `PUnit.{w}`, and the inverse map does the same in reverse. Both compositions of these maps yield the identity function on their respective types.

Equiv.propEquivBool definition

: Prop ≃ Bool

Full source

/-- `Prop` is noncomputably equivalent to `Bool`. -/
noncomputable def propEquivBool : Prop ≃ Bool where
  toFun p := @decide p (Classical.propDecidable _)
  invFun b := b
  left_inv p := by simp [@Bool.decide_iff p (Classical.propDecidable _)]
  right_inv b := by cases b <;> simp

Equivalence between propositions and booleans

Informal description

The equivalence `Prop ≃ Bool` is a bijection between the type of propositions `Prop` and the type of booleans `Bool`. The forward map assigns to each proposition `p` its truth value `decide p` (using classical decidability), and the inverse map assigns to each boolean `b` the proposition `b` itself (where `true` corresponds to `True` and `false` corresponds to `False`). This equivalence satisfies that composing the maps in either direction yields the identity.

Equiv.arrowPUnitEquivPUnit definition

(α : Sort*) : (α → PUnit.{v}) ≃ PUnit.{w}

Full source

/-- The sort of maps to `PUnit.{v}` is equivalent to `PUnit.{w}`. -/
def arrowPUnitEquivPUnit (α : Sort*) : (α → PUnit.{v}) ≃ PUnit.{w} :=
  ⟨fun _ => .unit, fun _ _ => .unit, fun _ => rfl, fun _ => rfl⟩

Equivalence between functions to a singleton and a singleton

Informal description

For any type $\alpha$, the type of functions from $\alpha$ to the singleton type $\text{PUnit}.\{v\}$ is equivalent to the singleton type $\text{PUnit}.\{w\}$ in a possibly different universe. The equivalence maps any function $f : \alpha \to \text{PUnit}.\{v\}$ to the unique element $\text{unit}$ of $\text{PUnit}.\{w\}$, and conversely, maps $\text{unit}$ to the constant function sending every element of $\alpha$ to $\text{unit}$.

Equiv.piUnique definition

[Unique α] (β : α → Sort*) : (∀ i, β i) ≃ β default

Full source

/-- The equivalence `(∀ i, β i) ≃ β ⋆` when the domain of `β` only contains `⋆` -/
@[simps -fullyApplied]
def piUnique [Unique α] (β : α → Sort*) : (∀ i, β i) ≃ β default where
  toFun f := f default
  invFun := uniqueElim
  left_inv f := by ext i; cases Unique.eq_default i; rfl
  right_inv _ := rfl

Equivalence between dependent functions on a unique type and their value at the default element

Informal description

Given a type `α` with a unique element (i.e., `[Unique α]`) and a type family `β : α → Sort*`, the equivalence `(∀ i, β i) ≃ β default` maps a dependent function `f` to its value at the default element of `α`, and conversely, any element of `β default` can be uniquely extended to a dependent function on `α` via the unique elimination principle. This establishes a bijection between dependent functions on `α` and their values at the default element.

Equiv.funUnique definition

(α β) [Unique.{u} α] : (α → β) ≃ β

Full source

/-- If `α` has a unique term, then the type of function `α → β` is equivalent to `β`. -/
@[simps! -fullyApplied apply symm_apply]
def funUnique (α β) [Unique.{u} α] : (α → β) ≃ β := piUnique _

Equivalence between functions from a singleton type and their codomain

Informal description

Given a type $\alpha$ with a unique element (i.e., $\alpha$ is a singleton type) and any type $\beta$, the type of functions from $\alpha$ to $\beta$ is equivalent to $\beta$ itself. The equivalence maps a function $f : \alpha \to \beta$ to its value at the unique element of $\alpha$, and conversely, any element $b : \beta$ can be viewed as the constant function sending the unique element of $\alpha$ to $b$.

Equiv.punitArrowEquiv definition

(α : Sort*) : (PUnit.{u} → α) ≃ α

Full source

/-- The sort of maps from `PUnit` is equivalent to the codomain. -/
def punitArrowEquiv (α : Sort*) : (PUnit.{u} → α) ≃ α := funUnique PUnitPUnit.{u} α

Equivalence between functions from the unit type and their codomain

Informal description

For any type $\alpha$, the type of functions from the unit type $\text{PUnit}$ to $\alpha$ is equivalent to $\alpha$ itself. The equivalence maps a function $f : \text{PUnit} \to \alpha$ to its value at the unique element of $\text{PUnit}$, and conversely, any element $a : \alpha$ can be viewed as the constant function sending the unique element of $\text{PUnit}$ to $a$.

Equiv.trueArrowEquiv definition

(α : Sort*) : (True → α) ≃ α

Full source

/-- The sort of maps from `True` is equivalent to the codomain. -/
def trueArrowEquiv (α : Sort*) : (True → α) ≃ α := funUnique _ _

Equivalence between functions from `True` and their codomain

Informal description

The type of functions from the singleton type `True` to any type `α` is equivalent to `α` itself. The equivalence maps a function `f : True → α` to its value at the unique element `true`, and conversely, any element `a : α` can be viewed as the constant function sending `true` to `a`.

Equiv.arrowPUnitOfIsEmpty definition

(α β : Sort*) [IsEmpty α] : (α → β) ≃ PUnit.{u}

Full source

/-- The sort of maps from a type that `IsEmpty` is equivalent to `PUnit`. -/
def arrowPUnitOfIsEmpty (α β : Sort*) [IsEmpty α] : (α → β) ≃ PUnit.{u} where
  toFun _ := PUnit.unit
  invFun _ := isEmptyElim
  left_inv _ := funext isEmptyElim
  right_inv _ := rfl

Equivalence between functions from an empty type and the unit type

Informal description

For any types $\alpha$ and $\beta$ where $\alpha$ is empty, the type of functions from $\alpha$ to $\beta$ is equivalent to the unit type $\text{PUnit}$. The equivalence maps any function to the unique element of $\text{PUnit}$ and maps the unique element back to the empty function (using the fact that $\alpha$ is empty).

Equiv.emptyArrowEquivPUnit definition

(α : Sort*) : (Empty → α) ≃ PUnit.{u}

Full source

/-- The sort of maps from `Empty` is equivalent to `PUnit`. -/
def emptyArrowEquivPUnit (α : Sort*) : (Empty → α) ≃ PUnit.{u} := arrowPUnitOfIsEmpty _ _

Equivalence between functions from Empty and the unit type

Informal description

The type of functions from the empty type `Empty` to any type `α` is equivalent to the unit type `PUnit`. The equivalence maps any function from `Empty` to the unique element of `PUnit` and maps the unique element back to the empty function (which exists uniquely since `Empty` has no elements).

Equiv.pemptyArrowEquivPUnit definition

(α : Sort*) : (PEmpty → α) ≃ PUnit.{u}

Full source

/-- The sort of maps from `PEmpty` is equivalent to `PUnit`. -/
def pemptyArrowEquivPUnit (α : Sort*) : (PEmpty → α) ≃ PUnit.{u} := arrowPUnitOfIsEmpty _ _

Equivalence between functions from the empty type and the unit type

Informal description

The type of functions from the empty type `PEmpty` to any type `α` is equivalent to the unit type `PUnit`. The equivalence maps any function from `PEmpty` to the unique element of `PUnit` and maps the unique element back to the empty function (which exists uniquely since `PEmpty` has no elements).

Equiv.falseArrowEquivPUnit definition

(α : Sort*) : (False → α) ≃ PUnit.{u}

Full source

/-- The sort of maps from `False` is equivalent to `PUnit`. -/
def falseArrowEquivPUnit (α : Sort*) : (False → α) ≃ PUnit.{u} := arrowPUnitOfIsEmpty _ _

Equivalence between functions from `False` and the unit type

Informal description

The type of functions from the empty type `False` to any type `α` is equivalent to the unit type `PUnit`. The equivalence maps any function from `False` to the unique element of `PUnit` and maps the unique element back to the empty function (which exists uniquely since `False` has no elements).

Equiv.psigmaEquivSigma definition

{α} (β : α → Type*) : (Σ' i, β i) ≃ Σ i, β i

Full source

/-- A `PSigma`-type is equivalent to the corresponding `Sigma`-type. -/
@[simps apply symm_apply]
def psigmaEquivSigma {α} (β : α → Type*) : (Σ' i, β i) ≃ Σ i, β i where
  toFun a := ⟨a.1, a.2⟩
  invFun a := ⟨a.1, a.2⟩
  left_inv _ := rfl
  right_inv _ := rfl

Equivalence between `PSigma` and `Sigma` types

Informal description

For any type family $\beta : \alpha \to \text{Type}^*$, there is a natural equivalence between the dependent pair type $\Sigma' i, \beta i$ (a `PSigma` type) and the corresponding $\Sigma$ type $\Sigma i, \beta i$. The equivalence maps each pair $\langle i, x \rangle$ in the `PSigma` type to the same pair $\langle i, x \rangle$ in the $\Sigma$ type, and vice versa, with both directions being identity maps.

Equiv.psigmaEquivSigmaPLift definition

{α} (β : α → Sort*) : (Σ' i, β i) ≃ Σ i : PLift α, PLift (β i.down)

Full source

/-- A `PSigma`-type is equivalent to the corresponding `Sigma`-type. -/
@[simps apply symm_apply]
def psigmaEquivSigmaPLift {α} (β : α → Sort*) : (Σ' i, β i) ≃ Σ i : PLift α, PLift (β i.down) where
  toFun a := ⟨PLift.up a.1, PLift.up a.2⟩
  invFun a := ⟨a.1.down, a.2.down⟩
  left_inv _ := rfl
  right_inv _ := rfl

Equivalence between `PSigma` and lifted `Sigma` types

Informal description

For any type family $\beta : \alpha \to \text{Sort}^*$, there is a natural equivalence between the dependent pair type $\Sigma' i, \beta i$ (a `PSigma` type) and the $\Sigma$ type $\Sigma i : \text{PLift } \alpha, \text{PLift } (\beta i.\text{down})$. The equivalence maps each pair $\langle i, x \rangle$ in the `PSigma` type to $\langle \text{PLift.up } i, \text{PLift.up } x \rangle$ in the $\Sigma$ type, and vice versa via $\langle a.1.\text{down}, a.2.\text{down} \rangle$, with both compositions being identity maps.

Equiv.psigmaCongrRight definition

{β₁ β₂ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) : (Σ' a, β₁ a) ≃ Σ' a, β₂ a

Full source

/-- A family of equivalences `Π a, β₁ a ≃ β₂ a` generates an equivalence between `Σ' a, β₁ a` and
`Σ' a, β₂ a`. -/
@[simps apply]
def psigmaCongrRight {β₁ β₂ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) : (Σ' a, β₁ a) ≃ Σ' a, β₂ a where
  toFun a := ⟨a.1, F a.1 a.2⟩
  invFun a := ⟨a.1, (F a.1).symm a.2⟩
  left_inv | ⟨a, b⟩ => congr_arg (PSigma.mk a) <| symm_apply_apply (F a) b
  right_inv | ⟨a, b⟩ => congr_arg (PSigma.mk a) <| apply_symm_apply (F a) b

Equivalence of dependent pair types under componentwise equivalences

Informal description

Given a family of equivalences $F : \forall a, \beta_1 a \simeq \beta_2 a$ between dependent types $\beta_1$ and $\beta_2$ indexed by $\alpha$, there is an equivalence between the dependent pair types $\Sigma' a, \beta_1 a$ and $\Sigma' a, \beta_2 a$. The forward map sends a pair $\langle a, b \rangle$ to $\langle a, F a \, b \rangle$, and the inverse map sends $\langle a, b \rangle$ to $\langle a, (F a)^{-1} \, b \rangle$, with both compositions being identity maps.

Equiv.psigmaCongrRight_trans theorem

 {α} {β₁ β₂ β₃ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) (G : ∀ a, β₂ a ≃ β₃ a) :
  (psigmaCongrRight F).trans (psigmaCongrRight G) = psigmaCongrRight fun a => (F a).trans (G a)

Full source

theorem psigmaCongrRight_trans {α} {β₁ β₂ β₃ : α → Sort*}
    (F : ∀ a, β₁ a ≃ β₂ a) (G : ∀ a, β₂ a ≃ β₃ a) :
    (psigmaCongrRight F).trans (psigmaCongrRight G) =
      psigmaCongrRight fun a => (F a).trans (G a) := rfl

Composition of componentwise equivalences for dependent pair types

Informal description

For any type $\alpha$ and families of types $\beta_1, \beta_2, \beta_3 : \alpha \to \text{Sort}^*$, given families of equivalences $F : \forall a, \beta_1 a \simeq \beta_2 a$ and $G : \forall a, \beta_2 a \simeq \beta_3 a$, the composition of the equivalences $\text{psigmaCongrRight } F$ and $\text{psigmaCongrRight } G$ is equal to the equivalence $\text{psigmaCongrRight } (\lambda a, (F a).trans (G a))$.

Equiv.psigmaCongrRight_symm theorem

 {α} {β₁ β₂ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) : (psigmaCongrRight F).symm = psigmaCongrRight fun a => (F a).symm

Full source

theorem psigmaCongrRight_symm {α} {β₁ β₂ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) :
    (psigmaCongrRight F).symm = psigmaCongrRight fun a => (F a).symm := rfl

Inverse of Dependent Pair Equivalence via Componentwise Inverses

Informal description

Given a family of equivalences $F : \forall a, \beta_1 a \simeq \beta_2 a$ between dependent types $\beta_1$ and $\beta_2$ indexed by $\alpha$, the inverse of the equivalence `psigmaCongrRight F` is equal to the equivalence `psigmaCongrRight` applied to the family of inverses $\lambda a, (F a)^{-1}$.

Equiv.psigmaCongrRight_refl theorem

{α} {β : α → Sort*} : (psigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl (Σ' a, β a)

Full source

@[simp]
theorem psigmaCongrRight_refl {α} {β : α → Sort*} :
    (psigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl (Σ' a, β a) := rfl

Identity Equivalence for Dependent Pair Types via Componentwise Identity

Informal description

For any type $\alpha$ and a family of types $\beta : \alpha \to \text{Sort}^*$, the equivalence $\text{psigmaCongrRight}$ applied to the family of identity equivalences $\lambda a, \text{refl } (\beta a)$ is equal to the identity equivalence on the dependent pair type $\Sigma' a, \beta a$.

Equiv.sigmaCongrRight definition

{α} {β₁ β₂ : α → Type*} (F : ∀ a, β₁ a ≃ β₂ a) : (Σ a, β₁ a) ≃ Σ a, β₂ a

Full source

/-- A family of equivalences `Π a, β₁ a ≃ β₂ a` generates an equivalence between `Σ a, β₁ a` and
`Σ a, β₂ a`. -/
@[simps apply]
def sigmaCongrRight {α} {β₁ β₂ : α → Type*} (F : ∀ a, β₁ a ≃ β₂ a) : (Σ a, β₁ a) ≃ Σ a, β₂ a where
  toFun a := ⟨a.1, F a.1 a.2⟩
  invFun a := ⟨a.1, (F a.1).symm a.2⟩
  left_inv | ⟨a, b⟩ => congr_arg (Sigma.mk a) <| symm_apply_apply (F a) b
  right_inv | ⟨a, b⟩ => congr_arg (Sigma.mk a) <| apply_symm_apply (F a) b

Equivalence of Dependent Sums via Component-wise Equivalence

Informal description

Given a family of equivalences $F : \forall a, \beta_1 a \simeq \beta_2 a$ indexed by elements of type $\alpha$, the function `Equiv.sigmaCongrRight` constructs an equivalence between the dependent sums $\Sigma a, \beta_1 a$ and $\Sigma a, \beta_2 a$. The forward map applies $F a$ to the second component of each pair $\langle a, b \rangle$, and the inverse map applies the inverse of $F a$ to the second component of each pair $\langle a, b \rangle$.

Equiv.sigmaCongrRight_trans theorem

 {α} {β₁ β₂ β₃ : α → Type*} (F : ∀ a, β₁ a ≃ β₂ a) (G : ∀ a, β₂ a ≃ β₃ a) :
  (sigmaCongrRight F).trans (sigmaCongrRight G) = sigmaCongrRight fun a => (F a).trans (G a)

Full source

theorem sigmaCongrRight_trans {α} {β₁ β₂ β₃ : α → Type*}
    (F : ∀ a, β₁ a ≃ β₂ a) (G : ∀ a, β₂ a ≃ β₃ a) :
    (sigmaCongrRight F).trans (sigmaCongrRight G) =
      sigmaCongrRight fun a => (F a).trans (G a) := rfl

Composition of Component-wise Equivalences on Dependent Sums

Informal description

Given a type $\alpha$ and families of types $\beta_1, \beta_2, \beta_3 : \alpha \to \text{Type}^*$, along with equivalences $F : \forall a, \beta_1 a \simeq \beta_2 a$ and $G : \forall a, \beta_2 a \simeq \beta_3 a$, the composition of the equivalences $\text{sigmaCongrRight}\, F$ and $\text{sigmaCongrRight}\, G$ is equal to the equivalence obtained by component-wise composition, i.e., \[ (\text{sigmaCongrRight}\, F) \circ (\text{sigmaCongrRight}\, G) = \text{sigmaCongrRight}\, (\lambda a, F a \circ G a). \]

Equiv.sigmaCongrRight_symm theorem

 {α} {β₁ β₂ : α → Type*} (F : ∀ a, β₁ a ≃ β₂ a) : (sigmaCongrRight F).symm = sigmaCongrRight fun a => (F a).symm

Full source

theorem sigmaCongrRight_symm {α} {β₁ β₂ : α → Type*} (F : ∀ a, β₁ a ≃ β₂ a) :
    (sigmaCongrRight F).symm = sigmaCongrRight fun a => (F a).symm := rfl

Inverse of Component-wise Equivalence on Dependent Sums

Informal description

Given a family of equivalences $F : \forall a, \beta_1 a \simeq \beta_2 a$ indexed by elements of type $\alpha$, the inverse of the equivalence $\Sigma a, \beta_1 a \simeq \Sigma a, \beta_2 a$ constructed by `sigmaCongrRight F` is equal to the equivalence constructed by applying the inverse of each $F a$ component-wise, i.e., $$(\text{sigmaCongrRight } F)^{-1} = \text{sigmaCongrRight } (\lambda a, (F a)^{-1}).$$

Equiv.sigmaCongrRight_refl theorem

{α} {β : α → Type*} : (sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl (Σ a, β a)

Full source

@[simp]
theorem sigmaCongrRight_refl {α} {β : α → Type*} :
    (sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl (Σ a, β a) := rfl

Component-wise Identity Equivalence Preserves Dependent Sum Identity

Informal description

For any type $\alpha$ and family of types $\beta : \alpha \to \text{Type}^*$, the equivalence obtained by applying the identity equivalence $\text{refl}(\beta a)$ component-wise to each $\beta a$ is equal to the identity equivalence on the dependent sum type $\Sigma a, \beta a$.

Equiv.psigmaEquivSubtype definition

{α : Type v} (P : α → Prop) : (Σ' i, P i) ≃ Subtype P

Full source

/-- A `PSigma` with `Prop` fibers is equivalent to the subtype. -/
def psigmaEquivSubtype {α : Type v} (P : α → Prop) : (Σ' i, P i) ≃ Subtype P where
  toFun x := ⟨x.1, x.2⟩
  invFun x := ⟨x.1, x.2⟩
  left_inv _ := rfl
  right_inv _ := rfl

Equivalence between dependent pairs with Prop fibers and subtypes

Informal description

For any type $\alpha$ and predicate $P : \alpha \to \text{Prop}$, there is an equivalence between the dependent pair type $\Sigma' i, P i$ (a `PSigma` type with `Prop` fibers) and the subtype $\{x : \alpha \mid P x\}$. The equivalence maps $(i, p)$ to $\langle i, p \rangle$ and vice versa.

Equiv.sigmaPLiftEquivSubtype definition

{α : Type v} (P : α → Prop) : (Σ i, PLift (P i)) ≃ Subtype P

Full source

/-- A `Sigma` with `PLift` fibers is equivalent to the subtype. -/
def sigmaPLiftEquivSubtype {α : Type v} (P : α → Prop) : (Σ i, PLift (P i)) ≃ Subtype P :=
  ((psigmaEquivSigma _).symm.trans
    (psigmaCongrRight fun _ => Equiv.plift)).trans (psigmaEquivSubtype P)

Equivalence between $\Sigma$-type with $\text{PLift}$ fibers and subtype

Informal description

For any type $\alpha$ and predicate $P : \alpha \to \text{Prop}$, there is an equivalence between the dependent pair type $\Sigma i, \text{PLift}(P i)$ (where $\text{PLift}$ lifts a Prop to a Type) and the subtype $\{x : \alpha \mid P x\}$. The equivalence is constructed by composing three natural equivalences: first taking the symmetric equivalence between $\Sigma'$ and $\Sigma$ types, then applying componentwise lifting via $\text{PLift}$, and finally using the equivalence between $\Sigma'$ with Prop fibers and the subtype.

Equiv.sigmaULiftPLiftEquivSubtype definition

{α : Type v} (P : α → Prop) : (Σ i, ULift (PLift (P i))) ≃ Subtype P

Full source

/-- A `Sigma` with `fun i ↦ ULift (PLift (P i))` fibers is equivalent to `{ x // P x }`.
Variant of `sigmaPLiftEquivSubtype`.
-/
def sigmaULiftPLiftEquivSubtype {α : Type v} (P : α → Prop) :
    (Σ i, ULift (PLift (P i))) ≃ Subtype P :=
  (sigmaCongrRight fun _ => Equiv.ulift).trans (sigmaPLiftEquivSubtype P)

Equivalence between $\Sigma$-type with $\text{ULift} \circ \text{PLift}$ fibers and subtype

Informal description

For any type $\alpha$ and predicate $P : \alpha \to \text{Prop}$, there is an equivalence between the dependent pair type $\Sigma i, \text{ULift}(\text{PLift}(P i))$ (where $\text{PLift}$ lifts a $\text{Prop}$ to a $\text{Type}$ and $\text{ULift}$ lifts a $\text{Type}$ to a higher universe) and the subtype $\{x : \alpha \mid P x\}$. The equivalence is constructed by first applying the equivalence $\text{ULift}$ componentwise to the $\text{PLift}$ fibers, then using the equivalence between $\Sigma$-type with $\text{PLift}$ fibers and the subtype.

Equiv.Perm.sigmaCongrRight abbrev

{α} {β : α → Sort _} (F : ∀ a, Perm (β a)) : Perm (Σ a, β a)

Full source

/-- A family of permutations `Π a, Perm (β a)` generates a permutation `Perm (Σ a, β₁ a)`. -/
abbrev sigmaCongrRight {α} {β : α → Sort _} (F : ∀ a, Perm (β a)) : Perm (Σ a, β a) :=
  Equiv.sigmaCongrRight F

Permutation of Dependent Sum via Component-wise Permutations

Informal description

Given a family of permutations $F : \forall a, \text{Perm}(\beta a)$ indexed by elements of type $\alpha$, the function $\text{sigmaCongrRight}$ constructs a permutation on the dependent sum type $\Sigma a, \beta a$. The permutation acts by applying $F a$ to the second component of each pair $\langle a, b \rangle$ in the dependent sum.

Equiv.Perm.sigmaCongrRight_trans theorem

 {α} {β : α → Sort _} (F : ∀ a, Perm (β a)) (G : ∀ a, Perm (β a)) :
  (sigmaCongrRight F).trans (sigmaCongrRight G) = sigmaCongrRight fun a => (F a).trans (G a)

Full source

@[simp] theorem sigmaCongrRight_trans {α} {β : α → Sort _}
    (F : ∀ a, Perm (β a)) (G : ∀ a, Perm (β a)) :
    (sigmaCongrRight F).trans (sigmaCongrRight G) = sigmaCongrRight fun a => (F a).trans (G a) :=
  Equiv.sigmaCongrRight_trans F G

Composition of Component-wise Permutations on Dependent Sums

Informal description

For any type $\alpha$ and a family of types $\beta : \alpha \to \text{Sort}$, given two families of permutations $F, G : \forall a, \text{Perm}(\beta a)$, the composition of the permutations $\text{sigmaCongrRight}\, F$ and $\text{sigmaCongrRight}\, G$ on the dependent sum type $\Sigma a, \beta a$ is equal to the permutation obtained by component-wise composition, i.e., \[ (\text{sigmaCongrRight}\, F) \circ (\text{sigmaCongrRight}\, G) = \text{sigmaCongrRight}\, (\lambda a, F a \circ G a). \]

Equiv.Perm.sigmaCongrRight_symm theorem

{α} {β : α → Sort _} (F : ∀ a, Perm (β a)) : (sigmaCongrRight F).symm = sigmaCongrRight fun a => (F a).symm

Full source

@[simp] theorem sigmaCongrRight_symm {α} {β : α → Sort _} (F : ∀ a, Perm (β a)) :
    (sigmaCongrRight F).symm = sigmaCongrRight fun a => (F a).symm :=
  Equiv.sigmaCongrRight_symm F

Inverse of Component-wise Permutation on Dependent Sums

Informal description

Given a family of permutations $F : \forall a, \text{Perm}(\beta a)$ indexed by elements of type $\alpha$, the inverse of the permutation $\text{sigmaCongrRight } F$ on the dependent sum type $\Sigma a, \beta a$ is equal to the permutation obtained by applying the inverse of each $F a$ component-wise, i.e., $$(\text{sigmaCongrRight } F)^{-1} = \text{sigmaCongrRight } (\lambda a, (F a)^{-1}).$$

Equiv.Perm.sigmaCongrRight_refl theorem

{α} {β : α → Sort _} : (sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl (Σ a, β a)

Full source

@[simp] theorem sigmaCongrRight_refl {α} {β : α → Sort _} :
    (sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl (Σ a, β a) :=
  Equiv.sigmaCongrRight_refl

Identity Permutation Preserves Dependent Sum Identity

Informal description

For any type $\alpha$ and family of types $\beta : \alpha \to \text{Sort}\_$, the permutation obtained by applying the identity permutation component-wise to each $\beta(a)$ is equal to the identity permutation on the dependent sum type $\Sigma a, \beta a$. In other words, $\text{sigmaCongrRight}(\lambda a, \text{refl}(\beta a)) = \text{refl}(\Sigma a, \beta a)$.

Equiv.sigmaCongrLeft definition

{α₁ α₂ : Type*} {β : α₂ → Sort _} (e : α₁ ≃ α₂) : (Σ a : α₁, β (e a)) ≃ Σ a : α₂, β a

Full source

/-- An equivalence `f : α₁ ≃ α₂` generates an equivalence between `Σ a, β (f a)` and `Σ a, β a`. -/
@[simps apply] def sigmaCongrLeft {α₁ α₂ : Type*} {β : α₂ → Sort _} (e : α₁ ≃ α₂) :
    (Σ a : α₁, β (e a)) ≃ Σ a : α₂, β a where
  toFun a := ⟨e a.1, a.2⟩
  invFun a := ⟨e.symm a.1, (e.right_inv' a.1).symm ▸ a.2⟩
  left_inv := fun ⟨a, b⟩ => by simp
  right_inv := fun ⟨a, b⟩ => by simp

Equivalence of Dependent Sums via Left Composition

Informal description

Given an equivalence $e : \alpha_1 \simeq \alpha_2$ between types $\alpha_1$ and $\alpha_2$, and a family of types $\beta : \alpha_2 \to \text{Sort} \_$, the function `Equiv.sigmaCongrLeft` constructs an equivalence between the dependent sum types $\Sigma (a : \alpha_1), \beta(e(a))$ and $\Sigma (a : \alpha_2), \beta(a)$. The forward map sends a pair $\langle a, b \rangle$ to $\langle e(a), b \rangle$, and the inverse map sends $\langle a, b \rangle$ to $\langle e^{-1}(a), b' \rangle$, where $b'$ is obtained by transporting $b$ along the proof that $e$ is a right inverse of $e^{-1}$.

Equiv.sigmaCongrLeft' definition

{α₁ α₂} {β : α₁ → Sort _} (f : α₁ ≃ α₂) : (Σ a : α₁, β a) ≃ Σ a : α₂, β (f.symm a)

Full source

/-- Transporting a sigma type through an equivalence of the base -/
def sigmaCongrLeft' {α₁ α₂} {β : α₁ → Sort _} (f : α₁ ≃ α₂) :
    (Σ a : α₁, β a) ≃ Σ a : α₂, β (f.symm a) := (sigmaCongrLeft f.symm).symm

Equivalence of dependent sums via left composition (variant)

Informal description

Given an equivalence $f : \alpha_1 \simeq \alpha_2$ between types $\alpha_1$ and $\alpha_2$, and a family of types $\beta : \alpha_1 \to \text{Sort} \_$, the function `Equiv.sigmaCongrLeft'` constructs an equivalence between the dependent sum types $\Sigma (a : \alpha_1), \beta(a)$ and $\Sigma (a : \alpha_2), \beta(f^{-1}(a))$. The forward map sends a pair $\langle a, b \rangle$ to $\langle f(a), b \rangle$, and the inverse map sends $\langle a, b \rangle$ to $\langle f^{-1}(a), b' \rangle$, where $b'$ is obtained by transporting $b$ along the proof that $f$ is a left inverse of $f^{-1}$.

Equiv.sigmaCongr definition

 {α₁ α₂} {β₁ : α₁ → Sort _} {β₂ : α₂ → Sort _} (f : α₁ ≃ α₂) (F : ∀ a, β₁ a ≃ β₂ (f a)) : Sigma β₁ ≃ Sigma β₂

Full source

/-- Transporting a sigma type through an equivalence of the base and a family of equivalences
of matching fibers -/
def sigmaCongr {α₁ α₂} {β₁ : α₁ → Sort _} {β₂ : α₂ → Sort _} (f : α₁ ≃ α₂)
    (F : ∀ a, β₁ a ≃ β₂ (f a)) : SigmaSigma β₁ ≃ Sigma β₂ :=
  (sigmaCongrRight F).trans (sigmaCongrLeft f)

Equivalence of dependent sums via base change and fiber-wise equivalence

Informal description

Given an equivalence $f : \alpha_1 \simeq \alpha_2$ between types $\alpha_1$ and $\alpha_2$, and a family of equivalences $F : \forall a, \beta_1 a \simeq \beta_2 (f a)$ where $\beta_1 : \alpha_1 \to \text{Sort} \_$ and $\beta_2 : \alpha_2 \to \text{Sort} \_$, the function `Equiv.sigmaCongr` constructs an equivalence between the dependent sums $\Sigma (a : \alpha_1), \beta_1 a$ and $\Sigma (a : \alpha_2), \beta_2 a$. This is achieved by first applying the component-wise equivalence $F$ (via `sigmaCongrRight`) and then applying the base change equivalence $f$ (via `sigmaCongrLeft`).

Equiv.sigmaEquivProd definition

(α β : Type*) : (Σ _ : α, β) ≃ α × β

Full source

/-- `Sigma` type with a constant fiber is equivalent to the product. -/
@[simps (config := { attrs := [`mfld_simps] }) apply symm_apply]
def sigmaEquivProd (α β : Type*) : (Σ _ : α, β) ≃ α × β :=
  ⟨fun a => ⟨a.1, a.2⟩, fun a => ⟨a.1, a.2⟩, fun ⟨_, _⟩ => rfl, fun ⟨_, _⟩ => rfl⟩

Equivalence between dependent pair type with constant fiber and product type

Informal description

The equivalence between the dependent pair type $\Sigma\ (a : \alpha), \beta$ (where $\beta$ is a constant type) and the product type $\alpha \times \beta$. The bijection maps $(a, b)$ to $(a, b)$ in both directions, with the inverse functions being the identity maps.

Equiv.sigmaEquivProdOfEquiv definition

{α β} {β₁ : α → Sort _} (F : ∀ a, β₁ a ≃ β) : Sigma β₁ ≃ α × β

Full source

/-- If each fiber of a `Sigma` type is equivalent to a fixed type, then the sigma type
is equivalent to the product. -/
def sigmaEquivProdOfEquiv {α β} {β₁ : α → Sort _} (F : ∀ a, β₁ a ≃ β) : SigmaSigma β₁ ≃ α × β :=
  (sigmaCongrRight F).trans (sigmaEquivProd α β)

Equivalence between dependent sum with component-wise equivalent fibers and product type

Informal description

Given a type $\alpha$, a type $\beta$, and a family of types $\beta_1 : \alpha \to \text{Sort}$ such that each $\beta_1 a$ is equivalent to $\beta$ via $F a : \beta_1 a \simeq \beta$, the dependent sum $\Sigma (a : \alpha), \beta_1 a$ is equivalent to the product type $\alpha \times \beta$. This equivalence is constructed by first applying the component-wise equivalence $F$ to the second component of each pair in the dependent sum, and then using the equivalence between $\Sigma (a : \alpha), \beta$ and $\alpha \times \beta$.

Equiv.sigmaAssoc definition

 {α : Type*} {β : α → Type*} (γ : ∀ a : α, β a → Type*) : (Σ ab : Σ a : α, β a, γ ab.1 ab.2) ≃ Σ a : α, Σ b : β a, γ a b

Full source

/-- The dependent product of types is associative up to an equivalence. -/
def sigmaAssoc {α : Type*} {β : α → Type*} (γ : ∀ a : α, β a → Type*) :
    (Σ ab : Σ a : α, β a, γ ab.1 ab.2) ≃ Σ a : α, Σ b : β a, γ a b where
  toFun x := ⟨x.1.1, ⟨x.1.2, x.2⟩⟩
  invFun x := ⟨⟨x.1, x.2.1⟩, x.2.2⟩
  left_inv _ := rfl
  right_inv _ := rfl

Associativity of Sigma Types

Informal description

For any type $\alpha$ and dependent types $\beta : \alpha \to \text{Type}$ and $\gamma : \forall a : \alpha, \beta a \to \text{Type}$, there is a natural equivalence between the nested sigma types $(\Sigma (ab : \Sigma (a : \alpha), \beta a), \gamma ab.1 ab.2)$ and $(\Sigma (a : \alpha), \Sigma (b : \beta a), \gamma a b)$. The bijection is given explicitly by: - The forward map sends $\langle\langle a, b\rangle, c\rangle$ to $\langle a, \langle b, c\rangle\rangle$ - The inverse map sends $\langle a, \langle b, c\rangle\rangle$ to $\langle\langle a, b\rangle, c\rangle$

Equiv.pSigmaAssoc definition

 {α : Sort*} {β : α → Sort*} (γ : ∀ a : α, β a → Sort*) :
  (Σ' ab : Σ' a : α, β a, γ ab.1 ab.2) ≃ Σ' a : α, Σ' b : β a, γ a b

Full source

/-- The dependent product of sorts is associative up to an equivalence. -/
def pSigmaAssoc {α : Sort*} {β : α → Sort*} (γ : ∀ a : α, β a → Sort*) :
    (Σ' ab : Σ' a : α, β a, γ ab.1 ab.2) ≃ Σ' a : α, Σ' b : β a, γ a b where
  toFun x := ⟨x.1.1, ⟨x.1.2, x.2⟩⟩
  invFun x := ⟨⟨x.1, x.2.1⟩, x.2.2⟩
  left_inv _ := rfl
  right_inv _ := rfl

Associativity of dependent products (sigma types)

Informal description

The equivalence states that for any types $\alpha$ (in any universe) and dependent types $\beta : \alpha \to \text{Sort}*$ and $\gamma : \forall a : \alpha, \beta a \to \text{Sort}*$, the dependent product $\Sigma' (ab : \Sigma' (a : \alpha), \beta a), \gamma ab.1 ab.2$ is equivalent to $\Sigma' (a : \alpha), \Sigma' (b : \beta a), \gamma a b$. Here $\Sigma'$ denotes the dependent product (sigma type) in the given universe. This shows that nested dependent products can be reassociated, with the equivalence given explicitly by: - The forward map takes $\langle\langle a, b\rangle, c\rangle$ to $\langle a, \langle b, c\rangle\rangle$ - The inverse map takes $\langle a, \langle b, c\rangle\rangle$ to $\langle\langle a, b\rangle, c\rangle$

Equiv.forall_congr_right theorem

: (∀ a, q (e a)) ↔ ∀ b, q b

Full source

protected lemma forall_congr_right : (∀ a, q (e a)) ↔ ∀ b, q b :=
  ⟨fun h a ↦ by simpa using h (e.symm a), fun h _ ↦ h _⟩

Universal Quantification Transfer via Equivalence: $(\forall a, q(e(a))) \leftrightarrow (\forall b, q(b))$

Informal description

For any equivalence $e : \alpha \simeq \beta$ and any predicate $q : \beta \to \text{Prop}$, the universal quantification over $\alpha$ of $q$ composed with $e$ is equivalent to the universal quantification over $\beta$ of $q$, i.e., \[ (\forall a : \alpha, q(e(a))) \leftrightarrow (\forall b : \beta, q(b)). \]

Equiv.forall_congr_left theorem

: (∀ a, p a) ↔ ∀ b, p (e.symm b)

Full source

protected lemma forall_congr_left : (∀ a, p a) ↔ ∀ b, p (e.symm b) :=
  e.symm.forall_congr_right.symm

Universal Quantification Transfer via Equivalence Inverse: $(\forall a, p(a)) \leftrightarrow (\forall b, p(e^{-1}(b)))$

Informal description

For any equivalence $e : \alpha \simeq \beta$ and any predicate $p : \alpha \to \text{Prop}$, the universal quantification over $\alpha$ of $p$ is equivalent to the universal quantification over $\beta$ of $p$ composed with the inverse of $e$, i.e., \[ (\forall a : \alpha, p(a)) \leftrightarrow (\forall b : \beta, p(e^{-1}(b))). \]

Equiv.forall_congr theorem

(h : ∀ a, p a ↔ q (e a)) : (∀ a, p a) ↔ ∀ b, q b

Full source

protected lemma forall_congr (h : ∀ a, p a ↔ q (e a)) : (∀ a, p a) ↔ ∀ b, q b :=
  e.forall_congr_left.trans (by simp [h])

Universal Quantification Transfer via Equivalence: $(\forall a, p(a)) \leftrightarrow (\forall b, q(b))$ under $p(a) \leftrightarrow q(e(a))$

Informal description

For any equivalence $e : \alpha \simeq \beta$ and predicates $p : \alpha \to \text{Prop}$ and $q : \beta \to \text{Prop}$ such that for all $a \in \alpha$, $p(a) \leftrightarrow q(e(a))$, the universal quantification over $\alpha$ of $p$ is equivalent to the universal quantification over $\beta$ of $q$, i.e., \[ (\forall a \in \alpha, p(a)) \leftrightarrow (\forall b \in \beta, q(b)). \]

Equiv.forall_congr' theorem

(h : ∀ b, p (e.symm b) ↔ q b) : (∀ a, p a) ↔ ∀ b, q b

Full source

protected lemma forall_congr' (h : ∀ b, p (e.symm b) ↔ q b) : (∀ a, p a) ↔ ∀ b, q b :=
  e.forall_congr_left.trans (by simp [h])

Universal Quantification Transfer via Equivalence Inverse with Predicate Condition: $(\forall a, p(a)) \leftrightarrow (\forall b, q(b))$ under $p(e^{-1}(b)) \leftrightarrow q(b)$

Informal description

For any equivalence $e : \alpha \simeq \beta$ and predicates $p : \alpha \to \text{Prop}$ and $q : \beta \to \text{Prop}$, if for every $b \in \beta$ we have $p(e^{-1}(b)) \leftrightarrow q(b)$, then the universal quantification over $\alpha$ of $p$ is equivalent to the universal quantification over $\beta$ of $q$, i.e., \[ (\forall a \in \alpha, p(a)) \leftrightarrow (\forall b \in \beta, q(b)). \]

Equiv.exists_congr_right theorem

: (∃ a, q (e a)) ↔ ∃ b, q b

Full source

protected lemma exists_congr_right : (∃ a, q (e a)) ↔ ∃ b, q b :=
  ⟨fun ⟨_, h⟩ ↦ ⟨_, h⟩, fun ⟨a, h⟩ ↦ ⟨e.symm a, by simpa using h⟩⟩

Existence Preservation under Equivalence: $(\exists a, q(e(a))) \leftrightarrow (\exists b, q(b))$

Informal description

For any equivalence $e : \alpha \simeq \beta$ and any predicate $q$ on $\beta$, there exists an element $a \in \alpha$ such that $q(e(a))$ holds if and only if there exists an element $b \in \beta$ such that $q(b)$ holds.

Equiv.exists_congr_left theorem

: (∃ a, p a) ↔ ∃ b, p (e.symm b)

Full source

protected lemma exists_congr_left : (∃ a, p a) ↔ ∃ b, p (e.symm b) :=
  e.symm.exists_congr_right.symm

Existence Preservation under Equivalence Inverse: $(\exists a, p(a)) \leftrightarrow (\exists b, p(e^{-1}(b)))$

Informal description

For any equivalence $e : \alpha \simeq \beta$ and any predicate $p$ on $\alpha$, there exists an element $a \in \alpha$ such that $p(a)$ holds if and only if there exists an element $b \in \beta$ such that $p(e^{-1}(b))$ holds, where $e^{-1}$ is the inverse of $e$.

Equiv.exists_congr theorem

(h : ∀ a, p a ↔ q (e a)) : (∃ a, p a) ↔ ∃ b, q b

Full source

protected lemma exists_congr (h : ∀ a, p a ↔ q (e a)) : (∃ a, p a) ↔ ∃ b, q b :=
  e.exists_congr_left.trans <| by simp [h]

Existence Preservation under Equivalence with Predicate Condition: $(\exists a, p(a)) \leftrightarrow (\exists b, q(b))$

Informal description

For any equivalence $e : \alpha \simeq \beta$ and predicates $p$ on $\alpha$ and $q$ on $\beta$, if for every $a \in \alpha$ we have $p(a) \leftrightarrow q(e(a))$, then there exists $a \in \alpha$ such that $p(a)$ holds if and only if there exists $b \in \beta$ such that $q(b)$ holds.

Equiv.exists_congr' theorem

(h : ∀ b, p (e.symm b) ↔ q b) : (∃ a, p a) ↔ ∃ b, q b

Full source

protected lemma exists_congr' (h : ∀ b, p (e.symm b) ↔ q b) : (∃ a, p a) ↔ ∃ b, q b :=
  e.exists_congr_left.trans <| by simp [h]

Existence Preservation under Equivalence with Predicate Condition: $(\exists a, p(a)) \leftrightarrow (\exists b, q(b))$

Informal description

For any equivalence $e : \alpha \simeq \beta$ and predicates $p$ on $\alpha$ and $q$ on $\beta$, if for every $b \in \beta$ we have $p(e^{-1}(b)) \leftrightarrow q(b)$, then there exists $a \in \alpha$ such that $p(a)$ holds if and only if there exists $b \in \beta$ such that $q(b)$ holds.

Equiv.existsUnique_congr_right theorem

: (∃! a, q (e a)) ↔ ∃! b, q b

Full source

protected lemma existsUnique_congr_right : (∃! a, q (e a)) ↔ ∃! b, q b :=
  e.exists_congr <| by simpa using fun _ _ ↦ e.forall_congr (by simp)

Uniqueness Preservation under Equivalence: $(\exists! a, q(e(a))) \leftrightarrow (\exists! b, q(b))$

Informal description

For any equivalence $e : \alpha \simeq \beta$ and predicate $q$ on $\beta$, there exists a unique $a \in \alpha$ such that $q(e(a))$ holds if and only if there exists a unique $b \in \beta$ such that $q(b)$ holds.

Equiv.existsUnique_congr_left theorem

: (∃! a, p a) ↔ ∃! b, p (e.symm b)

Full source

protected lemma existsUnique_congr_left : (∃! a, p a) ↔ ∃! b, p (e.symm b) :=
  e.symm.existsUnique_congr_right.symm

Uniqueness Preservation under Equivalence (Left Version): $(\exists! a, p(a)) \leftrightarrow (\exists! b, p(e^{-1}(b)))$

Informal description

For any equivalence $e : \alpha \simeq \beta$ and predicate $p$ on $\alpha$, there exists a unique $a \in \alpha$ such that $p(a)$ holds if and only if there exists a unique $b \in \beta$ such that $p(e^{-1}(b))$ holds.

Equiv.existsUnique_congr theorem

(h : ∀ a, p a ↔ q (e a)) : (∃! a, p a) ↔ ∃! b, q b

Full source

protected lemma existsUnique_congr (h : ∀ a, p a ↔ q (e a)) : (∃! a, p a) ↔ ∃! b, q b :=
  e.existsUnique_congr_left.trans <| by simp [h]

Uniqueness Preservation under Equivalence: $(\exists! a, p(a)) \leftrightarrow (\exists! b, q(b))$ when $p(a) \leftrightarrow q(e(a))$

Informal description

For any equivalence $e : \alpha \simeq \beta$ and predicates $p$ on $\alpha$ and $q$ on $\beta$ such that for all $a \in \alpha$, $p(a) \leftrightarrow q(e(a))$, the following are equivalent: 1. There exists a unique $a \in \alpha$ such that $p(a)$ holds. 2. There exists a unique $b \in \beta$ such that $q(b)$ holds.

Equiv.existsUnique_congr' theorem

(h : ∀ b, p (e.symm b) ↔ q b) : (∃! a, p a) ↔ ∃! b, q b

Full source

protected lemma existsUnique_congr' (h : ∀ b, p (e.symm b) ↔ q b) : (∃! a, p a) ↔ ∃! b, q b :=
  e.existsUnique_congr_left.trans <| by simp [h]

Uniqueness Preservation under Equivalence via Inverse: $(\exists! a, p(a)) \leftrightarrow (\exists! b, q(b))$ under $p(e^{-1}(b)) \leftrightarrow q(b)$

Informal description

For any equivalence $e : \alpha \simeq \beta$ and predicates $p$ on $\alpha$ and $q$ on $\beta$ such that for all $b \in \beta$, $p(e^{-1}(b)) \leftrightarrow q(b)$, there exists a unique $a \in \alpha$ satisfying $p(a)$ if and only if there exists a unique $b \in \beta$ satisfying $q(b)$.

Equiv.forall₂_congr theorem

 {α₁ α₂ β₁ β₂ : Sort*} {p : α₁ → β₁ → Prop} {q : α₂ → β₂ → Prop} (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂)
  (h : ∀ {x y}, p x y ↔ q (eα x) (eβ y)) : (∀ x y, p x y) ↔ ∀ x y, q x y

Full source

protected theorem forall₂_congr {α₁ α₂ β₁ β₂ : Sort*} {p : α₁ → β₁ → Prop} {q : α₂ → β₂ → Prop}
    (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂) (h : ∀ {x y}, p x y ↔ q (eα x) (eβ y)) :
    (∀ x y, p x y) ↔ ∀ x y, q x y :=
  eα.forall_congr fun _ ↦ eβ.forall_congr <| @h _

Universal Quantification Transfer for Binary Predicates via Equivalences: $(\forall x y, p(x, y)) \leftrightarrow (\forall x y, q(x, y))$ under $p(x, y) \leftrightarrow q(e_\alpha(x), e_\beta(y))$

Informal description

For any types $\alpha_1, \alpha_2, \beta_1, \beta_2$, predicates $p : \alpha_1 \to \beta_1 \to \text{Prop}$ and $q : \alpha_2 \to \beta_2 \to \text{Prop}$, and equivalences $e_\alpha : \alpha_1 \simeq \alpha_2$ and $e_\beta : \beta_1 \simeq \beta_2$ such that for all $x \in \alpha_1$ and $y \in \beta_1$, $p(x, y) \leftrightarrow q(e_\alpha(x), e_\beta(y))$, the universal quantification over $\alpha_1$ and $\beta_1$ of $p$ is equivalent to the universal quantification over $\alpha_2$ and $\beta_2$ of $q$, i.e., \[ (\forall x \in \alpha_1, \forall y \in \beta_1, p(x, y)) \leftrightarrow (\forall x \in \alpha_2, \forall y \in \beta_2, q(x, y)). \]

Equiv.forall₂_congr' theorem

 {α₁ α₂ β₁ β₂ : Sort*} {p : α₁ → β₁ → Prop} {q : α₂ → β₂ → Prop} (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂)
  (h : ∀ {x y}, p (eα.symm x) (eβ.symm y) ↔ q x y) : (∀ x y, p x y) ↔ ∀ x y, q x y

Full source

protected theorem forall₂_congr' {α₁ α₂ β₁ β₂ : Sort*} {p : α₁ → β₁ → Prop} {q : α₂ → β₂ → Prop}
    (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂) (h : ∀ {x y}, p (eα.symm x) (eβ.symm y) ↔ q x y) :
    (∀ x y, p x y) ↔ ∀ x y, q x y := (Equiv.forall₂_congr eα.symm eβ.symm h.symm).symm

Universal Quantification Transfer for Binary Predicates via Equivalence Inverses: $(\forall x y, p(x, y)) \leftrightarrow (\forall x y, q(x, y))$ under $p(e_\alpha^{-1}(x), e_\beta^{-1}(y)) \leftrightarrow q(x, y)$

Informal description

For any types $\alpha_1, \alpha_2, \beta_1, \beta_2$, predicates $p : \alpha_1 \to \beta_1 \to \text{Prop}$ and $q : \alpha_2 \to \beta_2 \to \text{Prop}$, and equivalences $e_\alpha : \alpha_1 \simeq \alpha_2$ and $e_\beta : \beta_1 \simeq \beta_2$ such that for all $x \in \alpha_2$ and $y \in \beta_2$, $p(e_\alpha^{-1}(x), e_\beta^{-1}(y)) \leftrightarrow q(x, y)$, the universal quantification over $\alpha_1$ and $\beta_1$ of $p$ is equivalent to the universal quantification over $\alpha_2$ and $\beta_2$ of $q$, i.e., \[ (\forall x \in \alpha_1, \forall y \in \beta_1, p(x, y)) \leftrightarrow (\forall x \in \alpha_2, \forall y \in \beta_2, q(x, y)). \]

Equiv.forall₃_congr theorem

 {α₁ α₂ β₁ β₂ γ₁ γ₂ : Sort*} {p : α₁ → β₁ → γ₁ → Prop} {q : α₂ → β₂ → γ₂ → Prop} (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂)
  (eγ : γ₁ ≃ γ₂) (h : ∀ {x y z}, p x y z ↔ q (eα x) (eβ y) (eγ z)) : (∀ x y z, p x y z) ↔ ∀ x y z, q x y z

Full source

protected theorem forall₃_congr
    {α₁ α₂ β₁ β₂ γ₁ γ₂ : Sort*} {p : α₁ → β₁ → γ₁ → Prop} {q : α₂ → β₂ → γ₂ → Prop}
    (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂) (eγ : γ₁ ≃ γ₂) (h : ∀ {x y z}, p x y z ↔ q (eα x) (eβ y) (eγ z)) :
    (∀ x y z, p x y z) ↔ ∀ x y z, q x y z :=
  Equiv.forall₂_congr _ _ <| Equiv.forall_congr _ <| @h _ _

Universal Quantification Transfer for Ternary Predicates via Equivalences: $(\forall x y z, p(x, y, z)) \leftrightarrow (\forall x y z, q(x, y, z))$ under $p(x, y, z) \leftrightarrow q(e_\alpha(x), e_\beta(y), e_\gamma(z))$

Informal description

For any types $\alpha_1, \alpha_2, \beta_1, \beta_2, \gamma_1, \gamma_2$, predicates $p : \alpha_1 \to \beta_1 \to \gamma_1 \to \text{Prop}$ and $q : \alpha_2 \to \beta_2 \to \gamma_2 \to \text{Prop}$, and equivalences $e_\alpha : \alpha_1 \simeq \alpha_2$, $e_\beta : \beta_1 \simeq \beta_2$, $e_\gamma : \gamma_1 \simeq \gamma_2$ such that for all $x \in \alpha_1$, $y \in \beta_1$, $z \in \gamma_1$, we have $p(x, y, z) \leftrightarrow q(e_\alpha(x), e_\beta(y), e_\gamma(z))$, then the universal quantification over $\alpha_1, \beta_1, \gamma_1$ of $p$ is equivalent to the universal quantification over $\alpha_2, \beta_2, \gamma_2$ of $q$, i.e., \[ (\forall x \in \alpha_1, \forall y \in \beta_1, \forall z \in \gamma_1, p(x, y, z)) \leftrightarrow (\forall x \in \alpha_2, \forall y \in \beta_2, \forall z \in \gamma_2, q(x, y, z)). \]

Equiv.forall₃_congr' theorem

 {α₁ α₂ β₁ β₂ γ₁ γ₂ : Sort*} {p : α₁ → β₁ → γ₁ → Prop} {q : α₂ → β₂ → γ₂ → Prop} (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂)
  (eγ : γ₁ ≃ γ₂) (h : ∀ {x y z}, p (eα.symm x) (eβ.symm y) (eγ.symm z) ↔ q x y z) :
  (∀ x y z, p x y z) ↔ ∀ x y z, q x y z

Full source

protected theorem forall₃_congr'
    {α₁ α₂ β₁ β₂ γ₁ γ₂ : Sort*} {p : α₁ → β₁ → γ₁ → Prop} {q : α₂ → β₂ → γ₂ → Prop}
    (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂) (eγ : γ₁ ≃ γ₂)
    (h : ∀ {x y z}, p (eα.symm x) (eβ.symm y) (eγ.symm z) ↔ q x y z) :
    (∀ x y z, p x y z) ↔ ∀ x y z, q x y z :=
  (Equiv.forall₃_congr eα.symm eβ.symm eγ.symm h.symm).symm

Universal Quantification Transfer for Ternary Predicates via Equivalence Inverses: $(\forall x y z, p(x, y, z)) \leftrightarrow (\forall x y z, q(x, y, z))$ under $p(e_\alpha^{-1}(x), e_\beta^{-1}(y), e_\gamma^{-1}(z)) \leftrightarrow q(x, y, z)$

Informal description

For any types $\alpha_1, \alpha_2, \beta_1, \beta_2, \gamma_1, \gamma_2$, predicates $p : \alpha_1 \to \beta_1 \to \gamma_1 \to \text{Prop}$ and $q : \alpha_2 \to \beta_2 \to \gamma_2 \to \text{Prop}$, and equivalences $e_\alpha : \alpha_1 \simeq \alpha_2$, $e_\beta : \beta_1 \simeq \beta_2$, $e_\gamma : \gamma_1 \simeq \gamma_2$ such that for all $x \in \alpha_2$, $y \in \beta_2$, $z \in \gamma_2$, we have $p(e_\alpha^{-1}(x), e_\beta^{-1}(y), e_\gamma^{-1}(z)) \leftrightarrow q(x, y, z)$, then the universal quantification over $\alpha_1, \beta_1, \gamma_1$ of $p$ is equivalent to the universal quantification over $\alpha_2, \beta_2, \gamma_2$ of $q$, i.e., \[ (\forall x \in \alpha_1, \forall y \in \beta_1, \forall z \in \gamma_1, p(x, y, z)) \leftrightarrow (\forall x \in \alpha_2, \forall y \in \beta_2, \forall z \in \gamma_2, q(x, y, z)). \]

Equiv.ofBijective definition

(f : α → β) (hf : Bijective f) : α ≃ β

Full source

/-- If `f` is a bijective function, then its domain is equivalent to its codomain. -/
@[simps apply]
noncomputable def ofBijective (f : α → β) (hf : Bijective f) : α ≃ β where
  toFun := f
  invFun := surjInv hf.surjective
  left_inv := leftInverse_surjInv hf
  right_inv := rightInverse_surjInv _

Equivalence from a bijective function

Informal description

Given a bijective function $ f : \alpha \to \beta $, the equivalence $ \alpha \simeq \beta $ is constructed with $ f $ as the forward map and its surjective inverse $ \text{surjInv}_f $ as the backward map, satisfying $ \text{surjInv}_f \circ f = \text{id}_\alpha $ and $ f \circ \text{surjInv}_f = \text{id}_\beta $.

Equiv.ofBijective_apply_symm_apply theorem

(f : α → β) (hf : Bijective f) (x : β) : f ((ofBijective f hf).symm x) = x

Full source

lemma ofBijective_apply_symm_apply (f : α → β) (hf : Bijective f) (x : β) :
    f ((ofBijective f hf).symm x) = x :=
  (ofBijective f hf).apply_symm_apply x

Recovery of Element via Bijection: $f(f^{-1}(x)) = x$

Informal description

For any bijective function $f : \alpha \to \beta$ and any element $x \in \beta$, applying $f$ to the inverse image of $x$ under the equivalence constructed from $f$ recovers $x$, i.e., $f(f^{-1}(x)) = x$, where $f^{-1}$ is the inverse function of $f$.

Equiv.ofBijective_symm_apply_apply theorem

(f : α → β) (hf : Bijective f) (x : α) : (ofBijective f hf).symm (f x) = x

Full source

@[simp]
lemma ofBijective_symm_apply_apply (f : α → β) (hf : Bijective f) (x : α) :
    (ofBijective f hf).symm (f x) = x :=
  (ofBijective f hf).symm_apply_apply x

Inverse of Bijective Equivalence Recovers Input

Informal description

For any bijective function $f \colon \alpha \to \beta$ and any element $x \in \alpha$, the inverse of the equivalence $\alpha \simeq \beta$ constructed from $f$ satisfies $(f^{-1} \circ f)(x) = x$, where $f^{-1}$ is the inverse function of $f$.

Quot.congr definition

 {ra : α → α → Prop} {rb : β → β → Prop} (e : α ≃ β) (eq : ∀ a₁ a₂, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) : Quot ra ≃ Quot rb

Full source

/-- An equivalence `e : α ≃ β` generates an equivalence between quotient spaces,
if `ra a₁ a₂ ↔ rb (e a₁) (e a₂)`. -/
protected def congr {ra : α → α → Prop} {rb : β → β → Prop} (e : α ≃ β)
    (eq : ∀ a₁ a₂, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) : QuotQuot ra ≃ Quot rb where
  toFun := Quot.map e fun a₁ a₂ => (eq a₁ a₂).1
  invFun := Quot.map e.symm fun b₁ b₂ h =>
    (eq (e.symm b₁) (e.symm b₂)).2
      ((e.apply_symm_apply b₁).symm ▸ (e.apply_symm_apply b₂).symm ▸ h)
  left_inv := by rintro ⟨a⟩; simp only [Quot.map, Equiv.symm_apply_apply]
  right_inv := by rintro ⟨a⟩; simp only [Quot.map, Equiv.apply_symm_apply]

Equivalence of Quotients Induced by Type Equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and two relations $r_a$ on $\alpha$ and $r_b$ on $\beta$ such that $r_a(a_1, a_2) \leftrightarrow r_b(e(a_1), e(a_2))$ for all $a_1, a_2 \in \alpha$, there is an induced equivalence $\text{Quot } r_a \simeq \text{Quot } r_b$ between the quotient spaces. The forward map is defined by lifting $e$ to the quotient via $\text{Quot.map}$, and the inverse map is similarly defined using $e^{-1}$.

Quot.congr_mk theorem

 {ra : α → α → Prop} {rb : β → β → Prop} (e : α ≃ β) (eq : ∀ a₁ a₂ : α, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) (a : α) :
  Quot.congr e eq (Quot.mk ra a) = Quot.mk rb (e a)

Full source

@[simp] theorem congr_mk {ra : α → α → Prop} {rb : β → β → Prop} (e : α ≃ β)
    (eq : ∀ a₁ a₂ : α, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) (a : α) :
    Quot.congr e eq (Quot.mk ra a) = Quot.mk rb (e a) := rfl

Commutativity of Quotient Equivalence with Respect to Equivalence Class Construction

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and two relations $r_a$ on $\alpha$ and $r_b$ on $\beta$ such that $r_a(a_1, a_2) \leftrightarrow r_b(e(a_1), e(a_2))$ for all $a_1, a_2 \in \alpha$, the equivalence $\text{Quot.congr } e \text{ eq}$ maps the equivalence class of $a$ in $\text{Quot } r_a$ to the equivalence class of $e(a)$ in $\text{Quot } r_b$. In other words, the following diagram commutes: \[ \text{Quot.congr } e \text{ eq} (\text{Quot.mk } r_a \ a) = \text{Quot.mk } r_b \ (e \ a) \]

Quot.congrRight definition

{r r' : α → α → Prop} (eq : ∀ a₁ a₂, r a₁ a₂ ↔ r' a₁ a₂) : Quot r ≃ Quot r'

Full source

/-- Quotients are congruent on equivalences under equality of their relation.
An alternative is just to use rewriting with `eq`, but then computational proofs get stuck. -/
protected def congrRight {r r' : α → α → Prop} (eq : ∀ a₁ a₂, r a₁ a₂ ↔ r' a₁ a₂) :
    QuotQuot r ≃ Quot r' := Quot.congr (Equiv.refl α) eq

Equivalence of Quotients under Equivalent Relations

Informal description

Given two relations $r$ and $r'$ on a type $\alpha$ such that $r(a_1, a_2) \leftrightarrow r'(a_1, a_2)$ for all $a_1, a_2 \in \alpha$, there is an equivalence between the quotient spaces $\text{Quot } r$ and $\text{Quot } r'$. This equivalence is constructed using the identity equivalence on $\alpha$ and the given relation equivalence.

Quot.congrLeft definition

{r : α → α → Prop} (e : α ≃ β) : Quot r ≃ Quot fun b b' => r (e.symm b) (e.symm b')

Full source

/-- An equivalence `e : α ≃ β` generates an equivalence between the quotient space of `α`
by a relation `ra` and the quotient space of `β` by the image of this relation under `e`. -/
protected def congrLeft {r : α → α → Prop} (e : α ≃ β) :
    QuotQuot r ≃ Quot fun b b' => r (e.symm b) (e.symm b') :=
  Quot.congr e fun _ _ => by simp only [e.symm_apply_apply]

Equivalence of quotients induced by an equivalence on the base types

Informal description

Given an equivalence $e : \alpha \simeq \beta$ and a relation $r$ on $\alpha$, there is an induced equivalence between the quotient space $\text{Quot } r$ and the quotient space of $\beta$ by the relation $r'$ defined as $r'(b, b') = r(e^{-1}(b), e^{-1}(b'))$ for all $b, b' \in \beta$. This equivalence is constructed by lifting $e$ to the quotient spaces.

Quotient.congr definition

 {ra : Setoid α} {rb : Setoid β} (e : α ≃ β) (eq : ∀ a₁ a₂, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) : Quotient ra ≃ Quotient rb

Full source

/-- An equivalence `e : α ≃ β` generates an equivalence between quotient spaces,
if `ra a₁ a₂ ↔ rb (e a₁) (e a₂)`. -/
protected def congr {ra : Setoid α} {rb : Setoid β} (e : α ≃ β)
    (eq : ∀ a₁ a₂, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) :
    QuotientQuotient ra ≃ Quotient rb := Quot.congr e eq

Equivalence of Quotients Induced by Type Equivalence and Relation Compatibility

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and two setoids $ra$ on $\alpha$ and $rb$ on $\beta$ such that $ra(a_1, a_2) \leftrightarrow rb(e(a_1), e(a_2))$ for all $a_1, a_2 \in \alpha$, there is an induced equivalence $\text{Quotient } ra \simeq \text{Quotient } rb$ between the quotient spaces. The forward map is defined by lifting $e$ to the quotient via $\text{Quotient.map}$, and the inverse map is similarly defined using $e^{-1}$.

Quotient.congr_mk theorem

 {ra : Setoid α} {rb : Setoid β} (e : α ≃ β) (eq : ∀ a₁ a₂ : α, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) (a : α) :
  Quotient.congr e eq (Quotient.mk ra a) = Quotient.mk rb (e a)

Full source

@[simp] theorem congr_mk {ra : Setoid α} {rb : Setoid β} (e : α ≃ β)
    (eq : ∀ a₁ a₂ : α, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) (a : α) :
    Quotient.congr e eq (Quotient.mk ra a) = Quotient.mk rb (e a) := rfl

Compatibility of Quotient Construction with Type Equivalence on Elements

Informal description

Given an equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and two setoids $ra$ on $\alpha$ and $rb$ on $\beta$ such that for all $a_1, a_2 \in \alpha$, $ra(a_1, a_2) \leftrightarrow rb(e(a_1), e(a_2))$, then for any $a \in \alpha$, the equivalence $\text{Quotient.congr } e \text{ eq}$ maps the equivalence class of $a$ in $\text{Quotient } ra$ to the equivalence class of $e(a)$ in $\text{Quotient } rb$.

Quotient.congrRight definition

{r r' : Setoid α} (eq : ∀ a₁ a₂, r a₁ a₂ ↔ r' a₁ a₂) : Quotient r ≃ Quotient r'

Full source

/-- Quotients are congruent on equivalences under equality of their relation.
An alternative is just to use rewriting with `eq`, but then computational proofs get stuck. -/
protected def congrRight {r r' : Setoid α}
    (eq : ∀ a₁ a₂, r a₁ a₂ ↔ r' a₁ a₂) : QuotientQuotient r ≃ Quotient r' :=
  Quot.congrRight eq

Equivalence of Quotients under Equivalent Setoids

Informal description

Given two setoids $r$ and $r'$ on a type $\alpha$ such that $r(a_1, a_2) \leftrightarrow r'(a_1, a_2)$ for all $a_1, a_2 \in \alpha$, there is an equivalence between the quotient spaces $\text{Quotient } r$ and $\text{Quotient } r'$. This equivalence is constructed using the identity equivalence on $\alpha$ and the given relation equivalence.

finZeroEquiv definition

: Fin 0 ≃ Empty

Full source

/-- Equivalence between `Fin 0` and `Empty`. -/
def finZeroEquiv : FinFin 0 ≃ Empty := .equivEmpty _

Equivalence between Fin 0 and Empty

Informal description

The equivalence between the type `Fin 0` (the finite type with zero elements) and the empty type `Empty`, establishing that both types have no elements.

finZeroEquiv' definition

: Fin 0 ≃ PEmpty.{u}

Full source

/-- Equivalence between `Fin 0` and `PEmpty`. -/
def finZeroEquiv' : FinFin 0 ≃ PEmpty.{u} := .equivPEmpty _

Equivalence between `Fin 0` and the polymorphic empty type

Informal description

The equivalence between the type `Fin 0` (the canonical type with zero elements) and the polymorphic empty type `PEmpty.{u}`. This bijection exists because both types are empty.

finOneEquiv definition

: Fin 1 ≃ Unit

Full source

/-- Equivalence between `Fin 1` and `Unit`. -/
def finOneEquiv : FinFin 1 ≃ Unit := .equivPUnit _

Equivalence between `Fin 1` and `Unit`

Informal description

The equivalence between the type `Fin 1` (the canonical type with one element) and the unit type `Unit`. Specifically, the function maps the single element of `Fin 1` to the single element of `Unit`, and the inverse function maps the single element of `Unit` back to the single element of `Fin 1`.

finTwoEquiv definition

: Fin 2 ≃ Bool

Full source

/-- Equivalence between `Fin 2` and `Bool`. -/
def finTwoEquiv : FinFin 2 ≃ Bool where
  toFun i := i == 1
  invFun b := bif b then 1 else 0
  left_inv i :=
    match i with
    | 0 => by simp
    | 1 => by simp
  right_inv b := by cases b <;> simp

Equivalence between `Fin 2` and `Bool`

Informal description

The equivalence between the type `Fin 2` (the canonical type with two elements) and the Boolean type `Bool`. Specifically, the function maps `0` to `false` and `1` to `true`, with the inverse function mapping `false` back to `0` and `true` back to `1`.

Equiv.sumIsLeft definition

: { x : α ⊕ β // x.isLeft } ≃ α

Full source

/-- The left summand of `α ⊕ β` is equivalent to `α`. -/
@[simps]
def sumIsLeft : {x : α ⊕ β // x.isLeft}{x : α ⊕ β // x.isLeft} ≃ α where
  toFun x := x.1.getLeft x.2
  invFun a := ⟨.inl a, Sum.isLeft_inl⟩
  left_inv | ⟨.inl _a, _⟩ => rfl
  right_inv _a := rfl

Equivalence between left summand and original type

Informal description

The equivalence between the left summand of a sum type $\alpha \oplus \beta$ (i.e., elements of the form $\text{inl}(a)$ for $a \in \alpha$) and the type $\alpha$ itself. Specifically, it maps an element $\text{inl}(a)$ to $a$ and its inverse maps $a$ back to $\text{inl}(a)$.

Equiv.sumIsRight definition

: { x : α ⊕ β // x.isRight } ≃ β

Full source

/-- The right summand of `α ⊕ β` is equivalent to `β`. -/
@[simps]
def sumIsRight : {x : α ⊕ β // x.isRight}{x : α ⊕ β // x.isRight} ≃ β where
  toFun x := x.1.getRight x.2
  invFun b := ⟨.inr b, Sum.isRight_inr⟩
  left_inv | ⟨.inr _b, _⟩ => rfl
  right_inv _b := rfl

Equivalence between right summand and original type

Informal description

The equivalence between the right summand of a sum type $\alpha \oplus \beta$ (i.e., elements of the form $\text{inr}(b)$ for $b \in \beta$) and the type $\beta$ itself. Specifically, it maps an element $\text{inr}(b)$ to $b$ and its inverse maps $b$ back to $\text{inr}(b)$.

Tags