# Congruence relations on abelian groups

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.

Created on 2023-03-08.

module group-theory.congruence-relations-abelian-groups where

Imports
open import foundation.binary-relations
open import foundation.equivalence-relations
open import foundation.equivalences
open import foundation.identity-types
open import foundation.propositions
open import foundation.torsorial-type-families
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.congruence-relations-groups


## Idea

A congruence relation on an abelian group A is a congruence relation on the underlying group of A.

## Definition

is-congruence-Ab :
{l1 l2 : Level} (A : Ab l1) →
equivalence-relation l2 (type-Ab A) →
UU (l1 ⊔ l2)
is-congruence-Ab A = is-congruence-Group (group-Ab A)

congruence-Ab : {l : Level} (l2 : Level) (A : Ab l) → UU (l ⊔ lsuc l2)
congruence-Ab l2 A = congruence-Group l2 (group-Ab A)

module _
{l1 l2 : Level} (A : Ab l1) (R : congruence-Ab l2 A)
where

equivalence-relation-congruence-Ab : equivalence-relation l2 (type-Ab A)
equivalence-relation-congruence-Ab =
equivalence-relation-congruence-Group (group-Ab A) R

prop-congruence-Ab : Relation-Prop l2 (type-Ab A)
prop-congruence-Ab = prop-congruence-Group (group-Ab A) R

sim-congruence-Ab : (x y : type-Ab A) → UU l2
sim-congruence-Ab = sim-congruence-Group (group-Ab A) R

is-prop-sim-congruence-Ab :
(x y : type-Ab A) → is-prop (sim-congruence-Ab x y)
is-prop-sim-congruence-Ab =
is-prop-sim-congruence-Group (group-Ab A) R

concatenate-eq-sim-congruence-Ab :
{x1 x2 y : type-Ab A} →
x1 ＝ x2 → sim-congruence-Ab x2 y → sim-congruence-Ab x1 y
concatenate-eq-sim-congruence-Ab =
concatenate-eq-sim-congruence-Group (group-Ab A) R

concatenate-sim-eq-congruence-Ab :
{x y1 y2 : type-Ab A} →
sim-congruence-Ab x y1 → y1 ＝ y2 → sim-congruence-Ab x y2
concatenate-sim-eq-congruence-Ab =
concatenate-sim-eq-congruence-Group (group-Ab A) R

concatenate-eq-sim-eq-congruence-Ab :
{x1 x2 y1 y2 : type-Ab A} → x1 ＝ x2 →
sim-congruence-Ab x2 y1 →
y1 ＝ y2 → sim-congruence-Ab x1 y2
concatenate-eq-sim-eq-congruence-Ab =
concatenate-eq-sim-eq-congruence-Group (group-Ab A) R

refl-congruence-Ab : is-reflexive sim-congruence-Ab
refl-congruence-Ab = refl-congruence-Group (group-Ab A) R

symmetric-congruence-Ab : is-symmetric sim-congruence-Ab
symmetric-congruence-Ab = symmetric-congruence-Group (group-Ab A) R

equiv-symmetric-congruence-Ab :
(x y : type-Ab A) →
sim-congruence-Ab x y ≃ sim-congruence-Ab y x
equiv-symmetric-congruence-Ab =
equiv-symmetric-congruence-Group (group-Ab A) R

transitive-congruence-Ab :
is-transitive sim-congruence-Ab
transitive-congruence-Ab = transitive-congruence-Group (group-Ab A) R

add-congruence-Ab = mul-congruence-Group (group-Ab A) R

(x : type-Ab A) {y z : type-Ab A} →
sim-congruence-Ab y z →
left-add-congruence-Ab = left-mul-congruence-Group (group-Ab A) R

{x y : type-Ab A} → sim-congruence-Ab x y →
(z : type-Ab A) →
right-add-congruence-Ab = right-mul-congruence-Group (group-Ab A) R

conjugation-congruence-Ab :
(x : type-Ab A) {y z : type-Ab A} → sim-congruence-Ab y z →
sim-congruence-Ab (conjugation-Ab A x y) (conjugation-Ab A x z)
conjugation-congruence-Ab =
conjugation-congruence-Group (group-Ab A) R

conjugation-congruence-Ab' :
(x : type-Ab A) {y z : type-Ab A} →
sim-congruence-Ab y z →
sim-congruence-Ab
( conjugation-Ab' A x y)
( conjugation-Ab' A x z)
conjugation-congruence-Ab' =
conjugation-congruence-Group' (group-Ab A) R

sim-right-subtraction-zero-congruence-Ab : (x y : type-Ab A) → UU l2
sim-right-subtraction-zero-congruence-Ab =
sim-right-div-unit-congruence-Group (group-Ab A) R

map-sim-right-subtraction-zero-congruence-Ab :
{x y : type-Ab A} → sim-congruence-Ab x y →
sim-right-subtraction-zero-congruence-Ab x y
map-sim-right-subtraction-zero-congruence-Ab =
map-sim-right-div-unit-congruence-Group (group-Ab A) R

map-inv-sim-right-subtraction-zero-congruence-Ab :
{x y : type-Ab A} →
sim-right-subtraction-zero-congruence-Ab x y → sim-congruence-Ab x y
map-inv-sim-right-subtraction-zero-congruence-Ab =
map-inv-sim-right-div-unit-congruence-Group (group-Ab A) R

sim-left-subtraction-zero-congruence-Ab : (x y : type-Ab A) → UU l2
sim-left-subtraction-zero-congruence-Ab =
sim-left-div-unit-congruence-Group (group-Ab A) R

map-sim-left-subtraction-zero-congruence-Ab :
{x y : type-Ab A} → sim-congruence-Ab x y →
sim-left-subtraction-zero-congruence-Ab x y
map-sim-left-subtraction-zero-congruence-Ab =
map-sim-left-div-unit-congruence-Group (group-Ab A) R

map-inv-sim-left-subtraction-zero-congruence-Ab :
{x y : type-Ab A} → sim-left-subtraction-zero-congruence-Ab x y →
sim-congruence-Ab x y
map-inv-sim-left-subtraction-zero-congruence-Ab =
map-inv-sim-left-div-unit-congruence-Group (group-Ab A) R

neg-congruence-Ab :
{x y : type-Ab A} → sim-congruence-Ab x y →
sim-congruence-Ab (neg-Ab A x) (neg-Ab A y)
neg-congruence-Ab = inv-congruence-Group (group-Ab A) R


## Properties

### Characterizing equality of congruence relations on groups

relate-same-elements-congruence-Ab :
{l1 l2 l3 : Level} (A : Ab l1) →
congruence-Ab l2 A → congruence-Ab l3 A → UU (l1 ⊔ l2 ⊔ l3)
relate-same-elements-congruence-Ab A =
relate-same-elements-congruence-Group (group-Ab A)

refl-relate-same-elements-congruence-Ab :
{l1 l2 : Level} (A : Ab l1) (R : congruence-Ab l2 A) →
relate-same-elements-congruence-Ab A R R
refl-relate-same-elements-congruence-Ab A =
refl-relate-same-elements-congruence-Group (group-Ab A)

is-torsorial-relate-same-elements-congruence-Ab :
{l1 l2 : Level} (A : Ab l1) (R : congruence-Ab l2 A) →
is-torsorial (relate-same-elements-congruence-Ab A R)
is-torsorial-relate-same-elements-congruence-Ab A =
is-torsorial-relate-same-elements-congruence-Group (group-Ab A)

relate-same-elements-eq-congruence-Ab :
{l1 l2 : Level} (A : Ab l1) (R S : congruence-Ab l2 A) →
R ＝ S → relate-same-elements-congruence-Ab A R S
relate-same-elements-eq-congruence-Ab A =
relate-same-elements-eq-congruence-Group (group-Ab A)

is-equiv-relate-same-elements-eq-congruence-Ab :
{l1 l2 : Level} (A : Ab l1) (R S : congruence-Ab l2 A) →
is-equiv (relate-same-elements-eq-congruence-Ab A R S)
is-equiv-relate-same-elements-eq-congruence-Ab A =
is-equiv-relate-same-elements-eq-congruence-Group (group-Ab A)

extensionality-congruence-Ab :
{l1 l2 : Level} (A : Ab l1) (R S : congruence-Ab l2 A) →
(R ＝ S) ≃ relate-same-elements-congruence-Ab A R S
extensionality-congruence-Ab A =
extensionality-congruence-Group (group-Ab A)

eq-relate-same-elements-congruence-Ab :
{l1 l2 : Level} (A : Ab l1) (R S : congruence-Ab l2 A) →
relate-same-elements-congruence-Ab A R S → R ＝ S
eq-relate-same-elements-congruence-Ab A =
eq-relate-same-elements-congruence-Group (group-Ab A)