Functions

In Lean, a function is a relation that associates each element of one type (the domain) with a unique element of another type (the codomain). This concept is foundational in both mathematics and programming. In this chapter, we delve into how functions are represented and utilized in Lean. Key topics include:

• The definition and notation of functions in Lean.
• Function composition and application.
• Special types of functions, such as injective (one-to-one), surjective (onto), and bijective (one-to-one and onto) functions, and their significance in mathematical reasoning.

By the end of this chapter, we will have a basic foundation for defining, manipulating, and formally reasoning about functions in Lean.

Throughout this chapter, we assume that A, B, C and D are arbitrary types

Functions.lean

variable (A B C D : Type)

Given two types, A and B, the expression A → B denotes the type of all functions from A to B. The arrow → is written in Lean using \to. In this context, A is called the domain, and B the codomain. Each element f of A → B is a function. If a : A is an element of the domain, then f a represents its image under f and belongs to B. In Lean, function application does not require parentheses, making the syntax more natural and readable. Instead of writing f(a), as in many programming languages, Lean uses f a.

Functions.lean

-- The type of all functions from A to B
#check A → B

-- Declare functions f and g
variable (f g : A → B)

-- Declare an element a of type A
variable (a : A)

-- This is an element of type B
#check f a

Equality

The function type A → B comes with a natural notion of equality. Function extensionality, expressed by funext, states that if two functions with the same domain and codomain produce the same output for every input, then they are equal:
(∀ (a : A), f a = g a) → f = g. In many dependent type theory systems, function extensionality is an axiom, as it cannot be derived from the core logic alone. Conversely, if two functions are equal, then they yield the same result for every input:
f = g → ∀ (a : A), f a = g a. This follows from the congruence property of functions, implemented in Lean as congrFun. The following example illustrates both principles:

Functions.lean

theorem TEqApl : f = g ↔ ∀ (a : A), f a = g a := by
  apply Iff.intro
  -- f = g → ∀ (a : A), f a = g a
  intro h a
  exact congrFun h a
  -- (∀ (a : X), f a = g a) → f = g
  intro h
  exact funext h

Composition

If f : A → B and h : B → C are functions, their composition, written as h ∘ f, is a function of type A → C. In Lean, the composition operator ∘ is written using \comp or \circ.

Functions.lean

variable (h : B → C)
#check h ∘ f

Composition of functions is associative.

Associative.lean

theorem TCompAss {A B : Type} {f : A → B} {g : B → C} {h : C → D} : 
h ∘ (g ∘ f) = (h ∘ g) ∘ f := by
  funext a
  exact rfl

Identity function

For any type A, we can define the identity function id, which has type A → A. This function simply returns its input unchanged, meaning that for every a : A, we have id a = a.

If we #print id, Lean returns:

def id.{u} : {α : Sort u} → α → α := fun {α} a => a

This definition shows that id takes an implicit argument {α : Sort u}—a type in any universe—and an explicit argument a : α, returning a unchanged.

The identity function serves as a neutral element for function composition, meaning that composing any function with id, whether on the left or the right, leaves the function unchanged.

Neutral.lean

theorem TIdNeutral : (f ∘ id = f) ∧ (id ∘ f = f) := by
  apply And.intro
  -- f ∘ id = f
  funext a
  exact rfl
  -- id ∘ f = f
  funext a
  exact rfl

Observe that in the proof above, the equality f ∘ id = f uses id to denote the identity function on A, while in the equality id ∘ f = f, id refers to the identity function on B. This proof showcases Lean’s capabilities for type inference.

If we want to explicitly specify the domain of the identity function, we can disable the automatic insertion of implicit parameters by using the @ symbol before id. For example, @id A returns the identity function defined on the type A.

Id.lean

#check @id A

Injections

In this section, we introduce the concepts of injective function, monomorphism, and left inverse of a function, and we examine their relationships and key properties.

Injective

We say that a function f : A → B is injective or one-to-one if, for all pairs of elements a1, a2 : A, the equality f a1 = f a2 implies a1 = a2.

Injective.lean

def injective {A B : Type} (f : A → B) : Prop := ∀{a1 a2 : A}, 
(f a1 = f a2) → (a1 = a2)

Monomorphism

We say that a function f : A → B is a monomorphism if, for every other type C and every pair of functions g h : C → A, the equality f∘g = f∘h implies that g = h.

Monomorphism.lean

def monomorphism {A B : Type} (f : A → B) : Prop :=  ∀{C : Type}, 
∀{g h : C → A}, f∘g = f∘h → g = h

Left inverse

We say that a function f : A → B has a left inverse if there exists a function g : B → A such that g∘f = id.

Has Left Inverse.lean

def hasleftinv {A B : Type} (f : A → B) : Prop := ∃(g : B → A), g∘f = id 

An example: The identity

Every identity is injective, a monomorphism and has a left inverse (the identity itself).

Identity.lean

-- The identity is injective
theorem TIdInj : injective (@id A) := by
  -- rw [injective] -- rw to recover the definition
  intro a1 a2 h
  calc
    a1 = id a1 := by exact rfl
    _  = id a2 := by exact h
    _  = a2    := by exact rfl

-- The identity is a monomorphism
theorem TIdMon : monomorphism (@id A) := by
  -- rw [monomorphism] -- rw to recover the definition
  intro C g h h1
  calc
    g = id ∘ g := by exact rfl
    _ = id ∘ h := by exact h1
    _ = h      := by exact rfl

-- The identity has a left inverse
theorem TIdHasLeftInv : hasleftinv (@id A) := by
  -- rw [hasleftinv] -- rw to recover the definition
  apply Exists.intro id 
  exact rfl

Exercises

Exercises.lean

-- Negation of injective
theorem TNegInj {A B : Type} {f : A → B} : ¬ (injective f) ↔ ∃(a1 a2 : A), 
f a1 = f a2 ∧ a1 ≠ a2 := by sorry

-- The composition of injective functions is injective
theorem TCompInj {A B : Type}  {f : A → B} {g : B → C} (h1 : injective f) 
(h2 : injective g) : injective (g∘f) := by sorry
  
-- If the composition (g∘f) is injective, then f is injective
theorem TCompRInj {A B : Type} {f : A → B} {g : B → C} (h1 : injective (g∘f)) 
: (injective f) := by sorry

-- Injective and Monomorphism are equivalent concepts
theorem TCarMonoInj {A B : Type} {f : A → B} : injective f ↔ monomorphism f := by sorry

-- If a function has a left inverse then it is injective
theorem THasLeftInvtoInj {A B : Type} {f : A → B} : hasleftinv f → injective f := by sorry

Surjections

In this section, we introduce the concepts of surjective function, epimorphism, and right inverse of a function, and we examine their relationships and key properties.

Surjective

We say that a function f : A → B is surjective or onto if, for every element b : B, there exists an element a : A such that f a = b.

Surjective.lean

def surjective {A B : Type} (f : A → B) : Prop := ∀{b : B}, ∃(a : A), 
f a = b

Epimorphism

We say that a function f : A → B is an epimorphism if, for every other type C and every pair of functions g h : B → C, the equality g∘f = h∘f implies that g = h.

Epimorphism.lean

def epimorphism {A B : Type} (f : A → B) : Prop := ∀{C : Type}, 
∀{g h : B → C}, g∘f = h∘f → g = h

Right inverse

We say that a function f : A → B has a right inverse if there exists a function g : B → A such that f∘g = id.

Has Right Inverse.lean

def hasrightinv {A B : Type} (f : A → B) : Prop := ∃(g : B → A), f∘ g = id

An example: The identity

Every identity is surjective, an epimorphism and has a right inverse (the identity itself).

Identity.lean

-- The identity is surjective
theorem TIdSurj : surjective (@id A) := by
  -- rw [surjective] -- rw to recover the definition
  intro a 
  apply Exists.intro a 
  exact rfl 

-- The identity is an epimorphism
theorem TIdMon : epimorphism (@id A) := by
  -- rw [epimorphism] -- rw to recover the definition
  intro C g h h1 
  calc
    g = g ∘ id := by exact rfl
    _ = h ∘ id := by exact h1 
    _ = h      := by exact rfl 

-- The identity has a right inverse
theorem TIdHasRightInv : hasrightinv (@id A) := by
  -- rw [hasrightinv] -- rw to recover the definition
  apply Exists.intro id
  exact rfl

Exercises

Exercises.lean

-- Negation of surjective
theorem TNegSurj {A B : Type} {f: A → B} : ¬ (surjective f) ↔ ∃(b : B), 
∀ (a : A), f a ≠ b := by sorry

-- The composition of surjective functions is surjective
theorem TCompSurj {A B : Type} {f : A → B} {g : B → C} (h1 : surjective f)
(h2 : surjective g) : surjective (g∘f) := by sorry

-- If the composition (g∘f) is surjective, then g is surjective
theorem TCompLSurj {A B : Type} {f : A → B} {g : B → C} 
(h1 : surjective (g∘f)) : (surjective g) := by sorry

-- Surjective and Epimorphism are equivalent concepts
theorem TCarEpiSurj {A B : Type} {f : A → B} : surjective f ↔ epimorphism f := by sorry
  
-- If a function has a right inverse then it is surjective
theorem THasRightInvtoInj {A B : Type} {f : A → B} : hasrightinv f → surjective f := by sorry

Bijections

In this section, we introduce the concepts of bijective function and isomorphism and we examine their relationships and key properties.

Bijective

We say that a function f : A → B is bijective if it is injective and surjective.

Bijective.lean

def bijective {A B : Type} (f : A → B) : Prop := injective f ∧ surjective f

Isomorphism

We say that a function f : A → B is an isomorphism if there exists a function g : B → A such that g∘f = id ∧ f∘g = id.

Isomorphism.lean

def isomorphism {A B : Type} (f : A → B) : Prop := ∃ (g : B → A), 
g∘f = id ∧ f∘g = id 

An example: The identity

Every identity is bijective and an isomorphism.

Identity.lean

-- The identity is bijective
theorem TIdBij : bijective (@id A) := by
  -- rw [bijective] -- rw to recover the definition
  apply And.intro
  exact TIdInj A
  exact TIdSurj A

-- The identity is an isomorphism
theorem TIdMon : isomorphism (@id A) := by
  rw [isomorphism] -- rw to recover the definition
  apply Exists.intro id
  apply And.intro
  exact rfl
  exact rfl

Exercises

Exercises.lean

-- The composition of bijective functions is bijective
theorem TCompBij {A B : Type} {f : A → B} {g : B → C} (h1 : bijective f)
(h2 : bijective g) : bijective (g∘f) := by sorry

-- A function is an isomorphism if and only if
-- it has left and right inverse
theorem TCarIso {A B : Type} {f : A → B} : isomorphism f ↔ (hasleftinv f 
∧ hasrightinv f) := by sorry

-- Every isomorphism is bijective
theorem TCarIsotoBij {A B : Type} {f : A → B} : isomorphism f → bijective f := by sorry