Equivalence relations
This file defines the complete lattice of equivalence relations on a type, results about the inductively defined equivalence closure of a binary relation, and the analogues of some isomorphism theorems for quotients of arbitrary types.
Implementation notes
The function rel and lemmas ending in ' make it easier to talk about different
equivalence relations on the same type.
The complete lattice instance for equivalence relations could have been defined by lifting
the Galois insertion of equivalence relations on α into binary relations on α, and then using
complete_lattice.copy to define a complete lattice instance with more appropriate
definitional equalities (a similar example is filter.complete_lattice in
order/filter/basic.lean). This does not save space, however, and is less clear.
Partitions are not defined as a separate structure here; users are encouraged to
reason about them using the existing setoid and its infrastructure.
Tags
setoid, equivalence, iseqv, relation, equivalence relation
A version of quotient.eq' compatible with setoid.rel, to make rewriting possible.
The kernel of a function is an equivalence relation.
The kernel of the quotient map induced by an equivalence relation r equals r.
Given types α, β, the product of two equivalence relations r on α and s on β:
(x₁, x₂), (y₁, y₂) ∈ α × β are related by r.prod s iff x₁ is related to y₁
by r and x₂ is related to y₂ by s.
The underlying binary operation of the infimum of a set of equivalence relations is the infimum of the set's image under the map to the underlying binary operation.
Equations
- setoid.partial_order = {le := has_le.le setoid.has_le, lt := λ (r s : setoid α), r ≤ s ∧ ¬s ≤ r, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
The complete lattice of equivalence relations on a type, with bottom element =
and top element the trivial equivalence relation.
Equations
- setoid.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (setoid α) setoid.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (setoid α) setoid.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (setoid α) setoid.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf setoid.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, top := {r := λ (_x _x : α), true, iseqv := _}, le_top := _, bot := {r := eq α, iseqv := _}, bot_le := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (setoid α) setoid.complete_lattice._proof_1), Inf := complete_lattice.Inf (complete_lattice_of_Inf (setoid α) setoid.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
The inductively defined equivalence closure of a binary relation r is the infimum of the set of all equivalence relations containing r.
The supremum of two equivalence relations r and s is the equivalence closure of the binary
relation x is related to y by r or s.
The supremum of 2 equivalence relations r and s is the equivalence closure of the supremum of the underlying binary operations.
The supremum of a set S of equivalence relations is the equivalence closure of the binary
relation there exists r ∈ S relating x and y.
The supremum of a set of equivalence relations is the equivalence closure of the supremum of the set's image under the map to the underlying binary operation.
The equivalence closure of an equivalence relation r is r.
Equivalence closure is idempotent.
The equivalence closure of a binary relation r is contained in any equivalence relation containing r.
Equivalence closure of binary relations is monotonic.
There is a Galois insertion of equivalence relations on α into binary relations on α, with equivalence closure the lower adjoint.
A function from α to β is injective iff its kernel is the bottom element of the complete lattice of equivalence relations on α.
The elements related to x ∈ α by the kernel of f are those in the preimage of f(x) under f.
Equivalence between functions α → β such that r x y → f x = f y and functions
quotient r → β.
Equations
- r.lift_equiv = {to_fun := λ (f : {f // r ≤ setoid.ker f}), quotient.lift ↑f _, inv_fun := λ (f : quotient r → β), ⟨f ∘ quotient.mk, _⟩, left_inv := _, right_inv := _}
The uniqueness part of the universal property for quotients of an arbitrary type.
Given a map f from α to β, the natural map from the quotient of α by the kernel of f is injective.
Given a map f from α to β, the kernel of f is the unique equivalence relation on α whose induced map from the quotient of α to β is injective.
The first isomorphism theorem for sets: the quotient of α by the kernel of a function f bijects with f's image.
Equations
- setoid.quotient_ker_equiv_range f = equiv.of_bijective (quotient.lift (λ (x : α), ⟨f x, _⟩) _) _
The quotient of α by the kernel of a surjective function f bijects with f's codomain.
Equations
Given a function f : α → β and equivalence relation r on α, the equivalence
closure of the relation on f's image defined by 'x ≈ y iff the elements of f⁻¹(x) are
related to the elements of f⁻¹(y) by r.'
Given a surjective function f whose kernel is contained in an equivalence relation r, the equivalence relation on f's codomain defined by x ≈ y ↔ the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by r.
A special case of the equivalence closure of an equivalence relation r equalling r.
Given a function f : α → β, an equivalence relation r on β induces an equivalence
relation on α defined by 'x ≈ y iff f(x) is related to f(y) by r'.
Given a map f : N → M and an equivalence relation r on β, the equivalence relation
induced on α by f equals the kernel of r's quotient map composed with f.
The second isomorphism theorem for sets.
Equations
The third isomorphism theorem for sets.
Equations
- r.quotient_quotient_equiv_quotient s h = {to_fun := λ (x : quotient (setoid.ker (quot.map_right h))), x.lift_on' (λ (w : quot (λ (x y : α), r.rel x y)), quotient.lift_on' w quotient.mk _) _, inv_fun := λ (x : quotient s), x.lift_on' (λ (w : α), ⟦⟦w⟧⟧) _, left_inv := _, right_inv := _}
Given an equivalence relation r on α, the order-preserving bijection between the set of equivalence relations containing r and the equivalence relations on the quotient of α by r.
Equations
- r.correspondence = {to_equiv := {to_fun := λ (s : {s // r ≤ s}), s.val.map_of_surjective quotient.mk _ quotient.exists_rep, inv_fun := λ (s : setoid (quotient r)), ⟨setoid.comap quotient.mk s, _⟩, left_inv := _, right_inv := _}, map_rel_iff' := _}