RingCon.ext'
theorem RingCon.ext' : ∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] {c d : RingCon R}, ⇑c = ⇑d → c = d
This theorem states that, given a type `R` with addition and multiplication structures, if we have two congruence relations for rings (`c` and `d`), then if their underlying binary relations (obtained by applying the coercion function `⇑`) are equal, the congruence relations themselves must be equal. Essentially, this is asserting that the mapping from a congruence relation to its underlying binary relation is injective in the context of rings, meaning that distinct congruence relations will map to distinct binary relations.
More concisely: If two congruence relations on a ring have equal underlying binary relations, then they are equal.
|
RingCon.ringConGen_le
theorem RingCon.ringConGen_le :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop} {c : RingCon R},
(∀ (x y : R), r x y → c x y) → ringConGen r ≤ c
The theorem `RingCon.ringConGen_le` states that for any type `R` with addition and multiplication operations, given a binary relation `r` and a congruence relation `c` on `R`, if `c` contains the relation `r`, then the smallest congruence relation containing `r` (denoted by `ringConGen r`) is contained in `c`. In more mathematical terms, if for all `x` and `y` in `R`, `r x y` implies `c x y`, then the smallest congruence relation that includes `r` is a subset of `c`. This theorem establishes that any congruence relation containing a specific relation must also contain the smallest congruence relation including that specific relation.
More concisely: If a relation `r` is contained in a congruence relation `c` on a ring `R`, then the smallest congruence relation `ringConGen r` containing `r` is a subset of `c`.
|
RingCon.eq
theorem RingCon.eq : ∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] (c : RingCon R) {a b : R}, ↑a = ↑b ↔ c a b := by
sorry
This theorem states that, given a ring `R` with addition `Add R` and multiplication `Mul R`, and a congruence relation `c : RingCon R`, any two elements `a` and `b` of `R` are related by `c` if and only if they are represented by the same element in the quotient of `R` by `c`. In other words, `a` and `b` are congruent under `c` precisely when their quotient group equivalence classes (denoted by `↑a` and `↑b`) are equal.
More concisely: For any ring `R` with addition `Add R` and multiplication `Mul R`, and a congruence relation `c : RingCon R`, elements `a` and `b` of `R` are congruent under `c` if and only if their quotient group equivalence classes `[a]_c` and `[b]_c` are equal.
|
RingCon.refl
theorem RingCon.refl : ∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] (c : RingCon R) (x : R), c x x
This theorem, `RingCon.refl`, states that for all types `R` that have both addition and multiplication operations, and for any `RingCon` relation `c` on `R` and any element `x` from `R`, `c` is reflexive. In other words, `x` is related to itself under the `RingCon` relation `c`. This is analogous to the reflexive property in mathematics where for any element `x` in a set, `x` is always related to itself.
More concisely: For any relation `c` on a type `R` with addition and multiplication operations, `c` is reflexive, that is, for all `x` in `R`, `x` is related to `x` under `c`.
|
RingCon.ringConGen_eq
theorem RingCon.ringConGen_eq :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] (r : R → R → Prop),
ringConGen r = sInf {s | ∀ (x y : R), r x y → s x y}
The theorem `RingCon.ringConGen_eq` states that for any type `R` that has both addition and multiplication operations, and any binary relation `r` on `R`, the smallest congruence relation containing `r` (which is inductively defined) is equal to the infimum of the set of all congruence relations that contain `r`. Here, a congruence relation on `R` is a relation that is compatible with the addition and multiplication operations on `R`. This theorem basically asserts the existence and uniqueness of the smallest congruence relation containing a given binary relation in the context of a ring.
More concisely: The smallest congruence relation containing a binary relation on a ring is equal to the infimum of all congruence relations that contain it.
|
RingCon.le_def
theorem RingCon.le_def :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] {c d : RingCon R}, c ≤ d ↔ ∀ {x y : R}, c x y → d x y
This theorem defines the order relation `≤` for congruence relations over rings. Given a type `R` that supports addition and multiplication operations, and two ring congruence relations `c` and `d` over `R`, the theorem states that `c` is less than or equal to `d` if and only if, for any elements `x` and `y` of `R`, if `x` is congruent to `y` under the relation `c`, then `x` is also congruent to `y` under the relation `d`.
More concisely: For ring congruence relations `c` and `d` over a ring `R`, `c` is less or equal to `d` if and only if for all `x, y` in `R`, `x ≡ y (mod c)` implies `x ≡ y (mod d)`.
|
RingCon.ringConGen_mono
theorem RingCon.ringConGen_mono :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] {r s : R → R → Prop},
(∀ (x y : R), r x y → s x y) → ringConGen r ≤ ringConGen s
This theorem states that for any given type `R` equipped with addition and multiplication operations, and any two binary relations `r` and `s` on `R` such that `r` is a subset of `s`, the smallest congruence relation that contains `s` also contains the smallest congruence relation that contains `r`. In other words, if a relation `r` is included in a relation `s`, then the smallest ring congruence containing `r` is also included in the smallest ring congruence containing `s`. This is a monotonicity property of the function that associates to each binary relation the smallest ring congruence containing that relation.
More concisely: If `r` is a subset of `s` and `[r]` and `[s]` are the respective smallest ring congruences containing `r` and `s` on a type `R` with addition and multiplication operations, then `[r]` is a subset of `[s]`.
|
RingCon.ext
theorem RingCon.ext :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] {c d : RingCon R}, (∀ (x y : R), c x y ↔ d x y) → c = d
This theorem is about the extensionality rule for congruence relations in the context of rings. Specifically, it states that given any type `R` that is equipped with addition and multiplication (i.e., a ring), if we have two congruence relations `c` and `d` on `R` such that for every pair of elements `x` and `y` from `R`, `x` is related to `y` under `c` if and only if `x` is related to `y` under `d`, then `c` and `d` are in fact the same congruence relation.
More concisely: If two congruence relations on a ring have the same equivalence classes for every pair of elements, then they are equal.
|
RingCon.sup_def
theorem RingCon.sup_def :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] {c d : RingCon R}, c ⊔ d = ringConGen (⇑c ⊔ ⇑d)
The theorem `RingCon.sup_def` states that for any type `R` equipped with addition and multiplication, and for any two ring congruence relations `c` and `d` on `R`, the supremum (or join) of `c` and `d` is equal to the smallest ring congruence relation that contains the supremum of the underlying binary operations of `c` and `d`. In other words, the most encompassing congruence relation between `c` and `d` is precisely the smallest congruence relation that includes both of the binary operations present in `c` and `d`.
More concisely: The supremum of ring congruences `c` and `d` on a ring `R` is equal to the smallest ring congruence containing the join of `c` and `d`'s underlying binary operations.
|
RingCon.add
theorem RingCon.add :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] (c : RingCon R) {w x y z : R}, c w x → c y z → c (w + y) (x + z)
This theorem, `RingCon.add`, states that for any ring `R` (signified by addition `Add` and multiplication `Mul` operations), and for any congruence relation `c` on `R`, if `c` relates `w` to `x` and `y` to `z`, then `c` also relates `(w + y)` to `(x + z)`. In other words, this congruence relation is preserved under the addition operation in the ring.
More concisely: If `R` is a ring, `c` is a congruence relation on `R`, and `w ~ c x` and `y ~ c z`, then `w + y ~ c (x + z)`.
|
RingCon.coe_sInf
theorem RingCon.coe_sInf :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] (S : Set (RingCon R)), ⇑(sInf S) = sInf (DFunLike.coe '' S) := by
sorry
This theorem states that for any given set `S` of ring congruence relations over a type `R` equipped with addition (`Add`) and multiplication (`Mul`), the infimum (or greatest lower bound) of `S` is equal to the infimum of the image of `S` under the functional mapping of its underlying binary relation. In other words, applying the infimum operator to the set of congruences and then converting to the binary relation gives the same result as first mapping each congruence to its binary relation and then finding the infimum.
More concisely: For any set of ring congruence relations over a type equipped with addition and multiplication, the infimum of the set is equal to the infimum of their underlying binary relations.
|
RingCon.sup_eq_ringConGen
theorem RingCon.sup_eq_ringConGen :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] (c d : RingCon R), c ⊔ d = ringConGen fun x y => c x y ∨ d x y
The theorem `RingCon.sup_eq_ringConGen` states that for any type `R` equipped with addition and multiplication operations, and any two ring congruence relations `c` and `d` on `R`, the supremum of `c` and `d` is equivalent to the smallest ring congruence relation that contains the binary relation where `x` is related to `y` if and only if `x` is related to `y` by `c` or `d`. Essentially, this means that the largest congruence relation that `c` and `d` can both fit into is the one generated by the union of their individual relations.
More concisely: The supremum of two ring congruence relations on a ring is the smallest ring congruence relation containing their union.
|
RingCon.add'
theorem RingCon.add' :
∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (self : RingCon R) {w x y z : R},
Setoid.r w x → Setoid.r y z → Setoid.r (w + y) (x + z)
This theorem states that for any type `R` equipped with operations of addition and multiplication, if `R` is also equipped with a RingCon (Ring congruence), then the equivalence relation defined by the Ring congruence is preserved under addition. Specifically, if `w` is equivalent to `x` and `y` is equivalent to `z` (in the sense defined by the Ring congruence), then the sum of `w` and `y` is equivalent to the sum of `x` and `z`. This is a formal way of saying that the additive structure of `R` respects the equivalence relation imposed by the Ring congruence.
More concisely: If `R` is a ring with additive congruence `RC`, then for all `x ≡ w` and `y ≡ z` in `R`, we have `x + y ≡ w + z`.
|
RingCon.symm
theorem RingCon.symm : ∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] (c : RingCon R) {x y : R}, c x y → c y x := by
sorry
This theorem, `RingCon.symm`, asserts that for any type `R` that has addition (Add) and multiplication (Mul) defined, given a relation `c` that's a congruence on the ring `R`, and any two elements `x` and `y` of `R`, if `x` is related to `y` under `c`, then `y` is also related to `x` under `c`. In other words, the congruence relation `c` is symmetric.
More concisely: If `c` is a congruence relation on a ring `R` with addition and multiplication, then for all `x` and `y` in `R`, if `x ≡ y (mod c)`, then `y ≡ x (mod c)`.
|
RingCon.sSup_eq_ringConGen
theorem RingCon.sSup_eq_ringConGen :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] (S : Set (RingCon R)),
sSup S = ringConGen fun x y => ∃ c ∈ S, c x y
The theorem `RingCon.sSup_eq_ringConGen` states that for any type `R` equipped with addition and multiplication, and for any set `S` of congruence relations on `R`, the supremum of `S` is equivalent to the smallest congruence relation that contains the binary relation 'there exists a congruence `c` in `S` such that `x` is related to `y` by `c`'. In other words, the supremum of a set of congruence relations is the smallest congruence relation that bundles all the relations in the set.
More concisely: The supremum of a set of congruence relations on a ring is the smallest congruence relation containing the relation "there exists a congruence in the set that relates x to y".
|
RingCon.sSup_def
theorem RingCon.sSup_def :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] {S : Set (RingCon R)},
sSup S = ringConGen (sSup (DFunLike.coe '' S))
The theorem `RingCon.sSup_def` states that for any type `R` with addition and multiplication operations, and any set `S` of ring congruence relations on `R`, the supremum of the set `S` is equal to the smallest ring congruence relation that includes the supremum of the images of the set `S` under the map to their underlying binary relations, where the map is defined using the function coercion `DFunLike.coe`. In simpler terms, it says that the "largest" congruence relation in a set is the same as the "smallest" congruence relation that contains all the relations in the set when considered as binary relations.
More concisely: The supremum of a set of ring congruence relations on a ring is equal to the binary relation that is the smallest congruence relation containing the images of all relations in the set under the function coercion.
|
RingCon.inf_iff_and
theorem RingCon.inf_iff_and :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] {c d : RingCon R} {x y : R}, (c ⊓ d) x y ↔ c x y ∧ d x y := by
sorry
The theorem `RingCon.inf_iff_and` asserts that for any type `R` equipped with addition and multiplication, and for any two congruence relations `c` and `d` on `R`, the infimum (greatest lower bound) of `c` and `d` applied on any two elements `x` and `y` of `R` is equivalent to the conjunction (logical "and") of `c` applied on `x` and `y` and `d` applied on `x` and `y`. That is, `x` and `y` are related by the infimum of `c` and `d` if and only if `x` and `y` are related by both `c` and `d`.
More concisely: For any commutative additive semigroup (R, +) with an associative multiplication and any congruence relations c and d on R, the inf inf{x, y ∈ R : x ≡ c(x, y) ∧ y ≡ d(x, y)} = c ∧ d.
|
RingCon.mul
theorem RingCon.mul :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] (c : RingCon R) {w x y z : R}, c w x → c y z → c (w * y) (x * z)
The theorem `RingCon.mul` states that for any type `R` that has addition and multiplication operations, given a structure `c` of type `RingCon R` and elements `w`, `x`, `y`, and `z` of `R`, if `c` relates `w` to `x` and `y` to `z`, then `c` must also relate the product of `w` and `y` to the product of `x` and `z`. In other words, it guarantees the compatibility of the relation `c` with the ring multiplication operation in this context.
More concisely: For any commutative ring `R` and `RingCon` structure `c` on `R`, if `c` relates `w` to `x` and `y` to `z`, then `c` relates `w * y` to `x * z`.
|
RingCon.sInf_toSetoid
theorem RingCon.sInf_toSetoid :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] (S : Set (RingCon R)),
(sInf S).toSetoid = sInf ((fun x => x.toSetoid) '' S)
This theorem states that for any set `S` of ring congruences on a type `R` (which is equipped with addition and multiplication), the infimum (greatest lower bound) of `S` converted to a setoid (an equivalence relation) is the same as the infimum of the images of the elements of `S` under the function that converts a ring congruence to a setoid. In other words, you get the same result whether you first find the infimum of the ring congruences and then convert to a setoid, or first convert each ring congruence to a setoid and then find the infimum.
More concisely: The infimum of a set of ring congruences on a ring and the infimum of their corresponding setoids are equal.
|
RingCon.trans
theorem RingCon.trans :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] (c : RingCon R) {x y z : R}, c x y → c y z → c x z
This theorem states that for any type `R` that has addition and multiplication operations (i.e., `R` is a ring), and any ring congruence relation `c` on `R`, if `x`, `y`, and `z` are elements of `R` such that `x` is related to `y` by `c` and `y` is related to `z` by `c`, then `x` is also related to `z` by `c`. In other words, the given ring congruence relation `c` is transitive.
More concisely: If `R` is a ring, and `c` is a ring congruence relation on `R`, then for all `x`, `y`, and `z` in `R` with `x ≡ y (mod c)` and `y ≡ z (mod c)`, it follows that `x ≡ z (mod c)`.
|
RingCon.ringConGen_idem
theorem RingCon.ringConGen_idem :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] (r : R → R → Prop), ringConGen ⇑(ringConGen r) = ringConGen r := by
sorry
This theorem states that for any binary relation `r` on a type `R` that is equipped with addition and multiplication, if we first generate the smallest ring congruence relation containing `r` (with `ringConGen r`), and then repeat this process on the outcome, the result is the same as if we had only applied `ringConGen` once. In other words, applying the operation of "generating the smallest ring congruence relation containing a given binary relation" twice in succession is the same as applying it once; hence, this operation is idempotent.
More concisely: The operation of generating the smallest ring congruence relation containing a binary relation is idempotent.
|
RingCon.coe_inf
theorem RingCon.coe_inf : ∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] {c d : RingCon R}, ⇑(c ⊓ d) = ⇑c ⊓ ⇑d := by
sorry
This theorem states that for any given type `R` equipped with addition and multiplication, and for any two congruence relations `c` and `d` on `R`, the infimum (greatest lower bound) of these two congruence relations is equal to the infimum of the underlying binary operations associated with `c` and `d`. In simpler terms, this theorem describes a property of the structure of these congruence relations, specifically focused on how the "minimum" or "lowest" relation is determined.
More concisely: Given types `R` with addition and multiplication, and congruence relations `c` and `d` on `R`, the infimum of congruences `c` and `d` equals the infimum of their associated binary operations.
|
RingCon.ringConGen_of_ringCon
theorem RingCon.ringConGen_of_ringCon :
∀ {R : Type u_2} [inst : Add R] [inst_1 : Mul R] (c : RingCon R), ringConGen ⇑c = c
This theorem states that for any given ring `R` with addition and multiplication operations, and a given congruence relation `c` on `R`, the smallest congruence relation containing `c` (generated by the function `ringConGen`) is equal to `c` itself. In other words, the congruence relation `c` is equivalent to the smallest congruence relation that includes it.
More concisely: For any ring `R` and congruence relation `c` on `R`, `c` is equal to the smallest congruence relation containing `c` (generated by `ringConGen`).
|