def AlgebraInLean.Injective {α : Type u_1} {β : Type u_2} (f : α → β) : Prop

A map is injective (or "one-to-one") when f(x) = f(y) only when x = y

Equations

• AlgebraInLean.Injective f = ∀ (x y : α), f x = f y → x = y

def AlgebraInLean.Surjective {α : Type u_1} {β : Type u_2} (f : α → β) : Prop

A map is surjective (or "onto") when its image is the entire codomain

Equations

• AlgebraInLean.Surjective f = ∀ (y : β), ∃ (x : α), f x = y

def AlgebraInLean.Bijective {α : Type u_1} {β : Type u_2} (f : α → β) : Prop

A map is bijective if it is both injective and surjective

Equations

• AlgebraInLean.Bijective f = (AlgebraInLean.Injective f ∧ AlgebraInLean.Surjective f)

theorem AlgebraInLean.surjective_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} (h1 : AlgebraInLean.Surjective f) (h2 : AlgebraInLean.Surjective g) : AlgebraInLean.Surjective (g ∘ f)

The composition of surjective functions is surjective

theorem AlgebraInLean.injective_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} (h1 : AlgebraInLean.Injective f) (h2 : AlgebraInLean.Injective g) : AlgebraInLean.Injective (g ∘ f)

The composition of injective functions is injective

theorem AlgebraInLean.bijective_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} (h1 : AlgebraInLean.Bijective f) (h2 : AlgebraInLean.Bijective g) : AlgebraInLean.Bijective (g ∘ f)

The composition of bijective functions is bijective

theorem AlgebraInLean.inv_from_bijective {α : Type u_1} {β : Type u_2} {f : α → β} (h : AlgebraInLean.Bijective f) : ∃ (g : β → α), g ∘ f = id ∧ f ∘ g = id

Bijective functions are invertible

theorem AlgebraInLean.bijective_from_inv {α : Type u_1} {β : Type u_2} {f : α → β} (h : ∃ (g : β → α), g ∘ f = id ∧ f ∘ g = id) : AlgebraInLean.Bijective f

Invertible functions are bijective

theorem AlgebraInLean.bijective_iff_inv {α : Type u_1} {β : Type u_2} {f : α → β} : AlgebraInLean.Bijective f ↔ ∃ (g : β → α), g ∘ f = id ∧ f ∘ g = id

A function is bijective iff it is invertible

noncomputable def AlgebraInLean.inv_of_bijective {α : Type u_1} {β : Type u_2} {f : α → β} (h : AlgebraInLean.Bijective f) : β → α

The inverse of a bijective function

Equations

• AlgebraInLean.inv_of_bijective h = ⋯.choose

noncomputable def AlgebraInLean.inv_of_bijective_spec {α : Type u_1} {β : Type u_2} {f : α → β} (h : AlgebraInLean.Bijective f) : AlgebraInLean.inv_of_bijective h ∘ f = id ∧ f ∘ AlgebraInLean.inv_of_bijective h = id

Show that inv_of_bijective actually produces an inverse

Equations

• ⋯ = ⋯

theorem AlgebraInLean.bijective_inv {α : Type u_1} {β : Type u_2} {f : α → β} (h : AlgebraInLean.Bijective f) : AlgebraInLean.Bijective (AlgebraInLean.inv_of_bijective h)

The inverse of a bijective function is a bijection

theorem AlgebraInLean.Group.inv_bijective {G : Type u_4} [AlgebraInLean.Group G] : AlgebraInLean.Bijective AlgebraInLean.ι

The inverse map of a group is bijective