GraphCriterion.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Graph characterization of finite congruence lattices

A finite lattice is the full congruence lattice of a nonempty finite algebra if and only if it admits a finite nonempty lattice-colored graph satisfying IsGraphWitness. Principal congruences supply the colors in one direction; all label-decreasing self-maps supply the unary operations in the other.

def OAI.FiniteCongruence.Admissible line 21
Source documentation
A label-decreasing self-map; collapsed edges are permitted.
Also declared: ComparatorChallenges/FiniteCongruenceGraph.lean:28 (same declaration text).
```
def Admissible {Lat Carrier : Type} [LE Lat] (color : Carrier → Carrier → Lat)
    (placement : Carrier → Carrier) : Prop :=
…
```
def OAI.FiniteCongruence.Marked line 26
Source documentation
An oriented image of a seed edge under an admissible map.
Also declared: ComparatorChallenges/FiniteCongruenceGraph.lean:32 (same declaration text).
```
def Marked {Lat Carrier : Type} [LE Lat] (color : Carrier → Carrier → Lat)
    (seeds : Finset (Carrier × Carrier)) (left right : Carrier) : Prop :=
…
```
def OAI.FiniteCongruence.Connected line 32
Source documentation
Finite paths in the undirected marked graph, including paths of length zero.
Also declared: ComparatorChallenges/FiniteCongruenceGraph.lean:37 (same declaration text).
```
def Connected {Lat Carrier : Type} [LE Lat] (color : Carrier → Carrier → Lat)
    (seeds : Finset (Carrier × Carrier)) (left right : Carrier) : Prop :=
…
```
def OAI.FiniteCongruence.IsGraphWitness line 38
Source documentation
Symmetric colors separate vertices, satisfy the join triangle inequality, detect order, and connect every pair below the join of any nonempty finite set of seed colors.
Also declared: ComparatorChallenges/FiniteCongruenceGraph.lean:41 (same declaration text).
```
def IsGraphWitness {Lat Carrier : Type} [Lattice Lat] [OrderBot Lat]
    (color : Carrier → Carrier → Lat) : Prop :=
…
```
def OAI.FiniteCongruence.HasGraphWitness line 50
Source documentation
The graph size is unbounded, but each individual witness is finite and nonempty.
Also declared: ComparatorChallenges/FiniteCongruenceGraph.lean:52 (same declaration text).
```
def HasGraphWitness (Lat : Type) [Lattice Lat] [OrderBot Lat] : Prop :=
…
```
def OAI.FiniteCongruence.principalColor line 58
Source documentation
Color a pair by its principal congruence, transported to the lattice.
```
noncomputable def principalColor (equiv : Lat ≃o Congruence alg) (left right : Carrier) : Lat :=
…
```
Mentions: OAI.FiniteCongruence.Congruence
theorem OAI.FiniteCongruence.principalColor_le line 62
theorem OAI.FiniteCongruence.map_bot_equality line 68
theorem OAI.FiniteCongruence.principalColor_eq_bot line 75
theorem OAI.FiniteCongruence.principalColor_triangle line 80
theorem OAI.FiniteCongruence.principalColor_reflect line 89
theorem OAI.FiniteCongruence.admissible_id line 104
theorem OAI.FiniteCongruence.Admissible.comp line 107
theorem OAI.FiniteCongruence.marked_map line 113
theorem OAI.FiniteCongruence.connected_map line 121
theorem OAI.FiniteCongruence.translation_admissible line 137
def OAI.FiniteCongruence.pathCongruence line 147
Source documentation
Connectivity in the marked graph is a congruence of the original algebra, not just of its admissible unary maps.
```
noncomputable def pathCongruence (equiv : Lat ≃o Congruence alg)
    (seeds : Finset (Carrier × Carrier)) : Congruence alg :=
…
```
Mentions: OAI.FiniteCongruence.Congruence
theorem OAI.FiniteCongruence.principalColor_connected line 154
theorem OAI.FiniteCongruence.principalColor_isGraphWitness line 172
def OAI.FiniteCongruence.graphAlgebra line 188
Source documentation
All label-decreasing maps, made into a finite list of unary total operations.
```
noncomputable def graphAlgebra (color : Carrier → Carrier → Lat) : Algebra Carrier := by
…
```
Mentions: OAI.FiniteCongruence.Algebra

theorem OAI.FiniteCongruence.graphAlgebra_preserves line 199

Source documentation

Every admissible map is one of the basic unary operations.

theorem graphAlgebra_preserves (color : Carrier → Carrier → Lat)
    (rel : Congruence (graphAlgebra color)) {placement : Carrier → Carrier}
    (admissible : Admissible color placement) {left right : Carrier} (related : rel left right) :
    rel (placement left) (placement right) := by
…

Mentions: OAI.FiniteCongruence.Congruence, OAI.FiniteCongruence.graphAlgebra, OAI.FiniteCongruence.Admissible

def OAI.FiniteCongruence.labelCongruence line 210
Source documentation
Each lattice element defines the equivalence relation of edges below its color.
```
noncomputable def labelCongruence (color : Carrier → Carrier → Lat)
    (witness : IsGraphWitness color) (bound : Lat) : Congruence (graphAlgebra color) := by
…
```
Mentions: OAI.FiniteCongruence.IsGraphWitness, OAI.FiniteCongruence.Congruence, OAI.FiniteCongruence.graphAlgebra
theorem OAI.FiniteCongruence.labelCongruence_apply line 226
theorem OAI.FiniteCongruence.labelCongruence_le_iff line 230

theorem OAI.FiniteCongruence.connected_below_congruence line 243

Source documentation

Equivalence closure of marked edges lies in every congruence containing the seed edges.

theorem connected_below_congruence (color : Carrier → Carrier → Lat)
    (rel : Congruence (graphAlgebra color)) (seeds : Finset (Carrier × Carrier))
    (contains : ∀ edge ∈ seeds, rel edge.1 edge.2) {left right : Carrier}
    (connected : Connected color seeds left right) : rel left right := by
…

Mentions: OAI.FiniteCongruence.Congruence, OAI.FiniteCongruence.graphAlgebra, OAI.FiniteCongruence.Connected

theorem OAI.FiniteCongruence.labelCongruence_surjective line 256
Source documentation
Every congruence is recovered using all its related pairs.
```
theorem labelCongruence_surjective [Nonempty Carrier] (color : Carrier → Carrier → Lat)
    (witness : IsGraphWitness color) : Function.Surjective (labelCongruence color witness) := by
…
```
Mentions: OAI.FiniteCongruence.IsGraphWitness, OAI.FiniteCongruence.labelCongruence
def OAI.FiniteCongruence.graphOrderIso line 278
Source documentation
The lattice is isomorphic to the full congruence lattice of the graph algebra.
```
noncomputable def graphOrderIso [Nonempty Carrier] (color : Carrier → Carrier → Lat)
    (witness : IsGraphWitness color) : Lat ≃o Congruence (graphAlgebra color) :=
…
```
Mentions: OAI.FiniteCongruence.IsGraphWitness, OAI.FiniteCongruence.Congruence, OAI.FiniteCongruence.graphAlgebra
theorem OAI.FiniteCongruence.graph_criterion line 291
Source documentation
A finite lattice is representable as the full congruence lattice of a nonempty finite algebra exactly when it has a finite nonempty colored-graph witness.
Distinct definitions of this name: ComparatorChallenges/FiniteCongruenceGraph.lean:57 (same statement text; different proof or body). Qualify references as OAI.FiniteCongruence.graph_criterion@path.
```
theorem graph_criterion (Lat : Type) [Fintype Lat] [Lattice Lat] [OrderBot Lat] :
    Representable Lat ↔ HasGraphWitness Lat := by
…
```
Mentions: OAI.FiniteCongruence.Representable, OAI.FiniteCongruence.HasGraphWitness