feat(Algebra/GroupWithZero/Range): the range of a MonoidHom whose codomain is a GroupWithZero as a GroupWithZero when #25496
feat(Algebra/GroupWithZero/Range): the range of a MonoidHom whose codomain is a GroupWithZero as a GroupWithZero when #25496
Conversation
…omain is a GroupWithZero as a GroupWithZero when We define an instance of `GroupWithZero` on the range of a MonoidHom taking values in a `GroupWithZero` Co-authored-by: Antoine Chambert-Loir --- <!-- The text above the `---` will become the commit message when your PR is merged. Please leave a blank newline before the `---`, otherwise GitHub will format the text above it as a title. For details on the "pull request lifecycle" in mathlib, please see: https://leanprover-community.github.io/contribute/index.html In particular, note that most reviewers will only notice your PR if it passes the continuous integration checks. Please ask for help on https://leanprover.zulipchat.com if needed. To indicate co-authors, include lines at the bottom of the commit message (that is, before the `---`) using the following format: Co-authored-by: Author Name <author@email.com> If you are moving or deleting declarations, please include these lines at the bottom of the commit message (that is, before the `---`) using the following format: Moves: - Vector.* -> List.Vector.* - ... Deletions: - Nat.bit1_add_bit1 - ... Any other comments you want to keep out of the PR commit should go below the `---`, and placed outside this HTML comment, or else they will be invisible to reviewers. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] --> [](https://gitpod.io/from-referrer/)
PR summary 45feb5a269Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
you need to run Also, can you fix the description of this PR? It currently ends mid-sentence. |
| /-! # Range of MonoidHomWithZero | ||
| Given a function `f : A → B` whose codomain `B` is a `GroupWithZero`, we define the | ||
| type `range₀`, by endowing the invertible elements in the range of `f` (i.e., all non-zero elements) | ||
| with a `0` (inherited from that of `B`): it is a `GroupWithZero` and if `B` is commutative, then |
There was a problem hiding this comment.
it is a
GroupWithZero
The thing you describe here is not a group with 0 in the generality in which you are writing (A is a random type and f is a random function). e.g. A could be {37} and f can be the inclusion into NNReal; then the thing you are describing here is {0,37}.
| * `range₀ f` is the smallest subgroup with zero containing the range of `f`; | ||
| * `range₀ f` is a `CancelCommMonoidWithZero`; | ||
| * `range₀ f` is a `GroupWithZero`; | ||
| * When `A` is a monoid with zero and `f` is a homomorphism of monoids with zero, `range₀ f` can be | ||
| explicitely descibed as the elements that are ratios of terms in `range f` , see | ||
| `MonoidHomWithZero.mem_range₀_iff_of_comm`. |
There was a problem hiding this comment.
I think we should stick to he usual style here, which is
## Main results
[set up notation, i.e. types of the things which will be inputs into the theorems]
* `name_of_theorem f A B` : `range₀ f` is the smallest subgroup with zero containing the range of `f`;
* etc
| section GroupWithZero | ||
|
|
||
| variable [GroupWithZero B] | ||
|
|
|
|
||
| ## Implementation details | ||
| The definition of `range₀` (as a `Submonoid B`) simply requires that `B` be a nontrivial | ||
| `CancelMonoidWithZero`, and no assumption neither on `A` nor on `f` is needed; that `B` is a |
There was a problem hiding this comment.
| `CancelMonoidWithZero`, and no assumption neither on `A` nor on `f` is needed; that `B` is a | |
| `CancelMonoidWithZero`, and no assumption on either `A` or`f` is needed; that `B` is a |
(sounds a bit better to this native speaker)
| /-- For a map with codomain a `MonoidWithZero`, this is a smallest | ||
| `GroupWithZero`, that contains the invertible elements in the image. | ||
|
|
||
| See `MonoidHomWithZero.mem_range₀_iff_of_comm` for another characterization | ||
| of `range₀ f` when `B` is commutative. -/ |
There was a problem hiding this comment.
The codomain is a GroupWithZero not a MonoidWithZero and a simpler way of saying "this is a smallest
GroupWithZero, that contains the invertible elements in the image." is "this is the smallest group with zero containing the image".
My instinct is that that the "mathlib way" to do this is just to define the lattice of subgroupwithzeros of a groupwithzero and then define this to be the SubgroupWithZero.closure of the range, rather than packing all of this stuff into carrier and then having to write such a complicated proof of mul_mem'.
There was a problem hiding this comment.
Your instinct is correct, but this is a side PR for some other aim (correcting the definition of the valuation on topologies) and I fear it will take us too far away.
There was a problem hiding this comment.
After some discussions with @faenuccio in Cambridge last week we decided that the best way to proceed is actually to define the value group of a valuation. We don't have this! We have something called ValueGroup but it's a group with zero and it's only defined under certain conditions. The value group of a valuation should be a subgroup of the group of units of the target groupwithzero:
import Mathlib
namespace Valuation
variable {R Γ₀ : Type*} [LinearOrderedCommMonoidWithZero Γ₀] [Ring R] (v : Valuation R Γ₀)
def ValueGroup : Subgroup Γ₀ˣ := .closure {γ : Γ₀ˣ | ∃ r, v r = γ}This should hopefully (a) be easier to work with than the definition currently in this PR (b) avoid the large amount of boilerplate which I had previously suggested and (c) give an easy definition of Discrete, which as far as I can see is the only thing currently holding up the definition of Valued.LocalField, the proposed definition of a local field which extends Valued.
NB: the plan currently is to have a second definition of a local field which does not come equipped with a preferred valuation, but for this we need the "module" of a locally compact ring: this is currently waiting on #25829 .
We define an instance of
GroupWithZeroon the subgroup generated by the range of a MonoidHom taking values in aGroupWithZero(by adding a zero to it).Co-authored-by: @AntoineChambert-Loir