Congruence relations #
This file proves basic properties of the quotient of a type by a congruence relation.
The second half of the file concerns congruence relations on monoids, in which case the quotient by the congruence relation is also a monoid. There are results about the universal property of quotients of monoids, and the isomorphism theorems for monoids.
Implementation notes #
A congruence relation on a monoid M
can be thought of as a submonoid of M × M
for which
membership is an equivalence relation, but whilst this fact is established in the file, it is not
used, since this perspective adds more layers of definitional unfolding.
Tags #
congruence, congruence relation, quotient, quotient by congruence relation, monoid, quotient monoid, isomorphism theorems
Given types with multiplications M, N
, the product of two congruence relations c
on M
and
d
on N
: (x₁, x₂), (y₁, y₂) ∈ M × N
are related by c.prod d
iff x₁
is related to y₁
by c
and x₂
is related to y₂
by d
.
Equations
Instances For
Given types with additions M, N
, the product of two congruence relations
c
on M
and d
on N
: (x₁, x₂), (y₁, y₂) ∈ M × N
are related by c.prod d
iff x₁
is related to y₁
by c
and x₂
is related to y₂
by d
.
Equations
Instances For
The submonoid of M × M
defined by a congruence relation on a monoid M
.
Equations
Instances For
The AddSubmonoid
of M × M
defined by an additive congruence
relation on an AddMonoid
M
.
Equations
Instances For
The congruence relation on a monoid M
from a submonoid of M × M
for which membership
is an equivalence relation.
Equations
Instances For
The additive congruence relation on an AddMonoid
M
from
an AddSubmonoid
of M × M
for which membership is an equivalence relation.
Equations
Instances For
Coercion from a congruence relation c
on a monoid M
to the submonoid of M × M
whose
elements are (x, y)
such that x
is related to y
by c
.
Equations
Coercion from a congruence relation c
on an AddMonoid
M
to the AddSubmonoid
of M × M
whose elements are (x, y)
such that x
is related to y
by c
.
Equations
Given a congruence relation c
on a monoid and a homomorphism f
constant on c
's
equivalence classes, f
has the same image as the homomorphism that f
induces on the
quotient.
Given an additive congruence relation c
on an AddMonoid
and a homomorphism f
constant on c
's equivalence classes, f
has the same image as the homomorphism that f
induces
on the quotient.
Given a monoid homomorphism f
, the induced homomorphism on the quotient by f
's kernel has
the same image as f
.
Given an AddMonoid
homomorphism f
, the induced homomorphism
on the quotient by f
's kernel has the same image as f
.
The first isomorphism theorem for monoids.
Equations
Instances For
The first isomorphism theorem for AddMonoid
s.
Equations
Instances For
The first isomorphism theorem for monoids in the case of a homomorphism with right inverse.
Equations
Instances For
The first isomorphism theorem for AddMonoid
s in the case of a homomorphism
with right inverse.
Equations
Instances For
The first isomorphism theorem for Monoids in the case of a surjective homomorphism.
For a computable
version, see Con.quotientKerEquivOfRightInverse
.
Equations
Instances For
The first isomorphism theorem for AddMonoid
s in the case of a surjective
homomorphism.
For a computable
version, see AddCon.quotientKerEquivOfRightInverse
.
Equations
Instances For
If e : M →* N is surjective then (c.comap e).Quotient ≃* c.Quotient with c : Con N
Equations
Instances For
If e : M →* N is surjective then (c.comap e).Quotient ≃* c.Quotient with c : AddCon N
Equations
Instances For
This version infers the surjectivity of the function from a MulEquiv function
This version infers the surjectivity of the function from a MulEquiv function
The second isomorphism theorem for monoids.
Equations
Instances For
The second isomorphism theorem for AddMonoid
s.