Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(algebra/group_with_zero): Bundled
monoid_with_zero_hom (#4995)
This adds, without notation, `monoid_with_zero_hom` as a variant of `A →* B` that also satisfies `f 0 = 0`. As part of this, this change: * Splits up `group_with_zero` into multiple files, so that the definitions can be used in the bundled homs before any of the lemmas start pulling in dependencies * Adds `monoid_with_zero_hom` as a base class of `ring_hom` * Changes some `monoid_hom` objects into `monoid_with_zero_hom` objects. * Moves some lemmas about `valuation` into `monoid_hom`, since they apply more generally * Add automatic coercions between `monoid_with_zero_hom` and `monoid_hom`
- Loading branch information
1 parent
7a70764
commit 86b0971
Showing
22 changed files
with
360 additions
and
177 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| import algebra.group_with_zero.basic |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,113 @@ | ||
| /- | ||
| Copyright (c) 2020 Johan Commelin. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Johan Commelin | ||
| -/ | ||
| import algebra.group.defs | ||
| import logic.nontrivial | ||
|
|
||
| /-! | ||
| # Typeclasses for groups with an adjoined zero element | ||
| This file provides just the typeclass definitions, and the projection lemmas that expose their | ||
| members. | ||
| ## Main definitions | ||
| * `group_with_zero` | ||
| * `comm_group_with_zero` | ||
| -/ | ||
|
|
||
| set_option old_structure_cmd true | ||
|
|
||
| variables {M₀ G₀ M₀' G₀' : Type*} | ||
|
|
||
| section | ||
|
|
||
| /-- Typeclass for expressing that a type `M₀` with multiplication and a zero satisfies | ||
| `0 * a = 0` and `a * 0 = 0` for all `a : M₀`. -/ | ||
| @[protect_proj, ancestor has_mul has_zero] | ||
| class mul_zero_class (M₀ : Type*) extends has_mul M₀, has_zero M₀ := | ||
| (zero_mul : ∀ a : M₀, 0 * a = 0) | ||
| (mul_zero : ∀ a : M₀, a * 0 = 0) | ||
|
|
||
| section mul_zero_class | ||
|
|
||
| variables [mul_zero_class M₀] {a b : M₀} | ||
|
|
||
| @[ematch, simp] lemma zero_mul (a : M₀) : 0 * a = 0 := | ||
| mul_zero_class.zero_mul a | ||
|
|
||
| @[ematch, simp] lemma mul_zero (a : M₀) : a * 0 = 0 := | ||
| mul_zero_class.mul_zero a | ||
|
|
||
| end mul_zero_class | ||
|
|
||
| /-- Predicate typeclass for expressing that `a * b = 0` implies `a = 0` or `b = 0` | ||
| for all `a` and `b` of type `G₀`. -/ | ||
| class no_zero_divisors (M₀ : Type*) [has_mul M₀] [has_zero M₀] : Prop := | ||
| (eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : M₀}, a * b = 0 → a = 0 ∨ b = 0) | ||
|
|
||
| export no_zero_divisors (eq_zero_or_eq_zero_of_mul_eq_zero) | ||
|
|
||
| /-- A type `M` is a “monoid with zero” if it is a monoid with zero element, and `0` is left | ||
| and right absorbing. -/ | ||
| @[protect_proj] class monoid_with_zero (M₀ : Type*) extends monoid M₀, mul_zero_class M₀. | ||
|
|
||
| /-- A type `M` is a `cancel_monoid_with_zero` if it is a monoid with zero element, `0` is left | ||
| and right absorbing, and left/right multiplication by a non-zero element is injective. -/ | ||
| @[protect_proj] class cancel_monoid_with_zero (M₀ : Type*) extends monoid_with_zero M₀ := | ||
| (mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c) | ||
| (mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b ≠ 0 → a * b = c * b → a = c) | ||
|
|
||
| section cancel_monoid_with_zero | ||
|
|
||
| variables [cancel_monoid_with_zero M₀] {a b c : M₀} | ||
|
|
||
| lemma mul_left_cancel' (ha : a ≠ 0) (h : a * b = a * c) : b = c := | ||
| cancel_monoid_with_zero.mul_left_cancel_of_ne_zero ha h | ||
|
|
||
| lemma mul_right_cancel' (hb : b ≠ 0) (h : a * b = c * b) : a = c := | ||
| cancel_monoid_with_zero.mul_right_cancel_of_ne_zero hb h | ||
|
|
||
| end cancel_monoid_with_zero | ||
|
|
||
| /-- A type `M` is a commutative “monoid with zero” if it is a commutative monoid with zero | ||
| element, and `0` is left and right absorbing. -/ | ||
| @[protect_proj] | ||
| class comm_monoid_with_zero (M₀ : Type*) extends comm_monoid M₀, monoid_with_zero M₀. | ||
|
|
||
| /-- A type `M` is a `comm_cancel_monoid_with_zero` if it is a commutative monoid with zero element, | ||
| `0` is left and right absorbing, | ||
| and left/right multiplication by a non-zero element is injective. -/ | ||
| @[protect_proj] class comm_cancel_monoid_with_zero (M₀ : Type*) extends | ||
| comm_monoid_with_zero M₀, cancel_monoid_with_zero M₀. | ||
|
|
||
| /-- A type `G₀` is a “group with zero” if it is a monoid with zero element (distinct from `1`) | ||
| such that every nonzero element is invertible. | ||
| The type is required to come with an “inverse” function, and the inverse of `0` must be `0`. | ||
| Examples include division rings and the ordered monoids that are the | ||
| target of valuations in general valuation theory.-/ | ||
| class group_with_zero (G₀ : Type*) extends monoid_with_zero G₀, has_inv G₀, nontrivial G₀ := | ||
| (inv_zero : (0 : G₀)⁻¹ = 0) | ||
| (mul_inv_cancel : ∀ a:G₀, a ≠ 0 → a * a⁻¹ = 1) | ||
|
|
||
| section group_with_zero | ||
| variables [group_with_zero G₀] | ||
|
|
||
| @[simp] lemma inv_zero : (0 : G₀)⁻¹ = 0 := | ||
| group_with_zero.inv_zero | ||
|
|
||
| @[simp] lemma mul_inv_cancel {a : G₀} (h : a ≠ 0) : a * a⁻¹ = 1 := | ||
| group_with_zero.mul_inv_cancel a h | ||
|
|
||
| end group_with_zero | ||
|
|
||
| /-- A type `G₀` is a commutative “group with zero” | ||
| if it is a commutative monoid with zero element (distinct from `1`) | ||
| such that every nonzero element is invertible. | ||
| The type is required to come with an “inverse” function, and the inverse of `0` must be `0`. -/ | ||
| class comm_group_with_zero (G₀ : Type*) extends comm_monoid_with_zero G₀, group_with_zero G₀. | ||
|
|
||
| end |
Oops, something went wrong.