Supporting results for pointwise provable equality.

The least congruence containing a relation, defined as the intersection of all equivalence relations compatible with the given binary operation. No associativity, identity, or arithmetic hypothesis is required.

def PointwiseComposition.FailureOfComposition.CompositionClosure.IsCongruence {A : Type u} (op : A → A → A) (R : A → A → Prop) : Prop

The Is Congruence construction in FailureOfComposition.CompositionClosure.

Equations

• PointwiseComposition.FailureOfComposition.CompositionClosure.IsCongruence op R = (Equivalence R ∧ ∀ (a a' b b' : A), R a a' → R b b' → R (op a b) (op a' b'))

def PointwiseComposition.FailureOfComposition.CompositionClosure.Generated {A : Type u} (op : A → A → A) (r : A → A → Prop) (a b : A) : Prop

The Generated construction in FailureOfComposition.CompositionClosure.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FailureOfComposition.CompositionClosure.base {A : Type u} (op : A → A → A) (r : A → A → Prop) {a b : A} (h : r a b) : Generated op r a b

theorem PointwiseComposition.FailureOfComposition.CompositionClosure.refl {A : Type u} (op : A → A → A) (r : A → A → Prop) (a : A) : Generated op r a a

theorem PointwiseComposition.FailureOfComposition.CompositionClosure.symm {A : Type u} {op : A → A → A} {r : A → A → Prop} {a b : A} (h : Generated op r a b) : Generated op r b a

theorem PointwiseComposition.FailureOfComposition.CompositionClosure.trans {A : Type u} {op : A → A → A} {r : A → A → Prop} {a b c : A} (hab : Generated op r a b) (hbc : Generated op r b c) : Generated op r a c

theorem PointwiseComposition.FailureOfComposition.CompositionClosure.comp {A : Type u} {op : A → A → A} {r : A → A → Prop} {a a' b b' : A} (ha : Generated op r a a') (hb : Generated op r b b') : Generated op r (op a b) (op a' b')

theorem PointwiseComposition.FailureOfComposition.CompositionClosure.comp_left {A : Type u} (op : A → A → A) (r : A → A → Prop) (c : A) {a b : A} (h : Generated op r a b) : Generated op r (op c a) (op c b)

theorem PointwiseComposition.FailureOfComposition.CompositionClosure.comp_right {A : Type u} (op : A → A → A) (r : A → A → Prop) (c : A) {a b : A} (h : Generated op r a b) : Generated op r (op a c) (op b c)

theorem PointwiseComposition.FailureOfComposition.CompositionClosure.least {A : Type u} {op : A → A → A} {r R : A → A → Prop} (hR : IsCongruence op R) (hr : ∀ (x y : A), r x y → R x y) {a b : A} (h : Generated op r a b) : R a b

Every congruence containing the generators contains the generated relation.

theorem PointwiseComposition.FailureOfComposition.CompositionClosure.isCongruence {A : Type u} (op : A → A → A) (r : A → A → Prop) : IsCongruence op (Generated op r)

def PointwiseComposition.FailureOfComposition.CompositionClosure.setoid {A : Type u} (op : A → A → A) (r : A → A → Prop) : Setoid A

The setoid construction in FailureOfComposition.CompositionClosure.

Equations

• PointwiseComposition.FailureOfComposition.CompositionClosure.setoid op r = { r := PointwiseComposition.FailureOfComposition.CompositionClosure.Generated op r, iseqv := ⋯ }

theorem PointwiseComposition.FailureOfComposition.CompositionClosure.monotone {A : Type u} {op : A → A → A} {r s : A → A → Prop} (hrs : ∀ (x y : A), r x y → s x y) {a b : A} (h : Generated op r a b) : Generated op s a b

theorem PointwiseComposition.FailureOfComposition.CompositionClosure.iff_of_isCongruence {A : Type u} {op : A → A → A} {r : A → A → Prop} (hr : IsCongruence op r) (a b : A) : Generated op r a b ↔ r a b

theorem PointwiseComposition.FailureOfComposition.CompositionClosure.idempotent {A : Type u} (op : A → A → A) (r : A → A → Prop) (a b : A) : Generated op (Generated op r) a b ↔ Generated op r a b

theorem PointwiseComposition.FailureOfComposition.CompositionClosure.map {A : Type u} {B : Type v} (opA : A → A → A) (opB : B → B → B) (r : A → A → Prop) (s : B → B → Prop) (f : A → B) (hop : ∀ (x y : A), f (opA x y) = opB (f x) (f y)) (hrs : ∀ (x y : A), r x y → s (f x) (f y)) {a b : A} (h : Generated opA r a b) : Generated opB s (f a) (f b)

A homomorphism carrying generators into generators preserves their generated congruences, even between different universes.