English
Embeddings from a sum type α ⊕ β into γ are equivalent to a pair of embeddings f : α ↪ γ and g : β ↪ γ with disjoint ranges.
Русский
Встраивания суммы α ⊕ β в γ эквивалентны парам вложений f : α ↪ γ и g : β ↪ γ с попарно непересекающимися образами.
LaTeX
$$$\\mathrm{Emb}(\\alpha \\oplus \\beta, \\gamma) \\cong \\{ (f,g) : (\\alpha \\hookrightarrow \\gamma) \\times (\\beta \\hookrightarrow \\gamma) \\mid \\mathrm{Disjoint}(\\mathrm{range}(f), \\mathrm{range}(g)) \\}$$$
Lean4
/-- Embeddings from a sum type are equivalent to two separate embeddings with disjoint ranges. -/
def sumEmbeddingEquivProdEmbeddingDisjoint {α β γ : Type*} :
(α ⊕ β ↪ γ) ≃ { f : (α ↪ γ) × (β ↪ γ) // Disjoint (Set.range f.1) (Set.range f.2) }
where
toFun
f :=
⟨(inl.trans f, inr.trans f), by
rw [Set.disjoint_left]
rintro _ ⟨a, h⟩ ⟨b, rfl⟩
simp only at h
have : Sum.inl a = Sum.inr b := f.injective h
simp only [reduceCtorEq] at this⟩
invFun := fun ⟨⟨f, g⟩, disj⟩ =>
⟨fun x =>
match x with
| Sum.inl a => f a
| Sum.inr b => g b,
by
rintro (a₁ | b₁) (a₂ | b₂) f_eq <;> simp only at f_eq
· rw [f.injective f_eq]
· exfalso
exact disj.le_bot ⟨⟨a₁, f_eq⟩, ⟨b₂, by simp⟩⟩
· exfalso
exact disj.le_bot ⟨⟨a₂, rfl⟩, ⟨b₁, f_eq⟩⟩
· rw [g.injective f_eq]⟩
left_inv
f := by
dsimp only
ext x
cases x <;> simp!
right_inv := fun ⟨⟨f, g⟩, _⟩ => by
simp only
rfl
