Con.conGen_idem
theorem Con.conGen_idem : ∀ {M : Type u_1} [inst : Mul M] (r : M → M → Prop), conGen ⇑(conGen r) = conGen r
This theorem states that for any type `M` equipped with a multiplication operation and any binary relation `r` on `M`, applying the operation `conGen` twice to `r` is the same as applying it once. In other words, the process of finding the smallest multiplicative congruence relation containing `r` is idempotent: once you've found this smallest relation, doing the process again doesn't change anything.
More concisely: For any type `M` with multiplication and any binary relation `r` on `M`, the reflexive and transitive closure of `r` and the reflexive and transitive closure of the relation obtained by applying the multiplicative congruence `conGen` to `r`, are equal.
|
AddCon.ext'
theorem AddCon.ext' : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M}, ⇑c = ⇑d → c = d
This theorem states that in a given type 'M' equipped with an addition operation, if we have two additive congruence relations 'c' and 'd', and their underlying binary relations are equal (denoted by `⇑c = ⇑d`), then the congruence relations 'c' and 'd' themselves are also equal (`c = d`). In other words, the map that sends an additive congruence relation to its corresponding binary relation is injective, meaning it preserves distinctness: distinct congruence relations map to distinct binary relations.
More concisely: If two additive congruence relations on a type 'M' have equal underlying binary relations, then they are equal as additive congruence relations.
|
AddCon.eq
theorem AddCon.eq : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M) {a b : M}, ↑a = ↑b ↔ c a b
This theorem states that for any type `M` with addition (`Add M`), and any additive congruence relation `c` on `M`, two elements `a` and `b` of `M` are related by `c` if and only if their representatives (obtained via the quotient map) in the quotient of `M` by `c` are the same. In the language of Mathematics, this is expressing the fundamental property of quotient structures in the context of additive groups: two elements are in the same equivalence class, i.e., related by the congruence, if and only if their images under the canonical projection to the quotient group are the same.
More concisely: For any additive group `(M, +)` and additive congruence relation `c` on `M`, elements `a` and `b` are related by `c` if and only if their quotient group representatives are equal.
|
AddCon.coe_add
theorem AddCon.coe_add : ∀ {M : Type u_1} [inst : Add M] {c : AddCon M} (x y : M), ↑(x + y) = ↑x + ↑y
This theorem states that for any type `M` equipped with an addition operation and any additive congruence relation `c` on `M`, the mapping that sends elements to their equivalence classes in the quotient structure commutes with the addition operation. In other words, for any two elements `x` and `y` of `M`, the equivalence class of the sum `x + y` is the same as the sum of the equivalence classes of `x` and `y`.
More concisely: For any additive type `M` and additive congruence relation `c` on `M`, the operation of adding equivalence classes equals the equivalence class of the sum of their representatives.
|
AddCon.inf_iff_and
theorem AddCon.inf_iff_and : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M} {x y : M}, (c ⊓ d) x y ↔ c x y ∧ d x y
This theorem states that for any Type "M" that supports addition operation, and for any two additive congruence relations "c" and "d" defined on "M", and for any two elements "x" and "y" of "M", the infimum (or greatest lower bound) of the congruence relations "c" and "d" applied to "x" and "y" is equivalent to the logical conjunction (i.e., the 'and' relation) of "c" applied to "x" and "y" and "d" applied to "x" and "y".
More concisely: For any Type M with addition and congruence relations c and d, the inf inf{c(x, y), d(x, y)} = c(x, y) ∧ d(x, y).
|
AddCon.mapOfSurjective_eq_mapGen
theorem AddCon.mapOfSurjective_eq_mapGen :
∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {c : AddCon M} {f : M → N}
(H : ∀ (x y : M), f (x + y) = f x + f y) (h : AddCon.addKer f H ≤ c) (hf : Function.Surjective f),
c.mapGen f = c.mapOfSurjective f H h hf
This theorem states that for any types `M` and `N` with addition (`Add M` and `Add N`), given an additive congruence relation `c` on `M`, a function `f` from `M` to `N` that preserves addition (`f (x + y) = f x + f y`), and such that the kernel of `f` is a subset of `c` (i.e., `AddCon.addKer f H ≤ c`), if `f` is also surjective, then the smallest additive congruence relation containing the image of `c` under `f` is equal to the image of `c` under `f` when `f` is surjective. In other words, every element in `N` can be obtained from `f` applied to some element in `M`, and the smallest congruence relation in `N` including the image of `c` is exactly the image of `c`.
More concisely: If `f` is a surjective additive function from type `M` with additive congruence relation `c` to type `N`, then the smallest additive congruence relation containing the image of `c` under `f` is equal to the image of `c` itself.
|
AddCon.induction_on
theorem AddCon.induction_on :
∀ {M : Type u_1} [inst : Add M] {c : AddCon M} {C : c.Quotient → Prop} (q : c.Quotient), (∀ (x : M), C ↑x) → C q
The theorem `AddCon.induction_on` states the inductive principle used for proving propositions about elements of a quotient type formed by an additive congruence relation. In more detailed terms, for any type `M` with an additive structure, an additive congruence relation `c` on `M`, a proposition `C` about elements of the quotient type of `M` by the congruence relation `c`, and an element `q` of that quotient type, if the proposition `C` holds for all representatives `x` of `M`, then the proposition `C` also holds for `q`.
More concisely: If `C` is a proposition about elements of the quotient type of an additive type `M` by an additive congruence relation `c`, and `C` holds for all representatives of equivalence classes, then `C` holds for any equivalence class itself.
|
Con.coe_sInf
theorem Con.coe_sInf : ∀ {M : Type u_1} [inst : Mul M] (S : Set (Con M)), ⇑(sInf S) = sInf (DFunLike.coe '' S) := by
sorry
This theorem states that for any type `M` endowed with a multiplication operation and a set `S` of congruence relations on `M`, the infimum (greatest lower bound) of this set of congruences is equal to the infimum of the image of this set under the mapping to its underlying binary relation. In other words, when we take the infimum of a set of congruences in terms of their binary relations, we obtain the same result as if we had taken the infimum of the congruences themselves.
More concisely: Let `M` be a type with multiplication and `S` a set of congruences on `M`. The infimum of `S` equals the infimum of the images of congruences in `S` under the mapping to their binary relations.
|
Con.lift_apply_mk'
theorem Con.lift_apply_mk' :
∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} (f : c.Quotient →* P),
c.lift (f.comp c.mk') ⋯ = f
This theorem states that given a homomorphism `f` from the quotient of a monoid `M` by a congruence relation `c` to another monoid `P`, the homomorphism induced by `f` composed with the natural map from `M` to its quotient, denoted by `c.lift (f.comp c.mk')`, is equivalent to `f` itself. In other words, applying the lifting process with the composition of `f` and `c.mk'` effectively retrieves the original homomorphism `f`. This property is fundamental to the structure of quotient spaces in the context of monoids.
More concisely: The natural map from a monoid `M` to its quotient by a congruence relation `c`, composed with a homomorphism `f` from the quotient to another monoid `P`, is equal to the homomorphism `f` itself when restricted to the quotient.
|
AddCon.nsmul
theorem AddCon.nsmul :
∀ {M : Type u_4} [inst : AddMonoid M] (c : AddCon M) (n : ℕ) {w x : M}, c w x → c (n • w) (n • x)
This theorem states that additive congruence relations preserve natural scaling for any type 'M' that forms an additive monoid. More specifically, given an additive congruence relation 'c' on 'M', any natural number 'n', and any two elements 'w' and 'x' from 'M' that are related by 'c', the 'n'-fold scalar multiples of 'w' and 'x' are also related by 'c'. In other words, if 'w' and 'x' are congruent under 'c', then so are their 'n'-fold scaled versions.
More concisely: Given an additive monoid 'M' and an additive congruence relation 'c' on 'M', if 'w' is congruent to 'x' under 'c', then for any natural number 'n', 'n'*'w' is congruent to 'n'*'x' under 'c'.
|
AddCon.sub
theorem AddCon.sub :
∀ {M : Type u_1} [inst : AddGroup M] (c : AddCon M) {w x y z : M}, c w x → c y z → c (w - y) (x - z)
This theorem states that for any type `M` equipped with an additive group structure, if `c` is an additive congruence relation on `M`, then `c` preserves subtraction. Specifically, if `w` is congruent to `x` and `y` is congruent to `z` under `c`, then `w - y` is congruent to `x - z` under the same congruence relation.
More concisely: For any additive group `M` and additive congruence relation `c` on `M`, if `w ≡x` and `y ≡ z` under `c`, then `w - y ≡ x - z`.
|
Con.conGen_mono
theorem Con.conGen_mono :
∀ {M : Type u_1} [inst : Mul M] {r s : M → M → Prop}, (∀ (x y : M), r x y → s x y) → conGen r ≤ conGen s
The theorem `Con.conGen_mono` states that for any type `M` that supports multiplication and any two binary relations `r` and `s` over `M`, if `r` is a subset of `s` (i.e., whenever `r x y` holds, `s x y` also holds), then the smallest congruence relation that contains `r` is a subset of the smallest congruence relation that contains `s`. In other words, if one relation is contained in another, their generated congruence relations preserve this containment.
More concisely: If relation `r` is a subset of relation `s` over type `M` with multiplication, then the smallest congruence relation containing `r` is contained in the smallest congruence relation containing `s`.
|
AddCon.addConGen_mono
theorem AddCon.addConGen_mono :
∀ {M : Type u_1} [inst : Add M] {r s : M → M → Prop}, (∀ (x y : M), r x y → s x y) → addConGen r ≤ addConGen s := by
sorry
This theorem states that for any type `M` equipped with an addition operation and any two binary relations `r` and `s` on `M`, if `r` is a subset of `s` (i.e., for all `x` and `y` in `M`, whenever `r x y` holds then `s x y` also holds), then the smallest additive congruence relation that contains `r` is also a subset of the smallest additive congruence relation that contains `s`. This is essentially about the monotonicity of the function `addConGen` that generates the smallest additive congruence relation from a given binary relation.
More concisely: If relation `r` is a subset of relation `s` on a type `M` equipped with addition, then the smallest additive congruence relation containing `r` is included in the smallest additive congruence relation containing `s`.
|
Con.lift_comp_mk'
theorem Con.lift_comp_mk' :
∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} {f : M →* P}
(H : c ≤ Con.ker f), (c.lift f H).comp c.mk' = f
The theorem `Con.lift_comp_mk'` states that for any types `M` and `P` that satisfy the structure `MulOneClass` (meaning they are monoids), given a congruence relation `c` on `M` and a monoid homomorphism `f` from `M` to `P` such that `c` is contained in the kernel of `f`, the composite of the lift of `f` along `c` and the canonical projection `c.mk'` is equal to `f`. This expresses the universal property for quotients of monoids: any homomorphism defined on `M` which is constant on `c`-related pairs factors uniquely through the quotient monoid `M/c`.
More concisely: Given a monoid homomorphism `f` from `M` to `P` with kernel containing congruence relation `c` on `M`, the canonical projection `c.mk'` and the lift of `f` along `c` commute, i.e., `c.mk' ∘ f.lift c = f`.
|
Con.coe_mul
theorem Con.coe_mul : ∀ {M : Type u_1} [inst : Mul M] {c : Con M} (x y : M), ↑(x * y) = ↑x * ↑y
This theorem states that for any type `M` that is equipped with a multiplication operation, and for any congruence relation `c` on `M`, the coercion to the quotient of the congruence relation commutes with the multiplication operation. Specifically, if `x` and `y` are elements of `M`, then the equivalence class of the product `x * y` (denoted by `↑(x * y)`) is equal to the product of the equivalence classes of `x` and `y` (denoted by `↑x * ↑y`). The theorem assumes that the multiplication operation on `M` is compatible with the congruence relation `c`, as required by the definition of congruence relation.
More concisely: For any type `M` with a multiplication operation and congruence relation `c`, if `x` and `y` are elements of `M` such that `c` is compatible with multiplication, then `↑(x * y) = ↑x * ↑y`.
|
AddCon.mk'_surjective
theorem AddCon.mk'_surjective : ∀ {M : Type u_1} [inst : AddZeroClass M] {c : AddCon M}, Function.Surjective ⇑c.mk'
The theorem `AddCon.mk'_surjective` states that for any type `M` that has an `AddZeroClass` instance (which means `M` is an additive monoid), and any additive congruence relation `c` on `M`, the natural homomorphism from `M` to its quotient by `c` (denoted as `⇑c.mk'`) is surjective. In mathematical terms, this means that for every element in the quotient set, there exists an element in the original set `M` such that applying the homomorphism to this element yields the element in the quotient set.
More concisely: For any additive monoid `M` and additive congruence relation `c` on `M`, the natural homomorphism from `M` to the quotient by `c` is surjective.
|
AddCon.coe_zero
theorem AddCon.coe_zero : ∀ {M : Type u_1} [inst : AddZeroClass M] {c : AddCon M}, ↑0 = 0
This theorem states that for any type `M` with instance structure of an additive monoid with zero (`AddZeroClass M`), and any additive congruence relation `c` on `M`, the equivalence class of the monoid's zero element under this relation (denoted by `↑0`) is equal to the zero element of the quotient monoid (denoted by `0`). This means the zero value of the quotient structure is the equivalence class that contains the original zero value from `M`.
More concisely: For any additive monoid `M` with zero `0` and additive congruence relation `c`, the equivalence class of `0` under `c` is the zero element in the quotient monoid.
|
Con.trans
theorem Con.trans : ∀ {M : Type u_1} [inst : Mul M] (c : Con M) {x y z : M}, c x y → c y z → c x z
This theorem states that congruence relations are transitive in the context of an arbitrary type `M` equipped with a multiplication operation. In other words, for any type `M` and a congruence relation `c` on `M`, if `x`, `y`, and `z` are elements of `M` such that `x` is congruent to `y` and `y` is congruent to `z` under the relation `c`, then `x` is also congruent to `z` under the same relation. This is a key property of equivalence relations, of which congruence is a specific type that respects a given algebraic operation (in this case, multiplication).
More concisely: If `c` is a congruence relation on a type `M` with multiplication, then `x` is congruent to `z` under `c` whenever `x` is congruent to `y` under `c` and `y` is congruent to `z` under `c`.
|
Con.symm
theorem Con.symm : ∀ {M : Type u_1} [inst : Mul M] (c : Con M) {x y : M}, c x y → c y x
This theorem states that congruence relations are symmetric in the context of a multiplication operation on a type `M`. Specifically, for any type `M` with a multiplication operation, and for any congruence relation `c` on `M`, if `x` and `y` are elements of `M` such that `x` is congruent to `y` under the relation `c`, then `y` is also congruent to `x` under the same relation. In other words, if `c x y` is true, then `c y x` is also true, confirming the symmetry of the congruence relation.
More concisely: If `x` is congruent to `y` under a congruence relation `c` on a type `M` with multiplication operation, then `y` is congruent to `x` under the same relation. (i.e., `c x y` implies `c y x`)
|
Con.mk'_ker
theorem Con.mk'_ker : ∀ {M : Type u_1} [inst : MulOneClass M] (c : Con M), Con.ker c.mk' = c
This theorem states that the kernel of the natural homomorphism from a monoid to its quotient by a congruence relation 'c' is equal to 'c' itself. In other words, if we have a monoid 'M' and a congruence relation 'c' on 'M', then the kernel of the homomorphism that sends each element of 'M' to its equivalence class in the quotient monoid 'M/c' is precisely 'c'. In algebraic terms, this formalizes the idea that a congruence relation on a monoid corresponds to an equivalence relation on the set of elements that are mapped to the identity by the homomorphism.
More concisely: The kernel of the natural homomorphism from a monoid to its quotient by a congruence relation equals the congruence relation itself.
|
AddCon.refl
theorem AddCon.refl : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M) (x : M), c x x
This theorem states that additive congruence relations are reflexive for any type `M` with the addition operation. In other words, for any given type `M`, a specified additive congruence relation `c` on `M`, and an element `x` of type `M`, `x` is always congruent to itself under the relation `c`. This is a property of reflexive relations, which assert, in this case, that any element in an additive structure is congruent to itself.
More concisely: For any additive type M and congruence relation c on M, x ≡x (mod c) holds for all x in M. (Here, ≡ denotes congruence relation.)
|
Con.coe_inf
theorem Con.coe_inf : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M}, ⇑(c ⊓ d) = ⇑c ⊓ ⇑d
This theorem states that for any multiplication type `M` and any two congruence relations `c` and `d` on `M`, the infimum (or greatest lower bound) of the two congruence relations is equal to the infimum of the underlying binary operations of the two congruence relations. In other words, the application of the infimum to the congruence relations is the same as the application of the infimum to the corresponding binary operations. This establishes a crucial relationship between the structure of congruence relations and their corresponding binary operations in the context of multiplication types.
More concisely: For any multiplication type `M` and congruence relations `c` and `d` on `M`, the infimum of `c` and `d` equals the infimum of their underlying binary operations.
|
AddCon.addConGen_idem
theorem AddCon.addConGen_idem :
∀ {M : Type u_1} [inst : Add M] (r : M → M → Prop), addConGen ⇑(addConGen r) = addConGen r
This theorem states that for any type `M` that has an addition operation and any binary relation `r` on `M`, applying the function `addConGen` twice to `r` yields the same result as applying it once. In other words, the function `addConGen`, which maps a binary relation to the smallest additive congruence relation containing it, is idempotent. The idempotency means that once a binary relation is extended to an additive congruence relation, further attempts to extend it in the same manner do not change it.
More concisely: For any type `M` with addition and any binary relation `r` on `M`, the application of `addConGen` to `r` twice equals its application once. (i.e., `addConGen` is an idempotent function for binary relations on `M` with respect to addition.)
|
Con.sSup_def
theorem Con.sSup_def : ∀ {M : Type u_1} [inst : Mul M] {S : Set (Con M)}, sSup S = conGen (sSup (DFunLike.coe '' S))
This theorem states that for any set `S` of congruence relations over a type `M` equipped with a multiplication operation, the supremum of `S` is the same as the smallest congruence relation that contains the supremum of the set's image under the map from the congruence relations to their underlying binary relations. In essence, it shows a correspondence between the supremum of congruence relations and the supremum of their underlying binary relations, as mapped by a function.
More concisely: The supremum of a set of congruence relations over a type with multiplication is equal to the congruence relation containing the supremum of their image under the function mapping congruences to their binary relations.
|
Con.conGen_of_con
theorem Con.conGen_of_con : ∀ {M : Type u_1} [inst : Mul M] (c : Con M), conGen ⇑c = c
This theorem states that for a given type `M` equipped with a multiplication operation, and a given congruence relation `c` on `M`, the smallest multiplicative congruence relation that contains `c` is `c` itself. In other words, any congruence relation on `M` is equal to the smallest congruence relation in which it is contained. This is a property of the `conGen` function, which generates the smallest congruence relation containing a given binary relation.
More concisely: For any type `M` with a multiplication operation and a congruence relation `c` on `M`, the relation `c` is the smallest multiplicative congruence relation containing it.
|
Con.coe_inj
theorem Con.coe_inj : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M}, ⇑c = ⇑d ↔ c = d
This theorem states that for any type `M` with a multiplication operation, two congruence relations `c` and `d` on `M` are equal if and only if their underlying binary relations are equal. In other words, comparing the function applications of `c` and `d` is the same as directly comparing `c` and `d`.
More concisely: For any type `M` with a multiplication operation, two congruence relations `c` and `d` on `M` are equal if and only if their underlying binary relations are equal: `c = d <-> ∀ x y, x Rc y ↔ x Rd y`, where `Rc` and `Rd` are the reflexive and transitive closures of `c` and `d`, respectively.
|
AddCon.liftOn_coe
theorem AddCon.liftOn_coe :
∀ {M : Type u_1} [inst : Add M] {β : Sort u_4} (c : AddCon M) (f : M → β) (h : ∀ (a b : M), c a b → f a = f b)
(x : M), AddCon.liftOn (↑x) f h = f x
This theorem describes the functionality of the `AddCon.liftOn` operation on an element of type `M` in the context of an additive congruence relation `c`. In particular, if we have an instance of additive structure `Add M` on type `M`, a function `f` from `M` to some arbitrary type `β`, and a proof `h` that `f` is constant on the equivalence classes induced by `c`, then for any `x` of type `M`, applying `AddCon.liftOn` to the equivalence class of `x` (denoted by `↑x`), `f`, and `h` yields the same result as just applying `f` to `x`. This theorem encapsulates the idea that `AddCon.liftOn` behaves as expected when applied to elements of the original type `M` rather than to their equivalence classes under `c`.
More concisely: Given an additive congruence relation `c` on an additive type `M`, a constant function `f` on `M`'s equivalence classes induced by `c`, and an element `x` of `M`, `AddCon.liftOn (↑x) f h = f x`, where `h` is a proof of `f`'s constancy.
|
AddCon.comap_eq
theorem AddCon.comap_eq :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {c : AddCon M} {f : N →+ M},
AddCon.comap ⇑f ⋯ c = AddCon.ker (c.mk'.comp f)
This theorem states that for any `AddMonoid` homomorphism `f` mapping from type `N` to type `M`, and any additive congruence relation `c` defined on type `M`, the additive congruence relation that `f` induces on its domain `N`, is equal to the kernel of the composition of `c`'s quotient homomorphism and `f`. That is, two elements in `N` are equivalent under this induced relation if and only if their images under `f` are equivalent under `c`, and this equivalence relation coincides with the kernel of the composition of the quotient homomorphism induced by `c` and the original homomorphism `f`.
More concisely: The induced additive congruence relation on the domain of an AddMonoid homomorphism is equal to the kernel of the composition of the quotient homomorphism induced by the relation and the original homomorphism.
|
Con.mul
theorem Con.mul : ∀ {M : Type u_1} [inst : Mul M] (c : Con M) {w x y z : M}, c w x → c y z → c (w * y) (x * z) := by
sorry
This theorem states that if we have a congruence relation `c` on a type `M` that has a multiplication operation, then the multiplication operation is preserved under this relation. Formally, if `w` is congruent to `x` and `y` is congruent to `z` under this relation, then the product `w * y` is congruent to `x * z`.
More concisely: If `c` is a congruence relation on type `M` with multiplication operation, then for all `w ≡x` and `y ≡ z` in `c`, we have `w * y ≡ x * z`.
|
AddCon.kerLift_mk
theorem AddCon.kerLift_mk :
∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {f : M →+ P} (x : M),
(AddCon.kerLift f) ↑x = f x
The theorem `AddCon.kerLift_mk` states that for any additive monoid homomorphism `f` from an additive monoid `M` to another additive monoid `P`, and for any element `x` of `M`, the homomorphism induced on the quotient of `M` by the kernel of `f` and applied to the equivalence class of `x` under this quotient, is equal to `f` applied directly to `x`. This means that the diagram described by the universal property for quotients of additive monoids, when the additive congruence relation is the kernel of the homomorphism, commutes.
More concisely: For any additive monoid homomorphism $f$ from an additive monoid $M$ to another additive monoid $P$ and any $x$ in $M$, $f(x) = (f(|M|)([x]_{ker(f)}))$, where $|M|$ denotes the additive monoid structure on $M$, $[x]_{ker(f)}$ is the equivalence class of $x$ under the kernel of $f$, and $f(|M|)$ is the homomorphism induced on the quotient of $M$ by the kernel of $f$.
|
AddCon.kerLift_range_eq
theorem AddCon.kerLift_range_eq :
∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {f : M →+ P},
AddMonoidHom.mrange (AddCon.kerLift f) = AddMonoidHom.mrange f
This theorem states that for any given additive monoid homomorphism `f` from a type `M` to a type `P` (where both `M` and `P` are instances of the `AddZeroClass`), the range of the homomorphism induced on the quotient by the kernel of `f` is the same as the range of `f` itself. In other words, the image of any element in the quotient monoid under the induced homomorphism is in the same submonoid of `P` as the image of that element under the original homomorphism `f`.
More concisely: The image of an additive monoid homomorphism is equal to the image of its restriction to the quotient by the kernel.
|
Con.induction_on₂
theorem Con.induction_on₂ :
∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {c : Con M} {d : Con N}
{C : c.Quotient → d.Quotient → Prop} (p : c.Quotient) (q : d.Quotient), (∀ (x : M) (y : N), C ↑x ↑y) → C p q
This theorem, named `Con.induction_on₂`, is a version of `Con.induction_on` designed for predicates that take two arguments. It takes types `M` and `N` with multiplication (`Mul`) structures, along with two congruence relations `c` on `M` and `d` on `N`, and a predicate `C` that operates on the quotient types of `c` and `d`. It asserts that if `C` holds for all pairs of representatives `(x, y)` from `M` and `N` respectively (where `x` and `y` are lifted to their respective quotients), then `C` also holds for any two such quotient elements `p` from `c.Quotient` and `q` from `d.Quotient`.
More concisely: Given types `M` and `N` with multiplication structures and congruence relations `c` on `M` and `d` on `N`, if a predicate `C` holds for all pairs of representatives `(x, y)` from `M` and `N` in their respective quotient types `c.Quotient` and `d.Quotient`, then `C` also holds for any two quotient elements `p` and `q` from `c.Quotient` and `d.Quotient`, respectively.
|
AddCon.sInf_toSetoid
theorem AddCon.sInf_toSetoid :
∀ {M : Type u_1} [inst : Add M] (S : Set (AddCon M)), (sInf S).toSetoid = sInf (AddCon.toSetoid '' S)
This theorem states that for any type 'M' equipped with an addition operation and a set 'S' of additive congruence relations over 'M', the infimum (greatest lower bound) of the set 'S' mapped to its underlying equivalence relations is the same as the infimum of the set 'S' itself. In other words, the order structure of the additive congruence relations is preserved under the mapping to their underlying equivalence relations.
More concisely: The infimum of a set of additive congruence relations on a type equipped with addition is equal to the infimum of their underlying equivalence relations.
|
AddCon.ker_rel
theorem AddCon.ker_rel :
∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] (f : M →+ P) {x y : M},
(AddCon.ker f) x y ↔ f x = f y
This theorem states that for any given types `M` and `P` that have an `AddZeroClass` structure (essentially, they are additive monoids with a zero element), and any additively homomorphic function `f` from `M` to `P`, elements `x` and `y` of `M` are related under the additive congruence relation defined by the kernel of `f` if and only if `f` of `x` is equal to `f` of `y`. This captures the intuitive notion that the kernel of a function consists of inputs that are mapped to the same output.
More concisely: For additive monoids `M` and `P` with zero elements, and additively homomorphic function `f` from `M` to `P`, the kernel of `f` is the equivalence relation on `M` such that `x ≈ y` if and only if `f(x) = f(y)`.
|
Con.lift_unique
theorem Con.lift_unique :
∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} {f : M →* P}
(H : c ≤ Con.ker f) (g : c.Quotient →* P), g.comp c.mk' = f → g = c.lift f H
This theorem, named `Con.lift_unique`, states the uniqueness part of the universal property for quotients of monoids. Given two types `M` and `P` that are both instances of a `MulOneClass` (essentially monoids), a congruence relation `c` on `M`, and a monoid homomorphism `f` from `M` to `P` such that `c` is less than or equal to the kernel of `f`, the theorem asserts that for any monoid homomorphism `g` from the quotient of `M` by `c` to `P` for which the composition of `g` and the quotient map from `M` to `M/c` is equal to `f`, `g` must be equal to the map obtained by 'lifting' `f` to the quotient `M/c`. In other words, in the category of monoids, the lift of a map under a quotient is unique.
More concisely: Given monoids M and P, a congruence relation c on M, a monoid homomorphism f : M -> P with kernel containing c, and a monoid homomorphism g : M/c -> P such that f = g ∘ q, where q is the quotient map from M to M/c, then g is equal to the unique lift of f to M/c.
|
Con.ker_eq_lift_of_injective
theorem Con.ker_eq_lift_of_injective :
∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] (c : Con M) (f : M →* P)
(H : c ≤ Con.ker f), Function.Injective ⇑(c.lift f H) → Con.ker f = c
This theorem states that for any monoid homomorphism `f` from a type `M` to another type `P` (both types having multiplication and one as operations), given a congruence relation `c` on `M` and the condition that `c` is less than or equal to the kernel of `f`, if the induced map from the quotient of `M` by `c` to `P` is an injective function (i.e., distinct elements in the domain map to distinct elements in the codomain), then the kernel of `f` is equivalent to the congruence relation `c`. Thus, in this context, the kernel of `f` can be seen as the "smallest" congruence relation whose induced map is injective.
More concisely: If `f` is a monoid homomorphism from `M` to `P`, `c` is a congruence relation on `M` with `c` included in the kernel of `f`, and the induced map from the quotient of `M` by `c` to `P` is injective, then the kernel of `f` is equivalent to `c`.
|
Con.mul_ker_mk_eq
theorem Con.mul_ker_mk_eq : ∀ {M : Type u_1} [inst : Mul M] (c : Con M), Con.mulKer Con.toQuotient ⋯ = c
This theorem states that, for any type `M` equipped with a multiplication operation and any congruence relation `c` on `M`, the kernel of the quotient map induced by the congruence relation `c` is equal to `c` itself. Here, the kernel of a multiplication-preserving function is defined as a congruence relation, and the quotient map is the morphism into the quotient by the given congruence relation.
More concisely: For any type `M` with multiplication and congruence relation `c`, the kernel of the quotient map induced by `c` equals `c`.
|
Con.inv
theorem Con.inv : ∀ {M : Type u_1} [inst : Group M] (c : Con M) {x y : M}, c x y → c x⁻¹ y⁻¹
This theorem states that in a group `M`, if two elements `x` and `y` are related by a multiplicative congruence relation `c`, then their inverses `x⁻¹` and `y⁻¹` are also related by the same congruence relation `c`. In other words, multiplicative congruence relations preserve the operation of taking inverses in the group.
More concisely: In a group M, if x ≡ y (mod c) is a multiplicative congruence relation, then x⁻¹ ≡ y⁻¹ (mod c).
|
AddCon.sup_def
theorem AddCon.sup_def : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M}, c ⊔ d = addConGen (⇑c ⊔ ⇑d)
The theorem `AddCon.sup_def` states that for any type `M` equipped with an addition operation, and for any two additive congruence relations `c` and `d` on `M`, the supremum (or join, essentially the least upper bound) of `c` and `d` is equal to the smallest additive congruence relation that contains the supremum of the binary operations underlying `c` and `d`. In simpler terms, it means that the smallest relation that includes both `c` and `d` is equivalent to the relation generated by combining the binary operations of `c` and `d`.
More concisely: The supremum of two additive congruence relations on a type equipped with an addition operation is the smallest additive congruence relation containing their underlying binary operations' supremum.
|
AddCon.ext
theorem AddCon.ext : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M}, (∀ (x y : M), c x y ↔ d x y) → c = d
This theorem is called the Extensionality rule for additive congruence relations. It states that for all types `M` with addition operation, and for any two additive congruence relations `c` and `d` on `M`, if for all elements `x` and `y` of `M`, `x` is related to `y` by `c` if and only if `x` is related to `y` by `d`, then `c` and `d` are the same relation. In mathematical terms, if two additive congruence relations define the same set of pairs `(x, y)`, then they are equal.
More concisely: If two additive congruence relations on a type with addition define the same equivalence classes, then they are equal.
|
AddCon.lift_funext
theorem AddCon.lift_funext :
∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M}
(f g : c.Quotient →+ P), (∀ (a : M), f ↑a = g ↑a) → f = g
This theorem states that for any additive monoid `M` and any type `P` equipped with the structure of an additive monoid, given an additive congruence relation `c` on `M`, if we have two additive homomorphisms `f` and `g` from the quotient of `M` by `c` to `P`, then `f` and `g` are equal if they map any element `a` of `M` (considered as an element of the quotient via coercion) to the same element in `P`. This theorem is essentially about the uniqueness of homomorphisms from the quotient of an additive monoid by an equivalence relation, in terms of their behavior on representatives of equivalence classes.
More concisely: Given an additive monoid `M` with an additive congruence relation `c`, any two additive homomorphisms from `M / c` to an additive monoid `P` that agree on the image of every element in `M` under the quotient map are equal.
|
Con.sup_eq_conGen
theorem Con.sup_eq_conGen : ∀ {M : Type u_1} [inst : Mul M] (c d : Con M), c ⊔ d = conGen fun x y => c x y ∨ d x y := by
sorry
The theorem `Con.sup_eq_conGen` states that, for any given type `M` that forms a multiplication structure, the supremum of any two congruence relations `c` and `d` on `M`, denoted by `c ⊔ d`, is equal to the smallest congruence relation that contains the binary relation "an element `x` is related to an element `y` by either `c` or `d`". Here, the smallest congruence relation containing a given binary relation is generated by the function `conGen`.
More concisely: For any type `M` with a multiplication structure and congruence relations `c` and `d` on `M`, `c ⊔ d` equals the congruence relation generated by `c ∪ d`.
|
AddCon.addConGen_le
theorem AddCon.addConGen_le :
∀ {M : Type u_1} [inst : Add M] {r : M → M → Prop} {c : AddCon M}, (∀ (x y : M), r x y → c x y) → addConGen r ≤ c
The theorem `AddCon.addConGen_le` states that for any type `M` equipped with an addition operation, given a binary relation `r` on `M` and an additive congruence relation `c` on `M`, if `c` contains `r` (i.e., for any two elements `x` and `y` of `M`, `r x y` implies `c x y`), then the smallest additive congruence relation containing `r` (denoted by `addConGen r`) is contained in `c`. In simpler terms, any additive congruence relation that contains `r` must also contain the smallest congruence relation that contains `r`.
More concisely: Given a type `M` with an addition operation, if a binary relation `r` on `M` is contained in an additive congruence relation `c` on `M`, then `addConGen r` (the smallest additive congruence relation containing `r`) is contained in `c`.
|
AddCon.map_apply
theorem AddCon.map_apply :
∀ {M : Type u_1} [inst : AddZeroClass M] {c d : AddCon M} (h : c ≤ d) (x : c.Quotient),
(c.map d h) x = (c.lift d.mk' ⋯) x
This theorem establishes a mapping in the context of additive congruence relations on an additive monoid. Given two additive congruence relations `c` and `d` on an `AddMonoid`, where `d` contains `c`, the theorem defines the homomorphism from the quotient by `c` to the quotient by `d` that is induced by `d`'s quotient map. In other words, for any element `x` of the quotient by `c`, the map from `c` to `d` applied to `x` is equal to the result of lifting `x` to `d` via `d`'s quotient map.
More concisely: Given additive congruence relations `c` and `d` on an additive monoid with `d` containing `c`, there exists a unique homomorphism from the quotient of the monoid by `c` to the quotient of the monoid by `d` such that the image of an element in the quotient by `c` under this homomorphism is equal to the image of that element under the quotient map from `c` to `d`.
|
AddCon.lift_coe
theorem AddCon.lift_coe :
∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M} {f : M →+ P}
(H : c ≤ AddCon.ker f) (x : M), (c.lift f H) ↑x = f x
This theorem states that for any function `f` from an additive monoid `M` to another additive monoid `P`, and for any additive congruence `c` on `M` such that `c` is a subset of the kernel of `f`, the universal property for quotients of additive monoids holds. Specifically, given any element `x` in `M`, applying the lift of `f` with respect to `c` to the equivalence class of `x` under `c` produces the same result as simply applying `f` to `x`. In other words, the diagram involving `M`, `P`, the quotient of `M` by `c`, and the functions `f` and `c.lift f H` commutes.
More concisely: For any additive monoid homomorphism $f$ from an additive monoid $M$ to an additive monoid $P$, and any additive congruence $c$ on $M$ contained in the kernel of $f$, the image of the equivalence class of any element $x$ in $M$ under $f$ is equal to the application of the lift of $f$ with respect to $c$ on that equivalence class.
|
Con.lift_mk'
theorem Con.lift_mk' :
∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} {f : M →* P}
(H : c ≤ Con.ker f) (x : M), (c.lift f H) (c.mk' x) = f x
The theorem `Con.lift_mk'` states the universal property for quotients of monoids. Specifically, for any given types `M` and `P` that have a multiplicative structure (denoted by `MulOneClass M` and `MulOneClass P`), given a congruence relation `c` on `M`, a monoid homomorphism `f` from `M` to `P`, and an element `x` of `M`, if `c` is a subrelation of the kernel of `f` (expressed as `c ≤ Con.ker f`), then applying the quotient map induced by `f` on the equivalence class of `x` under `c` (expressed as `(c.lift f H) (c.mk' x)`) yields the same result as directly applying `f` on `x`. In other words, the diagram involving original monoid, quotient monoid, and the target monoid, with maps being the original homomorphism and the induced homomorphism, commutes.
More concisely: Given a congruence relation `c` on a monoid `M`, a monoid homomorphism `f` from `M` to a monoid `P`, and an element `x` in `M` such that `c` is a subrelation of the kernel of `f`, the quotient map induced by `f` on the equivalence class of `x` under `c` equals directly applying `f` on `x`. (That is, the diagram commutes.)
|
Con.sInf_toSetoid
theorem Con.sInf_toSetoid :
∀ {M : Type u_1} [inst : Mul M] (S : Set (Con M)), (sInf S).toSetoid = sInf (Con.toSetoid '' S)
This theorem states that for any set of congruence relations on a type `M` endowed with a multiplication operation, the infimum of this set of congruence relations (viewed as a set of equivalence relations) is equal to the infimum of the set's image under the map that associates to each congruence relation its underlying equivalence relation. In other words, when considering the "lowest" or "most restrictive" congruence relation in the set, we get the same result whether we consider the congruence relations themselves or their underlying equivalence relations.
More concisely: The infimum of the set of congruence relations on a type endowed with multiplication equals the infimum of their underlying equivalence relations.
|
Con.ker_rel
theorem Con.ker_rel :
∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] (f : M →* P) {x y : M},
(Con.ker f) x y ↔ f x = f y
The theorem `Con.ker_rel` states that for any types `M` and `P` with instances of the `MulOneClass` (i.e., they are monoids), and for any monoid homomorphism `f` from `M` to `P`, the congruence relation `Con.ker f` holds between elements `x` and `y` of `M` if and only if `f(x)` equals `f(y)`. In other words, `x` and `y` are related under the kernel of `f` precisely when `f` maps `x` and `y` to the same element in `P`.
More concisely: For any monoid homomorphisms between monoids `M` and `P`, the kernel of `f` is the equivalence relation on `M` defined by `x ≡ y` if and only if `f(x) = f(y)`.
|
Con.toSetoid_inj
theorem Con.toSetoid_inj : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M}, c.toSetoid = d.toSetoid → c = d
This theorem states that the function that converts a congruence relation into its underlying equivalence relation, for a given type `M` equipped with a multiplication, is injective. In other words, if two congruence relations `c` and `d` on `M` produce the same equivalence relation when converted, then `c` and `d` must have been the same congruence relation to begin with.
More concisely: Given types equipped with multiplication and congruence relations on them, if two congruence relations have the same underlying equivalence relation, then they are equal as congruence relations.
|
AddCon.kerLift_injective
theorem AddCon.kerLift_injective :
∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] (f : M →+ P),
Function.Injective ⇑(AddCon.kerLift f)
The theorem `AddCon.kerLift_injective` states that for any `AddMonoid` homomorphism `f` from `M` to `P`, where `M` and `P` are types with addition and zero, the induced homomorphism on the quotient by the kernel of `f` is injective. In other words, if two elements in the quotient of `M` by the kernel of `f` map to the same element in `P` under the induced homomorphism, then those two elements were actually the same in the quotient. This means that the induced homomorphism does not collapse distinct elements in the quotient to the same element in `P`.
More concisely: Given an additive monoid homomorphism `f` from an additive monoid `M` to another additive monoid `P`, the induced homomorphism on the quotient by `f`'s kernel is injective.
|
Con.comap_eq
theorem Con.comap_eq :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {c : Con M} {f : N →* M},
Con.comap ⇑f ⋯ c = Con.ker (c.mk'.comp f)
Given a monoid homomorphism `f` from `N` to `M` and a congruence relation `c` on `M`, the theorem `Con.comap_eq` states that the congruence relation induced on `N` by `f` is equal to the kernel of the composition of the quotient homomorphism formed from `c` and `f`. In other words, if we consider any two elements in `N` to be related if their images under `f` are related under `c` in `M`, then this relation is the same as the relation defined by the kernel of the composed homomorphism.
More concisely: The congruence relation on `N` induced by a monoid homomorphism `f` from `N` to `M` is equal to the kernel of the composition of `f` with the quotient homomorphism formed from a congruence relation `c` on `M`.
|
Con.liftOn_coe
theorem Con.liftOn_coe :
∀ {M : Type u_1} [inst : Mul M] {β : Sort u_4} (c : Con M) (f : M → β) (h : ∀ (a b : M), c a b → f a = f b) (x : M),
Con.liftOn (↑x) f h = f x
The theorem `Con.liftOn_coe` states that for any type `M` with a multiplication operation, a congruence relation `c` on `M`, a function `f` from `M` to some other sort `β`, and a property `h` showing that `f` gives the same result for any two elements of `M` that are related by `c`, then the function `Con.liftOn` applied to the equivalence class of any element `x` of `M` under `c`, `f`, and `h` is equal to the value of `f` applied to `x`. In other words, the `Con.liftOn` function behaves the same way as `f` on individual elements of `M`.
More concisely: Given a type `M` with multiplication, a congruence relation `c` on `M`, a function `f` from `M` to some sort `β` satisfying `f (a) = f (b)` whenever `a` and `b` are related by `c`, the `Con.liftOn` function applied to the equivalence class of any element `x` under `c` equals `f(x)`.
|
AddCon.coe_inj
theorem AddCon.coe_inj : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M}, ⇑c = ⇑d ↔ c = d
This theorem states that for any type `M` with an additive structure, two additive congruence relations `c` and `d` are considered equal if and only if their underlying binary relations are equal. In other words, in the context of an additive structure on `M`, the equality of two additive congruence relations is determined by the equality of the binary relations that constitute them.
More concisely: For any additive type M, two additive congruence relations on M are equal if and only if their underlying binary relations are equal.
|
AddCon.zsmul
theorem AddCon.zsmul :
∀ {M : Type u_1} [inst : AddGroup M] (c : AddCon M) (n : ℤ) {w x : M}, c w x → c (n • w) (n • x)
This theorem states that for any additive congruence relation `c` on a type `M` that forms an additive group, the relation `c` is preserved under integer scaling. In more detail, if `w` and `x` are two elements of `M` such that `w` is related to `x` by the relation `c`, then the relation `c` also holds between `n` times `w` and `n` times `x` for any integer `n`. Here, `n • w` and `n • x` denote the operation of scaling `w` and `x` by the integer `n`.
More concisely: For any additive congruence relation `c` on an additive group `M`, if `w` is congruent to `x` modulo `c` (i.e., `w ≡ x (mod c)`), then `n • w` is congruent to `n • x` modulo `c` for any integer `n`.
|
AddCon.sSup_def
theorem AddCon.sSup_def :
∀ {M : Type u_1} [inst : Add M] {S : Set (AddCon M)}, sSup S = addConGen (sSup (DFunLike.coe '' S))
This theorem states that for a given type `M` equipped with an addition operation and a set `S` of additive congruence relations on `M`, the supremum of the set `S` is identical to the smallest additive congruence relation that contains the supremum of the image of `S` under the map to the underlying binary relation. In other words, determining the supremum of additive congruence relations is equivalent to generating the smallest additive congruence relation that encapsulates the supremum of the binary relations derived from the original set of congruence relations.
More concisely: The supremum of a set of additive congruence relations on a type `M` is equal to the smallest additive congruence relation containing the supremum of their images under the map to binary relations.
|
AddCon.map_of_add_left_rel_zero
theorem AddCon.map_of_add_left_rel_zero :
∀ {M : Type u_1} [inst : AddMonoid M] (c : AddCon M) (f : M → M),
(∀ (x : M), c (f x + x) 0) → ∀ {x y : M}, c x y → c (f x) (f y)
This theorem relates to the definition of an additive group in terms of a quotient of a monoid by an additive congruence relation. Sometimes, the inverse operation in such a group is defined as `Setoid.map f _` for some function `f`. In that context, this theorem provides a simplification, stating that to define the inverse operation and prove the group laws, one does not need to separately prove `∀ x y, c x y → c (f x) (f y)` (for defining the operation) and `∀ x, c (f x + x) 0` (for proving the group laws). Instead, it suffices to prove just the latter. Specifically, the theorem states that for any type `M` with the structure of an additive monoid, any additive congruence relation `c` on `M`, and any function `f` from `M` to `M`, if for all `x` in `M` the relation `c (f x + x) 0` holds, then for any `x` and `y` in `M` such that `c x y` holds, we have `c (f x) (f y)`.
More concisely: If an additive monoid `M` with an additive congruence relation `c` and a function `f` from `M` to `M` satisfy `c (f x + x) 0` for all `x` in `M`, then `c x y` implies `c (f x) (f y)`.
|
Con.coe_one
theorem Con.coe_one : ∀ {M : Type u_1} [inst : MulOneClass M] {c : Con M}, ↑1 = 1
This theorem states that in the context of a monoid `M` (a set equipped with an associative binary operation and an identity element), the equivalence class of the identity element `1` under a given congruence relation `c` is equal to `1` itself. In other words, if we partition the elements of the monoid `M` according to the congruence relation `c`, the identity element `1` is in the same class as itself.
More concisely: In a monoid with congruence relation `c`, the identity element lies in its own equivalence class.
|
Con.kerLift_injective
theorem Con.kerLift_injective :
∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] (f : M →* P),
Function.Injective ⇑(Con.kerLift f)
The theorem `Con.kerLift_injective` states that for any monoid homomorphism `f` from a monoid `M` to a monoid `P` (both monoids are endowed with a multiplication operation and a multiplicative identity element), the induced homomorphism on the quotient of `M` by the kernel of `f` is injective. In other words, if two members of the quotient monoid are mapped to the same element in `P` by this induced homomorphism, then they were the same member in the quotient monoid to start with. This theorem is a significant result in the theory of group homomorphisms and quotients.
More concisely: The homomorphism induced by a monoid homomorphism between two monoids is injective on the quotient by the kernel.
|
AddCon.toSetoid_inj
theorem AddCon.toSetoid_inj : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M}, c.toSetoid = d.toSetoid → c = d := by
sorry
This theorem states that the function that transforms an additive congruence relation into its underlying equivalence relation is injective. In other words, for any type `M` with an addition operation and any two additive congruence relations `c` and `d` on `M`, if the equivalence relations derived from `c` and `d` are equal, then `c` and `d` must be the same.
More concisely: If two additive congruence relations on a type with an addition operation have equal derived equivalence relations, then they are equal.
|
AddCon.add'
theorem AddCon.add' :
∀ {M : Type u_1} [inst : Add M] (self : AddCon M) {w x y z : M},
Setoid.r w x → Setoid.r y z → Setoid.r (w + y) (x + z)
The theorem `AddCon.add'` states that for any type `M` that has an addition operation (`Add M`), and for an additive congruence relation `self` on `M`, if two elements `w` and `x` are related by this congruence relation (`Setoid.r w x`), and if two other elements `y` and `z` are also related by the same congruence relation (`Setoid.r y z`), then the sums of `w` with `y` and `x` with `z` are also related by the same congruence relation (`Setoid.r (w + y) (x + z)`). In other words, additive congruence relations are preserved under addition.
More concisely: If `w` and `x` are related by an additive congruence relation and `y` and `z` are also related by the same congruence relation, then `w + y` and `x + z` are related by the same additive congruence relation.
|
AddCon.mk'_ker
theorem AddCon.mk'_ker : ∀ {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M), AddCon.ker c.mk' = c
This theorem states that the kernel of the natural homomorphism from an additive monoid to its quotient by an additive congruence relation `c` is equal to `c` itself. In other words, if you have an additive monoid `M` and an additive congruence relation `c` on `M`, then the set of elements that are mapped to the zero element of the quotient monoid by the natural homomorphism (which is defined by `c.mk'`) is exactly the set of elements that are related by the congruence relation `c`. This is what it means for `c` to be the kernel of the homomorphism.
More concisely: The kernel of the natural homomorphism from an additive monoid to its quotient by an additive congruence relation is equal to the congruence relation itself.
|
AddCon.symm
theorem AddCon.symm : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M) {x y : M}, c x y → c y x
This theorem states that additive congruence relations are symmetric. For any Type `M` that has an addition operation, and for any additive congruence relation `c` on `M`, if `x` and `y` are elements of `M` such that `c x y` holds, then `c y x` also holds. In other words, if `x` is congruent to `y` under the congruence relation `c`, then `y` is also congruent to `x` under the same relation.
More concisely: For any additive congruence relation `c` on an abelian group `(M, +)`, if `x ≡ y (mod c)`, then `y ≡ x (mod c)`.
|
Con.lift_coe
theorem Con.lift_coe :
∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} {f : M →* P}
(H : c ≤ Con.ker f) (x : M), (c.lift f H) ↑x = f x
The theorem `Con.lift_coe` establishes the universal property for quotients of monoids. Given two types `M` and `P` with `MulOneClass` structures (which means they behave like monoids with a multiplication operation and a designated "one" element), a congruence `c` on `M`, and a monoid homomorphism `f` from `M` to `P` such that `c` is less than or equal to the kernel of `f`, for any element `x` of `M`, the result of applying the lift of `f` with respect to `c` and `H` to the equivalence class of `x` under `c` (denoted `(c.lift f H) ↑x`) is equal to the result of applying `f` to `x` (denoted `f x`).
In simpler terms, this theorem states that if you map a monoid element `x` to another monoid through a monoid homomorphism `f` that respects a certain congruence `c`, it is the same as first taking the equivalence class of `x` under `c`, and then mapping it through the lifting of `f` with respect to `c` and `H`. This expresses the so-called commuting diagram property and is a key part of the universal property for quotients in category theory.
More concisely: Given a monoid homomorphism `f` from a monoid `M` to a monoid `P`, a congruence `c` on `M` contained in the kernel of `f`, and an element `x` in `M`, the lift of `f` with respect to `c` and `H` maps the equivalence class of `x` under `c` to `f(x)`.
|
Con.map_of_mul_left_rel_one
theorem Con.map_of_mul_left_rel_one :
∀ {M : Type u_1} [inst : Monoid M] (c : Con M) (f : M → M),
(∀ (x : M), c (f x * x) 1) → ∀ {x y : M}, c x y → c (f x) (f y)
This theorem states that in the context of defining a group as the quotient of a monoid by a congruence relation, the task of defining the inverse operation can be simplified. Typically, the inverse operation would be defined as `Setoid.map f _` for some function `f`, requiring proofs for both `∀ x y, c x y → c (f x) (f y)` and `∀ x, c (f x * x) 1`. However, this theorem shows that it is sufficient to only prove the latter (`∀ x, c (f x * x) 1`). In other words, if for every element `x` of the monoid `M`, `c (f x * x) 1` holds, then for any two elements `x` and `y` of `M` such that `c x y` holds, `c (f x) (f y)` will also hold.
More concisely: If the product of every element with itself in a monoid satisfies the congruence relation with the identity element, then the inverse operation can be defined as `Setoid.map f 1` for any function `f` preserving the congruence relation.
|
AddCon.lift_mk'
theorem AddCon.lift_mk' :
∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M} {f : M →+ P}
(H : c ≤ AddCon.ker f) (x : M), (c.lift f H) (c.mk' x) = f x
This theorem describes the universal property for quotients of additive monoids, stating that a certain diagram commutes. Specifically, for any types `M` and `P` that are instances of `AddZeroClass` (which are essentially additive monoids), given a congruence relation `c` on `M`, a homomorphism `f` from `M` to `P`, and a proof `H` that `c` is a subrelation of the kernel of `f`, the application of the lift of `f` with respect to `c` on the equivalence class of any element `x` in `M` is equal to the image of `x` under `f`. In other words, lifting `f` to the quotient of `M` by `c` and then applying it to the equivalence class of `x` gives the same result as just applying `f` to `x`.
More concisely: Given an additive monoid M, a congruence relation c on M, a homomorphism f : M -> P, and a proof that c is a subrelation of the kernel of f, for all x in M, the application of the lift of f with respect to c to the equivalence class [x]c is equal to f(x).
|
Con.map_apply
theorem Con.map_apply :
∀ {M : Type u_1} [inst : MulOneClass M] {c d : Con M} (h : c ≤ d) (x : c.Quotient),
(c.map d h) x = (c.lift d.mk' ⋯) x
The theorem `Con.map_apply` states that for any given type `M` equipped with a multiplication and identity (`MulOneClass M`), and given two congruence relations `c` and `d` on `M` such that `d` contains `c` (formally, `c ≤ d`), the application of the definition of the homomorphism from the quotient by `c` to the quotient by `d` (induced by `d`'s quotient map) is equivalent to the application of `c.lift d.mk'` on `x`. Here, `x` is an element of the quotient by `c`, and the homomorphism is given by `c.map d h`. The theorem essentially expresses a property of the homomorphism between quotients of a monoid with respect to different congruence relations.
More concisely: For any monoid `M` with congruence relations `c` and `d` such that `c ≤ d`, the homomorphism from `M/c` to `M/d` induced by `d`'s quotient map is equivalent to the composition of `c.lift` and `d.mk'` on the quotient `x` of `M` by `c`.
|
AddCon.lift_unique
theorem AddCon.lift_unique :
∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M} {f : M →+ P}
(H : c ≤ AddCon.ker f) (g : c.Quotient →+ P), g.comp c.mk' = f → g = c.lift f H
This theorem, referred to as `AddCon.lift_unique`, states the uniqueness part of the universal property for quotients of additive monoids. In detail, for any types `M` and `P` that are additive monoids (or have an `AddZeroClass` instance), a congruence relation `c` on `M`, a homomorphism `f` from `M` to `P`, a condition `H` that `c` is less than or equal to the kernel of `f`, and a homomorphism `g` from the quotient of `M` by `c` to `P`, if the composition of `g` with the quotient map from `M` to `c.Quotient` equals `f`, then `g` is equivalent to the lift of `f` via `c` under the condition `H`.
This theorem is essentially saying that in the context of additive monoids and additive congruence relations, there is a unique homomorphism from the quotient of the monoid by the congruence relation to any other additive monoid that makes the diagram commute. This is a fundamental property of quotients in category theory.
More concisely: Given additive monoids M and P, a congruence relation c on M, a homomorphism f from M to P, and a homomorphism g from the quotient of M by c to P such that H holds and g · q = f, where q is the quotient map from M to c.Quotient, then g is equal to the lift of f via c.
|
Con.ext
theorem Con.ext : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M}, (∀ (x y : M), c x y ↔ d x y) → c = d
The theorem `Con.ext` states that for any type `M` equipped with a multiplication operation, if we have two congruence relations `c` and `d` on `M`, then `c` is equal to `d` if and only if, for every pair of elements `x` and `y` from `M`, `x` is related to `y` by `c` if and only if `x` is related to `y` by `d`. Essentially, two congruence relations on a multiplication structure are identical if they relate the same pairs of elements.
More concisely: Two congruence relations on a multiplicative semigroup are equal if and only if they relate the same pairs of elements.
|
Con.lift_funext
theorem Con.lift_funext :
∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} (f g : c.Quotient →* P),
(∀ (a : M), f ↑a = g ↑a) → f = g
This theorem states that for any two homomorphisms `f` and `g` from the quotient of a monoid `M` under a congruence relation `c`, to another monoid `P`, if `f` and `g` agree on the images of all elements of `M` (represented as `f ↑a = g ↑a` where `↑a` denotes the image of `a` in the quotient), then the two homomorphisms are equal. This is essentially stating that two homomorphisms from a quotient monoid are determined by their actions on the elements of the original monoid.
More concisely: If `f` and `g` are homomorphisms from the quotient of a monoid `M` under a congruence relation `c` to another monoid `P`, and `f(a) = g(a)` for all `a` in `M`, then `f = g`.
|
Con.sup_def
theorem Con.sup_def : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M}, c ⊔ d = conGen (⇑c ⊔ ⇑d)
This theorem states that for any given type `M` equipped with a multiplication operation, and any two congruence relations `c` and `d` on `M`, the supremum (or join) of these two congruence relations is equal to the smallest congruence relation that contains the supremum of the underlying binary operations of `c` and `d`. In other words, when combining two congruence relations, the resulting relation is the smallest one that respects both the original relations and the multiplication operation on `M`.
More concisely: Given types `M` with a multiplication operation and congruence relations `c` and `d` on `M`, the smallest congruence relation containing the supremum of `c` and `d` is equal to the join of `c` and `d`.
|
AddCon.ker_eq_lift_of_injective
theorem AddCon.ker_eq_lift_of_injective :
∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] (c : AddCon M) (f : M →+ P)
(H : c ≤ AddCon.ker f), Function.Injective ⇑(c.lift f H) → AddCon.ker f = c
The theorem `AddCon.ker_eq_lift_of_injective` states that for any `AddMonoid` homomorphism `f` from a type `M` to a type `P` and for any additive congruence relation `c` on `M` such that `c` is included in the kernel of `f`, if the induced map from the quotient of `M` by `c` to `P` is injective (i.e., it does not map different elements to the same value), then `c` is the kernel of `f`. This theorem essentially provides a characterization of the kernel of an `AddMonoid` homomorphism in terms of injectivity of the induced map on the quotient.
More concisely: If `f` is an AddMonoid homomorphism from `M` to `P`, `c` is an additive congruence relation on `M` included in the kernel of `f`, and the induced map from the quotient of `M` by `c` to `P` is injective, then `c` is the kernel of `f`.
|
AddCon.sSup_eq_addConGen
theorem AddCon.sSup_eq_addConGen :
∀ {M : Type u_1} [inst : Add M] (S : Set (AddCon M)), sSup S = addConGen fun x y => ∃ c ∈ S, c x y
The theorem `AddCon.sSup_eq_addConGen` states that, given any set `S` of additive congruence relations on a type `M` equipped with addition, the supremum of `S` is equal to the smallest additive congruence relation that contains the binary relation 'there exists a relation `c` in `S` such that `x` is related to `y` by `c'`. In other words, the supremum of `S` is the minimal relation that relates `x` to `y` whenever there is some relation in `S` that does so.
More concisely: The supremum of a set of additive congruence relations on a type with addition is the smallest additive congruence relation containing the relation that unifies all relations in the set.
|
Con.conGen_le
theorem Con.conGen_le :
∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {c : Con M}, (∀ (x y : M), r x y → c x y) → conGen r ≤ c := by
sorry
The theorem `Con.conGen_le` states that for any type `M` equipped with a multiplication operation, given a binary relation `r` on `M` and a congruence relation `c` on `M` such that `c` contains `r`, then the smallest congruence relation containing `r` (denoted by `conGen r`) is contained within `c`. In other words, any congruence relation that contains `r` must also contain the smallest congruence relation built from `r`.
More concisely: For any type equipped with multiplication and given a binary relation and a congruence relation containing it, the smallest congruence relation generated from the relation is contained within the given congruence relation.
|
AddCon.induction_on₂
theorem AddCon.induction_on₂ :
∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {c : AddCon M} {d : AddCon N}
{C : c.Quotient → d.Quotient → Prop} (p : c.Quotient) (q : d.Quotient), (∀ (x : M) (y : N), C ↑x ↑y) → C p q
This theorem, `AddCon.induction_on₂`, is a more generalized version of `AddCon.induction_on` that allows for predicates with two arguments. Given two types `M` and `N` with defined addition operations, and two additive congruence relations `c` and `d` on `M` and `N` respectively, it states that for any predicate `C` taking two arguments from the quotient spaces of `M` and `N` by `c` and `d` respectively, if `C` holds for all pairs of representatives `(x, y)` from `M` and `N`, then `C` also holds for any two elements `p` and `q` from the quotient spaces. In mathematical terms, this theorem provides a principle of mathematical induction for two-variable predicates over quotients by additive congruence relations.
More concisely: Given additive congruence relations `c` on type `M` and `d` on type `N`, if a predicate `C` holds for all pairs of representatives from the quotient spaces `M / c` and `N / d`, then `C` holds for any pair of elements from `M / c` and `N / d`.
|
Con.div
theorem Con.div : ∀ {M : Type u_1} [inst : Group M] (c : Con M) {w x y z : M}, c w x → c y z → c (w / y) (x / z) := by
sorry
This theorem states that if we have a multiplicative congruence relation defined over a group, it preserves the operation of division. More formally, let `M` be a type that forms a group and `c` be a congruence relation on `M`. If `w` is congruent to `x` and `y` is congruent to `z` under the relation `c`, then the quotient of `w` by `y` is also congruent to the quotient of `x` by `z` under the same congruence relation `c`.
More concisely: If `w ≡x (mod c)` and `y ≡ z (mod c)` in a group `M` with congruence relation `c`, then `w / y ≡ x / z (mod c)`.
|
Con.sSup_eq_conGen
theorem Con.sSup_eq_conGen :
∀ {M : Type u_1} [inst : Mul M] (S : Set (Con M)), sSup S = conGen fun x y => ∃ c ∈ S, c x y
The theorem `Con.sSup_eq_conGen` says that for any type `M` that supports multiplication, and for any set `S` of congruence relations on `M`, the supremum of the set `S` is equal to the smallest congruence relation that contains the binary relation 'there exists a congruence relation `c` in `S` such that `x` is related to `y` via `c`'. In simpler terms, it asserts that the greatest lower bound of a set of congruence relations is the smallest congruence relation that includes all pairings where there's a congruence relation in the set that relates the two elements.
More concisely: The supremum of a set of congruence relations on a type `M` supporting multiplication is the smallest congruence relation containing all pairs with at least one congruence relation in the set relating the elements.
|
Con.kerLift_range_eq
theorem Con.kerLift_range_eq :
∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {f : M →* P},
MonoidHom.mrange (Con.kerLift f) = MonoidHom.mrange f
This theorem states that for any monoid homomorphism `f` from a monoid `M` to another monoid `P`, the image or range of the induced homomorphism on the quotient of `M` by the kernel of `f`, is the same as the image or range of `f`. In other words, the set of elements in `P` that can be reached by applying `f` is identical to the set of elements that can be reached by applying the induced homomorphism on the quotient monoid. Thus, the kernel of `f`, which is a kind of "noise" or "redundancy" in `M` that `f` cannot distinguish, does not affect the image of `f`.
More concisely: The image of a monoid homomorphism is equal to the image of its induced homomorphism on the quotient by the kernel.
|
Con.kerLift_mk
theorem Con.kerLift_mk :
∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {f : M →* P} (x : M),
(Con.kerLift f) ↑x = f x
This theorem states that for any given monoid homomorphism `f` from a monoid `M` to a monoid `P` and any element `x` of `M`, the result of applying the homomorphism induced on the quotient of `M` by the kernel of `f` to the equivalence class of `x` under this kernel is the same as the result of directly applying `f` to `x`. In other words, it confirms that the diagram which expresses the universal property for quotients of monoids, when the congruence relation is the kernel of the homomorphism, indeed commutes.
More concisely: For any monoid homomorphism $f$ from a monoid $M$ to a monoid $P$ and any $x$ in $M$, $f([x]\_{\ker(f)}) = [f(x)]\_{\ker(f)}$ in $P/\ker(f)$, where $[x]\_{\ker(f)}$ and $[f(x)]\_{\ker(f)}$ denote the equivalence classes of $x$ and $f(x)$ under the kernel of $f$, respectively.
|
AddCon.addConGen_eq
theorem AddCon.addConGen_eq :
∀ {M : Type u_1} [inst : Add M] (r : M → M → Prop), addConGen r = sInf {s | ∀ (x y : M), r x y → s x y}
This theorem states that for any type `M` with an addition operation and a binary relation `r` on `M`, the smallest inductively defined additive congruence relation that contains `r` is equal to the greatest lower bound (infimum) of the set of all additive congruence relations that contain `r`. In other words, the smallest relation that is both an additive congruence and contains `r`, is exactly the infimum of all additive congruences containing `r`.
More concisely: The smallest additive congruence relation containing a binary relation on a type with addition is equal to the infimum of all additive congruences containing it.
|
Con.eq
theorem Con.eq : ∀ {M : Type u_1} [inst : Mul M] (c : Con M) {a b : M}, ↑a = ↑b ↔ c a b
This theorem, `Con.eq`, states that for any type `M` equipped with a multiplication operation and any congruence relation `c` on `M`, two elements `a` and `b` from `M` are related by the congruence relation `c` if and only if they are represented by the same element in the quotient of `M` by `c`. In other words, `a` and `b` are congruent under the relation `c` precisely when their equivalence classes under `c` are the same.
More concisely: For any type equipped with a multiplication operation and a congruence relation, two elements are congruent if and only if their equivalence classes under the relation are equal.
|
Con.ext'
theorem Con.ext' : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M}, ⇑c = ⇑d → c = d
This theorem states that for any type `M` which is equipped with a multiplication operation, if we have two congruence relations `c` and `d` on `M`, and their underlying binary relations are identical, then the congruence relations `c` and `d` themselves must be identical. So, the function that takes a congruence relation and outputs its underlying binary relation is injective, meaning it will not map two different congruence relations to the same binary relation.
More concisely: If two congruence relations on a type with a multiplication operation have identical underlying binary relations, then they are equal.
|
Con.ext_iff
theorem Con.ext_iff : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M}, (∀ (x y : M), c x y ↔ d x y) ↔ c = d
This theorem states the "if and only if" version of the extensionality rule for congruence relations. Given a type `M` with a multiplication operation, and two congruence relations `c` and `d` over `M`, it asserts that `c` and `d` are the same relation if and only if for all elements `x` and `y` in `M`, `x` is related to `y` by `c` if and only if `x` is related to `y` by `d`.
More concisely: Two congruence relations over a type with multiplication are equal if and only if they define the same equivalence relation on the type, i.e., they make the same pairs equivalent.
|
Con.mul'
theorem Con.mul' :
∀ {M : Type u_1} [inst : Mul M] (self : Con M) {w x y z : M},
Setoid.r w x → Setoid.r y z → Setoid.r (w * y) (x * z)
The theorem `Con.mul'` states that for any type `M` that has a multiplication operation, given a congruence relation on `M` (represented by `self : Con M`), and any four elements `w, x, y, z` of `M`, if `w` is related to `x` and `y` is related to `z` under the congruence relation (as expressed by `Setoid.r w x` and `Setoid.r y z` respectively), then the products `w * y` and `x * z` are also related under the same congruence relation (`Setoid.r (w * y) (x * z)`). In other words, congruence relations in a multiplication structure are closed under multiplication.
More concisely: If `w` is congruent to `x` and `y` is congruent to `z` under a congruence relation on a multiplicative structure, then `w * y` is congruent to `x * z`.
|
AddCon.add
theorem AddCon.add : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M) {w x y z : M}, c w x → c y z → c (w + y) (x + z)
This theorem states that for any type `M` that has an addition operation, given an additive congruence relation `c` on `M`, if `w` is congruent to `x` and `y` is congruent to `z` under `c`, then the sum of `w` and `y` is congruent to the sum of `x` and `z` under the same congruence relation. In other words, congruence under `c` is preserved through the operation of addition, hence the name `AddCon.add`.
More concisely: For any additive congruence relation `c` on a type `M` with addition, if `w ≡x under c` and `y ≡ z under c`, then `w + y ≡ x + z under c`.
|
AddCon.lift_range
theorem AddCon.lift_range :
∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M} {f : M →+ P}
(H : c ≤ AddCon.ker f), AddMonoidHom.mrange (c.lift f H) = AddMonoidHom.mrange f
This theorem states that for a given additive congruence relation `c` on an additive monoid `M` and a homomorphism `f` that is constant on `c`'s equivalence classes, `f` and the homomorphism `f` induces on the quotient of `M` by `c` have the same range. In other words, both `f` and the quotient homomorphism map to the same set of values in the codomain `P`. Here, `c` being less than or equal to the kernel of `f` ensures that `f` is indeed constant on `c`'s equivalence classes.
More concisely: For an additive congruence relation `c` on an additive monoid `M` and a homomorphism `f` that is constant on `c`'s equivalence classes, the images of `f` and the quotient homomorphism of `f` on `M/c` have the same range.
|
Con.lift_surjective_of_surjective
theorem Con.lift_surjective_of_surjective :
∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} {f : M →* P}
(h : c ≤ Con.ker f), Function.Surjective ⇑f → Function.Surjective ⇑(c.lift f h)
This theorem states that for any two types `M` and `P` equipped with a multiplication operation and a neutral element (a `MulOneClass`), if `f` is a surjective monoid homomorphism from `M` to `P` and `c` is a congruence relation on `M` such that `c` is contained in the kernel of `f`, then the induced homomorphism on the quotient of `M` by `c` is also surjective.
In other words, if every element of `P` can be reached by `f` from an element of `M`, and `f` is constant on the equivalence classes defined by `c`, then every element of the quotient of `M` by `c` can also be reached by the induced homomorphism. This theorem is a property of surjective homomorphisms that are constant on congruence classes.
More concisely: If `f` is a surjective monoid homomorphism from type `M` to type `P` that is constant on congruence classes of a contained-in-kernel relation `c` on `M`, then the induced homomorphism on the quotient of `M` by `c` is also surjective.
|
Con.refl
theorem Con.refl : ∀ {M : Type u_1} [inst : Mul M] (c : Con M) (x : M), c x x
This theorem states that congruence relations are reflexive for any type `M` equipped with a multiplication operation. More specifically, for any such type `M`, any congruence relation `c` on `M`, and any element `x` of `M`, `x` is congruent to itself under `c`. In other words, for any multiplication-based type and any congruence relation on it, every element is congruent to itself under this relation.
More concisely: For any type `M` with multiplication and any congruence relation `c` on `M`, the reflexivity property holds, that is, for all `x` in `M`, `x` is congruent to `x` under `c`.
|
AddCon.coe_inf
theorem AddCon.coe_inf : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M}, ⇑(c ⊓ d) = ⇑c ⊓ ⇑d
This theorem states that for any type `M` equipped with an addition operation and any two additive congruence relations `c` and `d` on `M`, the infimum (greatest lower bound) of `c` and `d` as additive congruence relations is the same as the infimum of the underlying binary operations of `c` and `d`.
More concisely: For any type `M` with an addition operation, the infimum of two additive congruence relations `c` and `d` on `M` equals the infimum of their underlying binary operation congruences.
|
AddCon.le_def
theorem AddCon.le_def : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M}, c ≤ d ↔ ∀ {x y : M}, c x y → d x y
This theorem, `AddCon.le_def`, defines the comparison (≤) between two additive congruence relations `c` and `d` in an additive structure `M`. An additive congruence relation `c` is said to be less than or equal to `d` if, for any elements `x` and `y` in `M`, whenever `x` and `y` are related by `c`, they are also related by `d`. In other words, all pairs of elements that are equivalent under `c` are also equivalent under `d`.
More concisely: For all additive structures M and additive congruence relations c and d, c ≤ d if and only if for all x and y in M, x ~c y implies x ~d y. (Here, ~ denotes the equivalence relation defined by the congruence relation.)
|
AddCon.neg
theorem AddCon.neg : ∀ {M : Type u_1} [inst : AddGroup M] (c : AddCon M) {x y : M}, c x y → c (-x) (-y)
This theorem states that for any additive group `M` and any additive congruence relation `c` on `M`, if `x` and `y` are elements of `M` that are related by `c`, then their negations (`-x` and `-y`) are also related by `c`. In other words, an additive congruence relation preserves the operation of negation in the group. This is a property that arises in the study of abstract algebra.
More concisely: For any additive group (M, +) and additive congruence relation c on M, if x ≡ y (mod c), then -x ≡ -y (mod c).
|
AddCon.trans
theorem AddCon.trans : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M) {x y z : M}, c x y → c y z → c x z
This theorem states that additive congruence relations are transitive for any given type `M` that has an addition (`Add M`). Specifically, given an additive congruence relation `c` and any three objects `x`, `y`, and `z` of type `M`, if `x` is congruent to `y` under `c` and `y` is congruent to `z` under `c`, then `x` is congruent to `z` under `c`. Essentially, it means that if `x` is related to `y` and `y` is related to `z` in an additive congruence relation, then `x` is related to `z` in the same relation.
More concisely: If `x ≡ y` and `y ≡ z` hold in an additive congruence relation `c` on type `M` with addition, then `x ≡ z` holds in `c`.
|
Con.mk'_surjective
theorem Con.mk'_surjective : ∀ {M : Type u_1} [inst : MulOneClass M] {c : Con M}, Function.Surjective ⇑c.mk'
This theorem states that the natural homomorphism from a monoid to its quotient by a congruence relation is surjective. In other words, for any given monoid `M` with a multiplication and unit structure (`MulOneClass M`), and any congruence relation `c` on `M`, every element in the quotient of `M` by `c` can be reached by applying the natural homomorphism to some element in `M`.
More concisely: The natural homomorphism from a monoid to its quotient by a congruence relation is surjective, that is, every coset contains an element that maps to the identity element under the homomorphism.
|
AddCon.sup_eq_addConGen
theorem AddCon.sup_eq_addConGen :
∀ {M : Type u_1} [inst : Add M] (c d : AddCon M), c ⊔ d = addConGen fun x y => c x y ∨ d x y
This theorem states that for any given type `M` with an additive structure, and any two additive congruence relations `c` and `d` on `M`, the supremum (greatest lower bound) of `c` and `d` is the smallest additive congruence relation that contains the binary relation "`x` is related to `y` either by `c` or `d`". In other words, any two elements `x` and `y` of `M` are related in the supremum relation if and only if they are related either in `c` or in `d`.
More concisely: The supremum of two additive congruence relations on a type with additive structure is the smallest additive congruence relation containing their union.
|
AddCon.addConGen_of_addCon
theorem AddCon.addConGen_of_addCon : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M), addConGen ⇑c = c
This theorem states that for any additive congruence relation `c` on a type `M` equipped with an addition operation, `c` is equal to the smallest additive congruence relation that contains it. In other words, any given additive congruence relation is exactly the smallest possible congruence relation that includes all its pairs of congruent elements in the context of addition in `M`.
More concisely: For any additive congruence relation `c` on a type `M` with addition, `c` is the smallest additive congruence relation containing `c`.
|
AddCon.lift_comp_mk'
theorem AddCon.lift_comp_mk' :
∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M} {f : M →+ P}
(H : c ≤ AddCon.ker f), (c.lift f H).comp c.mk' = f
This theorem is about the universal property for quotients of additive monoids (`AddMonoid`s). It states that for any types `M` and `P` with classes `AddZeroClass`, and an additive congruence `c` on `M` and an additive monoid homomorphism `f` from `M` to `P` such that `c` is contained in the kernel of `f` (`AddCon.ker f`), the composition of the lift of `f` along `c` with the quotient map `c.mk'` equals `f`. In other words, the diagram involving the quotient map, the homomorphism, and the lift (an induced homomorphism from the quotient monoid to `P` that makes the diagram commute) commutes. This is a key property that characterizes the quotient of an additive monoid by a congruence relation in category theory.
More concisely: Given an additive monoid `M`, an additive congruence `c` on `M`, and an additive monoid homomorphism `f` from `M` to an additive monoid `P` such that `c` is contained in the kernel of `f`, the induced homomorphism from `M/c` to `P` via `f` and the quotient map from `M` to `M/c` commute.
|
Con.le_def
theorem Con.le_def : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M}, c ≤ d ↔ ∀ {x y : M}, c x y → d x y
This theorem provides a definition for the "less than or equal to" (`≤`) operator for congruence relations on a multiplication set. Given a type `M` that supports multiplication and two congruence relations `c` and `d` on `M`, it states that `c` is less than or equal to `d` (`c ≤ d`) if and only if for all pairs of elements `x` and `y` in `M`, whenever `x` and `y` are congruent under relation `c`, they are also congruent under relation `d`.
More concisely: For congruence relations `c` and `d` on a multiplication set `M`, `c` is less than or equal to `d` (`c ≤ d`) if and only if for all `x, y ∈ M`, `x ≡ y (c)` implies `x ≡ y (d)`.
|
Con.induction_on
theorem Con.induction_on :
∀ {M : Type u_1} [inst : Mul M] {c : Con M} {C : c.Quotient → Prop} (q : c.Quotient), (∀ (x : M), C ↑x) → C q := by
sorry
This theorem, `Con.induction_on`, is an instance of the inductive principle used to prove propositions about the elements of a quotient by a congruence relation. Given a type `M` equipped with a multiplication operation, a congruence relation `c` on `M`, a property `C` over the quotient of `M` by `c`, and an element `q` of the quotient type, this theorem states that if the property `C` holds for all elements of `M` (when considered as elements of the quotient), then `C` also holds for `q`.
More concisely: If a property holds for all equivalence classes of elements under a congruence relation with respect to a multiplication operation, then it holds for any given equivalence class.
|
AddCon.coe_sInf
theorem AddCon.coe_sInf : ∀ {M : Type u_1} [inst : Add M] (S : Set (AddCon M)), ⇑(sInf S) = sInf (DFunLike.coe '' S)
This theorem states that, for any set `S` of additive congruence relations on a type `M` with an addition operation (denoted `Add M`), the infimum of the set `S` is the same as the infimum of the image of the set `S` under the map to its underlying binary relation. In other words, it states an equality between the infimum of the additive congruence relations and the infimum of their corresponding binary relations. The function `DFunLike.coe` is used to map each additive congruence relation to its underlying binary relation.
More concisely: The infimum of a set of additive congruence relations on a type with addition equals the infimum of the corresponding binary relations obtained by applying the `DFunLike.coe` function.
|
Con.zpow
theorem Con.zpow : ∀ {M : Type u_1} [inst : Group M] (c : Con M) (n : ℤ) {w x : M}, c w x → c (w ^ n) (x ^ n) := by
sorry
This theorem states that, in the context of a group `M`, if two elements `w` and `x` are related by a certain multiplicative congruence relation `c`, then raising `w` and `x` to any integer power `n` preserves this relation. In other words, if `w` and `x` are congruent modulo `c`, then `w^n` and `x^n` are also congruent modulo `c`. This applies for any group, congruence relation, and integer exponent.
More concisely: In any group, if elements `w` and `x` are congruent with respect to a multiplicative congruence relation `c`, then raising them to any integer power `n` results in congruent elements modulo `c`.
|
Con.pow
theorem Con.pow : ∀ {M : Type u_4} [inst : Monoid M] (c : Con M) (n : ℕ) {w x : M}, c w x → c (w ^ n) (x ^ n) := by
sorry
This theorem states that if `w` and `x` are elements of a monoid `M` that are related by a congruence relation `c`, then their `n`-th powers are also related by the same congruence relation. More formally, for any natural number `n`, if `c w x` is true, then `c (w^n) (x^n)` is also true. This property is called the preservation of natural powers under multiplicative congruence relations.
More concisely: If `w` and `x` are related by a congruence relation `c` in a monoid, then `w^n` and `x^n` are related by `c` for any natural number `n`.
|
AddCon.lift_apply_mk'
theorem AddCon.lift_apply_mk' :
∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M}
(f : c.Quotient →+ P), c.lift (f.comp c.mk') ⋯ = f
This theorem states that for any given homomorphism `f` from the quotient of an additive monoid `M` by an additive congruence relation `c` to another additive monoid `P`, the result of applying function `f` is the same as the result of the homomorphism induced by `f` concatenated with the natural map from the additive monoid `M` to the quotient. In other words, when we map elements from the additive monoid `M` to the quotient and then apply the homomorphism `f`, it's equivalent to directly applying `f` on the quotient.
More concisely: For any additive monoid homomorphism `f` from `M/c` to `P`, where `M` is an additive monoid and `c` is an additive congruence on `M`, the diagram commutes: `M → M/c ❹ f = f ∘ (quot_map M)`.
|
Con.conGen_eq
theorem Con.conGen_eq :
∀ {M : Type u_1} [inst : Mul M] (r : M → M → Prop), conGen r = sInf {s | ∀ (x y : M), r x y → s x y}
This theorem states that for a given binary relation `r` on a type `M` equipped with multiplication, the smallest congruence relation containing `r`, which is inductively defined, is equivalent to the infimum of the set of all congruence relations which contain `r`. In other words, the smallest multiplicative congruence relation that includes `r` is the same as the greatest lower bound of the set of all congruence relations that satisfy `r`.
More concisely: The smallest multiplicative congruence relation containing a binary relation on a type with multiplication is equal to the greatest lower bound of all congruence relations containing it.
|
Con.inf_iff_and
theorem Con.inf_iff_and : ∀ {M : Type u_1} [inst : Mul M] {c d : Con M} {x y : M}, (c ⊓ d) x y ↔ c x y ∧ d x y := by
sorry
This theorem defines the infimum (greatest lower bound) of two congruence relations over the multiplication operation on a type `M`. Given two congruence relations `c` and `d` and two elements `x` and `y` of type `M`, it states that `(c ⊓ d) x y`, the infimum of `c` and `d`, holds if and only if both `c x y` and `d x y` hold. This means that `x` and `y` are related under the infimum of the two congruence relations if and only if `x` and `y` are related under each of the two congruence relations individually.
More concisely: The infimum of congruence relations c and d over the multiplication operation on type M holds between x and y if and only if both x y are related under c and x y are related under d.
|
Con.mapOfSurjective_eq_mapGen
theorem Con.mapOfSurjective_eq_mapGen :
∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {c : Con M} {f : M → N}
(H : ∀ (x y : M), f (x * y) = f x * f y) (h : Con.mulKer f H ≤ c) (hf : Function.Surjective f),
c.mapGen f = c.mapOfSurjective f H h hf
This theorem, `Con.mapOfSurjective_eq_mapGen`, asserts that for any multiplication structures `M` and `N`, a congruence relation `c` on `M`, and a multiplication-preserving surjective function `f : M → N`, if the kernel of `f` as a congruence relation (`Con.mulKer f`) is contained in `c`, then the smallest congruence relation generated by `f` (`c.mapGen f`) is equal to the congruence relation induced by `f` on `c` (`c.mapOfSurjective f`). This is a specialization of the principle that 'the smallest congruence relation containing a congruence relation `c` equals `c`'.
More concisely: If `f : M → N` is a multiplication-preserving surjective function between multiplication structures `M` and `N`, and `c` is a congruence relation on `M` such that `Con.mulKer f ⊆ c`, then `c.mapOfSurjective f` equals `c.mapGen f`.
|
Con.lift_range
theorem Con.lift_range :
∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} {f : M →* P}
(H : c ≤ Con.ker f), MonoidHom.mrange (c.lift f H) = MonoidHom.mrange f
The theorem `Con.lift_range` states that given a congruence relation `c` on a monoid, and a monoid homomorphism `f` that is constant on the equivalence classes of `c`, the image of `f` is the same as the image of the induced homomorphism on the quotient of the monoid by the congruence relation. Here, the condition "constant on the equivalence classes of `c`" is formalised as `c` being contained in the kernel of `f`, i.e., `H : c ≤ Con.ker f`. This theorem essentially says that when we factor through a congruence, the image of the homomorphism doesn't change.
More concisely: Given a congruence relation `c` on a monoid, and a monoid homomorphism `f` that respects `c` (i.e., `c ≤ ker f`), the image of `f` is equal to the image of the quotient monoid homomorphism induced by `f`.
|
AddCon.lift_surjective_of_surjective
theorem AddCon.lift_surjective_of_surjective :
∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M} {f : M →+ P}
(h : c ≤ AddCon.ker f), Function.Surjective ⇑f → Function.Surjective ⇑(c.lift f h)
The theorem `AddCon.lift_surjective_of_surjective` states that given two types `M` and `P` equipped with an additive zero class (which makes them into additive monoids), an additive congruence relation `c` on `M`, and a surjective homomorphism `f` from `M` to `P` such that `f` is constant on `c`'s equivalence classes, the induced function on the quotient of `M` by `c` is also surjective. In other words, if we have a surjective function that respects an additive congruence relation, then the function induced on the quotient by the congruence relation is also surjective.
More concisely: If `f` is a surjective homomorphism respecting an additive congruence relation `c` on additive monoids `M` and `P`, then the induced function on the quotient of `M` by `c` is also surjective.
|
AddCon.ext_iff
theorem AddCon.ext_iff : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M}, (∀ (x y : M), c x y ↔ d x y) ↔ c = d := by
sorry
This theorem, named `AddCon.ext_iff`, states that for any type `M` equipped with an additive structure, and any two additive congruence relations `c` and `d` over `M`, `c` is equal to `d` if and only if, for all `x` and `y` in `M`, `x` is related to `y` under `c` if and only if `x` is related to `y` under `d`. In other words, two additive congruence relations are the same if they relate the same pairs of elements in `M`.
More concisely: Two additive congruence relations on a type equipped with an additive structure are equal if and only if they relate the same pairs of elements.
|
AddCon.add_ker_mk_eq
theorem AddCon.add_ker_mk_eq : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M), AddCon.addKer AddCon.toQuotient ⋯ = c
This theorem states that for any additive congruence relation `c` on a type `M` with an addition operation, the kernel of the quotient map induced by `c` is equal to `c` itself. In other words, the set of elements in `M` that are mapped to the same value by the quotient map (i.e., the kernel of the quotient map) is exactly the set of elements identified by the congruence relation `c`. This fact is a key property of quotient maps in the theory of congruence relations.
More concisely: The kernel of the quotient map induced by an additive congruence relation on a type equals the relation itself.
|