# Congruence relations and homomorphisms #

This file contains elementary definitions involving congruence relations and morphisms.

## Main definitions #

`Con.ker`

: the kernel of a monoid homomorphism as a congruence relation`Con.mk'`

: the map from a monoid to its quotient by a congruence relation`Con.lift`

: the homomorphism on the quotient given that the congruence is in the kernel`Con.map`

: homomorphism from a smaller to a larger quotient

## Tags #

congruence, congruence relation, quotient, quotient by congruence relation, monoid, quotient monoid

The kernel of a monoid homomorphism as a congruence relation.

## Equations

- Con.ker f = Con.mulKer ⇑f ⋯

## Instances For

The kernel of an `AddMonoid`

homomorphism as an additive congruence relation.

## Equations

- AddCon.ker f = AddCon.addKer ⇑f ⋯

## Instances For

The definition of the congruence relation defined by a monoid homomorphism's kernel.

The definition of the additive congruence relation defined by an
`AddMonoid`

homomorphism's kernel.

The kernel of the natural homomorphism from a monoid to its quotient by a congruence
relation `c`

equals `c`

.

The kernel of the natural homomorphism from an `AddMonoid`

to its
quotient by an additive congruence relation `c`

equals `c`

.

The natural homomorphism from a monoid to its quotient by a congruence relation is surjective.

The natural homomorphism from an `AddMonoid`

to its quotient by a congruence
relation is surjective.

Given a monoid homomorphism `f : N → M`

and a congruence relation `c`

on `M`

, the congruence
relation induced on `N`

by `f`

equals the kernel of `c`

's quotient homomorphism composed with
`f`

.

Given an `AddMonoid`

homomorphism `f : N → M`

and an additive congruence relation
`c`

on `M`

, the additive congruence relation induced on `N`

by `f`

equals the kernel of `c`

's
quotient homomorphism composed with `f`

.

The homomorphism on the quotient of a monoid by a congruence relation `c`

induced by a
homomorphism constant on `c`

's equivalence classes.

## Equations

- c.lift f H = { toFun := fun (x : c.Quotient) => Con.liftOn x ⇑f ⋯, map_one' := ⋯, map_mul' := ⋯ }

## Instances For

The homomorphism on the quotient of an `AddMonoid`

by an additive congruence
relation `c`

induced by a homomorphism constant on `c`

's equivalence classes.

## Equations

- c.lift f H = { toFun := fun (x : c.Quotient) => AddCon.liftOn x ⇑f ⋯, map_zero' := ⋯, map_add' := ⋯ }

## Instances For

The diagram describing the universal property for quotients of monoids commutes.

The diagram describing the universal property for quotients of `AddMonoid`

s
commutes.

The diagram describing the universal property for quotients of monoids commutes.

The diagram describing the universal property for quotients of
`AddMonoid`

s commutes.

The diagram describing the universal property for quotients of monoids commutes.

The diagram describing the universal property for quotients of
`AddMonoid`

s commutes.

Given a homomorphism `f`

from the quotient of a monoid by a congruence relation, `f`

equals the
homomorphism on the quotient induced by `f`

composed with the natural map from the monoid to
the quotient.

Given a homomorphism `f`

from the quotient of an `AddMonoid`

by an
additive congruence relation, `f`

equals the homomorphism on the quotient induced by `f`

composed
with the natural map from the `AddMonoid`

to the quotient.

Homomorphisms on the quotient of a monoid by a congruence relation are equal if they are equal on elements that are coercions from the monoid.

Homomorphisms on the quotient of an `AddMonoid`

by an additive congruence relation
are equal if they are equal on elements that are coercions from the `AddMonoid`

.

The uniqueness part of the universal property for quotients of monoids.

The uniqueness part of the universal property for quotients of `AddMonoid`

s.

Surjective monoid homomorphisms constant on a congruence relation `c`

's equivalence classes
induce a surjective homomorphism on `c`

's quotient.

Surjective `AddMonoid`

homomorphisms constant on an additive congruence
relation `c`

's equivalence classes induce a surjective homomorphism on `c`

's quotient.

Given a monoid homomorphism `f`

from `M`

to `P`

, the kernel of `f`

is the unique congruence
relation on `M`

whose induced map from the quotient of `M`

to `P`

is injective.

Given an `AddMonoid`

homomorphism `f`

from `M`

to `P`

, the kernel of `f`

is the unique additive congruence relation on `M`

whose induced map from the quotient of `M`

to `P`

is injective.

The homomorphism induced on the quotient of a monoid by the kernel of a monoid homomorphism.

## Equations

- Con.kerLift f = (Con.ker f).lift f ⋯

## Instances For

The homomorphism induced on the quotient of an `AddMonoid`

by the kernel
of an `AddMonoid`

homomorphism.

## Equations

- AddCon.kerLift f = (AddCon.ker f).lift f ⋯

## Instances For

The diagram described by the universal property for quotients of monoids, when the congruence relation is the kernel of the homomorphism, commutes.

The diagram described by the universal property for quotients
of `AddMonoid`

s, when the additive congruence relation is the kernel of the homomorphism,
commutes.

A monoid homomorphism `f`

induces an injective homomorphism on the quotient by `f`

's kernel.

An `AddMonoid`

homomorphism `f`

induces an injective homomorphism on the quotient
by `f`

's kernel.

Given congruence relations `c, d`

on a monoid such that `d`

contains `c`

, `d`

's quotient
map induces a homomorphism from the quotient by `c`

to the quotient by `d`

.

## Equations

- c.map d h = c.lift d.mk' ⋯

## Instances For

Given additive congruence relations `c, d`

on an `AddMonoid`

such that `d`

contains `c`

, `d`

's quotient map induces a homomorphism from the quotient by `c`

to the quotient
by `d`

.

## Equations

- c.map d h = c.lift d.mk' ⋯

## Instances For

Given congruence relations `c, d`

on a monoid such that `d`

contains `c`

, the definition of
the homomorphism from the quotient by `c`

to the quotient by `d`

induced by `d`

's quotient
map.

Given additive congruence relations `c, d`

on an `AddMonoid`

such that `d`

contains `c`

, the definition of the homomorphism from the quotient by `c`

to the quotient by `d`

induced by `d`

's quotient map.