mathlib3 documentation

logic.equiv.embedding

Equivalences on embeddings #

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

This file shows some advanced equivalences on embeddings, useful for constructing larger embeddings from smaller ones.

source
def equiv.sum_embedding_equiv_prod_embedding_disjoint {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
(α ⊕ β ↪ γ) ≃ {f // disjoint (set.range ⇑(f.fst)) (set.range ⇑(f.snd))}

Embeddings from a sum type are equivalent to two separate embeddings with disjoint ranges.

Equations
source
def equiv.cod_restrict (α : Type u_1) {β : Type u_2} (bs : set β) :
{f // ∀ (a : α), ⇑f a ∈ bs} ≃ (α ↪ ↥bs)

Embeddings whose range lies within a set are equivalent to embeddings to that set. This is function.embedding.cod_restrict as an equiv.

Equations
source
def equiv.prod_embedding_disjoint_equiv_sigma_embedding_restricted {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
{f // disjoint (set.range ⇑(f.fst)) (set.range ⇑(f.snd))} ≃ Σ (f : α ↪ γ), β ↪ ↥(set.range ⇑f)ᶜ

Pairs of embeddings with disjoint ranges are equivalent to a dependent sum of embeddings, in which the second embedding cannot take values in the range of the first.

Equations
source
def equiv.sum_embedding_equiv_sigma_embedding_restricted {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
(α ⊕ β ↪ γ) ≃ Σ (f : α ↪ γ), β ↪ ↥(set.range ⇑f)ᶜ

A combination of the above results, allowing us to turn one embedding over a sum type into two dependent embeddings, the second of which avoids any members of the range of the first. This is helpful for constructing larger embeddings out of smaller ones.

Equations
source
def equiv.unique_embedding_equiv_result {α : Type u_1} {β : Type u_2} [unique α] :
(α ↪ β) ≃ β

Embeddings from a single-member type are equivalent to members of the target type.

Equations