# Equivalences on embeddings #

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

source
def Equiv.sumEmbeddingEquivProdEmbeddingDisjoint {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
(α ⊕ β ↪ γ) ≃ { f : (α ↪ γ) × (β ↪ γ) // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }

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

Equations

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

Instances For

source
def Equiv.codRestrict (α : 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.codRestrict` as an equiv.

Equations

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

Instances For

source
def Equiv.prodEmbeddingDisjointEquivSigmaEmbeddingRestricted {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
{ f : (α ↪ γ) × (β ↪ γ) // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) } ≃ (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

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

Instances For

source
def Equiv.sumEmbeddingEquivSigmaEmbeddingRestricted {α : 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

- Equiv.sumEmbeddingEquivSigmaEmbeddingRestricted = Equiv.sumEmbeddingEquivProdEmbeddingDisjoint.trans Equiv.prodEmbeddingDisjointEquivSigmaEmbeddingRestricted

Instances For

source
def Equiv.uniqueEmbeddingEquivResult {α : Type u_1} {β : Type u_2} [Unique α] :
(α ↪ β) ≃ β

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

Equations

- Equiv.uniqueEmbeddingEquivResult = { toFun := fun (f : α ↪ β) => f default, invFun := fun (x : β) => { toFun := fun (x_1 : α) => x, inj' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }

Instances For