Equivalences on embeddings

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

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.

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.

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.

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

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 := ⋯ }