Congruence.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Congruences of finite-signature algebras

An algebra has finitely many total operations of finite arity, including possibly nullary operations. Its congruences are ordered by inclusion. Compatibility with every operation is equivalent to stability under the unary translations obtained by fixing all but one input.

structure OAI.FiniteCongruence.Algebra line 18
Source documentation
A finite list of total finite-arity operations. Arity zero is allowed.
Also declared: ComparatorChallenges/FiniteCongruenceGraph.lean:10 (same declaration text).
```
structure Algebra (Carrier : Type) where
…
```
def OAI.FiniteCongruence.Compatible line 24
Source documentation
Compatibility with all operations of an algebra.
Also declared: ComparatorChallenges/FiniteCongruenceGraph.lean:15 (same declaration text).
```
def Compatible {Carrier : Type} (alg : Algebra Carrier) (rel : Setoid Carrier) : Prop :=
…
```
Mentions: OAI.FiniteCongruence.Algebra
def OAI.FiniteCongruence.Congruence line 29
Source documentation
The full ordered set of congruences, ordered by inclusion of relations.
Also declared: ComparatorChallenges/FiniteCongruenceGraph.lean:19 (same declaration text).
```
def Congruence {Carrier : Type} (alg : Algebra Carrier) :=
…
```
Mentions: OAI.FiniteCongruence.Algebra
instance OAI.FiniteCongruence.(instance at line 32) line 32
def OAI.FiniteCongruence.Representable line 36
Source documentation
Order-isomorphism with the entire congruence lattice of a nonempty finite algebra.
Also declared: ComparatorChallenges/FiniteCongruenceGraph.lean:25 (same declaration text).
```
def Representable (Lat : Type) [PartialOrder Lat] : Prop :=
…
```
instance OAI.FiniteCongruence.(instance at line 39) line 39
theorem OAI.FiniteCongruence.Congruence.ext line 47
theorem OAI.FiniteCongruence.Congruence.refl line 51
theorem OAI.FiniteCongruence.Congruence.symm line 53
theorem OAI.FiniteCongruence.Congruence.trans line 56
theorem OAI.FiniteCongruence.Congruence.compatible line 60
def OAI.FiniteCongruence.Congruence.equality line 65
Source documentation
Equality is the least congruence.
```
def equality (alg : Algebra Carrier) : Congruence alg :=
…
```
Mentions: OAI.FiniteCongruence.Algebra, OAI.FiniteCongruence.Congruence
theorem OAI.FiniteCongruence.Congruence.equality_apply line 72
theorem OAI.FiniteCongruence.Congruence.equality_le line 75
def OAI.FiniteCongruence.Congruence.principal line 81
Source documentation
The intersection of all congruences containing the generating pair.
```
def principal (alg : Algebra Carrier) (left right : Carrier) : Congruence alg :=
…
```
Mentions: OAI.FiniteCongruence.Algebra, OAI.FiniteCongruence.Congruence
theorem OAI.FiniteCongruence.Congruence.principal_pair line 90
theorem OAI.FiniteCongruence.Congruence.principal_le line 93
theorem OAI.FiniteCongruence.Congruence.principal_comm line 101

theorem OAI.FiniteCongruence.relation_map_of_updates line 111

Source documentation

Stability under all single-coordinate changes entails compatibility with a total operation. For nullary operations the two input tuples are equal.

theorem relation_map_of_updates {Carrier : Type} (rel : Setoid Carrier) {arity : ℕ}
    (operation : (Fin arity → Carrier) → Carrier)
    (stable : ∀ (coord : Fin arity) (inputs : Fin arity → Carrier) (left right : Carrier),
      rel left right →
      rel (operation (Function.update inputs coord left))
        (operation (Function.update inputs coord right)))
    (left right : Fin arity → Carrier) (related : ∀ coord, rel (left coord) (right coord)) :
    rel (operation left) (operation right) := by
…

def OAI.FiniteCongruence.translation line 138

Source documentation

A one-variable translation is obtained by fixing all but one input of an operation.

def translation {Carrier : Type} (alg : Algebra Carrier) (index : Fin alg.numOps)
    (coord : Fin (alg.arity index)) (inputs : Fin (alg.arity index) → Carrier)
    (point : Carrier) : Carrier :=
…

Mentions: OAI.FiniteCongruence.Algebra

theorem OAI.FiniteCongruence.translation_preserves line 143
theorem OAI.FiniteCongruence.compatible_iff_translations line 154