feat(zmod/basic) #18953
feat(zmod/basic) #18953
Conversation
github-actions
bot
added
the
modifies-synchronized-file
src/data/zmod/units.lean
Outdated
| lemma coe_map_of_dvd {a b : ℕ} (h : a ∣ b) (x : units (zmod b)) : | ||
| is_unit (x : zmod a) := |
There was a problem hiding this comment.
Either have a lemma is_unit _ → is_unit _ or a function (zmod b)ˣ → (zmod a)ˣ (possibly we want both!), but not a mix of them like this.
There was a problem hiding this comment.
Its true that a ∣ b → (zmod b → zmod a)? I think this follows trivially from that.
There was a problem hiding this comment.
It is a single line proof, yes. Shall I remove it? I possibly need it for future work but I can add it then.
There was a problem hiding this comment.
It's true that a ∣ b → (zmod b →+* zmod a). It wouldn't surprise me if mathlib already had a coercion zmod b -> zmod a for arbitrary a and b :-/
| begin | ||
| apply @embedding.discrete_topology _ _ _ _ prod.discrete_topology (units.embed_product _) | ||
| (units.embedding_embed_product), | ||
| { apply_instance, }, | ||
| { refine inducing.discrete_topology (mul_opposite.unop_injective) rfl, }, | ||
| end |
There was a problem hiding this comment.
I think this works, no?
| begin | |
| apply @embedding.discrete_topology _ _ _ _ prod.discrete_topology (units.embed_product _) | |
| (units.embedding_embed_product), | |
| { apply_instance, }, | |
| { refine inducing.discrete_topology (mul_opposite.unop_injective) rfl, }, | |
| end | |
| by apply_instance |
There was a problem hiding this comment.
No, it does not. The topology is not canonical.
There was a problem hiding this comment.
I'm not sure I understand. The canonical topology on (X × Y)ˣ is the one coming from the embedding into (X × Y) × (X × Y). If X, Y have the discrete topology, then so does (X × Y)ˣ. This is exactly what you're proving here. What's your non-canonical topology doing if it agrees with the canonical one in your use case?
There was a problem hiding this comment.
The embedding is from (X × Y)ˣ to (X × Y) × (X × Y)ᵐᵒᵖ . I don't think (X × Y)ᵐᵒᵖ has the discrete topology as an instance
There was a problem hiding this comment.
Ah then can you add it? That seems like an obvious omission.
There was a problem hiding this comment.
Does apply_instance now work?
There was a problem hiding this comment.
Then can you remove it entirely?
There was a problem hiding this comment.
I am now getting an error in src/topology/algebra/group/basic.lean on line 1338 :
invalid 'open' command, unknown declaration 'units.mul_opposite.continuous_op'
however, I did not touch any of that code..
There was a problem hiding this comment.
embedding.discrete_topology is not known to the typeclass system. This works:
instance foo {X : Type*} [topological_space X] [discrete_topology X] :
discrete_topology Xᵐᵒᵖ := sorry
lemma discrete_topology_of_discrete {X : Type*} [_root_.topological_space X] [discrete_topology X]
[monoid X] : discrete_topology Xˣ :=
begin
apply embedding.discrete_topology units.embedding_embed_product,
apply_instance,
end
| lemma is_unit_of_is_coprime_dvd {a b : ℕ} (h : a ∣ b) {x : ℕ} (hx : x.coprime b) : | ||
| is_unit (x : zmod a) := |
There was a problem hiding this comment.
This sounds like you're mixing two steps at once.
| lemma is_unit_of_is_coprime_dvd {a b : ℕ} (h : a ∣ b) {x : ℕ} (hx : x.coprime b) : | |
| is_unit (x : zmod a) := | |
| lemma is_unit_of_is_coprime {a x : ℕ} (hx : x.coprime a) : | |
| is_unit (x : zmod a) := |
and in fact that shows you can actually get an iff:
| lemma is_unit_of_is_coprime_dvd {a b : ℕ} (h : a ∣ b) {x : ℕ} (hx : x.coprime b) : | |
| is_unit (x : zmod a) := | |
| @[simp] lemma is_unit_iff_is_coprime {a x : ℕ} : | |
| is_unit (x : zmod a) \iff x.coprime a := |
| Note this is not the topology used by default in mathlib.-/ | ||
| @[continuity] | ||
| lemma induced_top_cont_inv {X : Type*} [topological_space X] [discrete_topology X] [monoid X] : | ||
| @continuous _ _ (topological_space.induced (units.coe_hom X) infer_instance) _ |
There was a problem hiding this comment.
The question now is: What makes you need that non-canonical topology?
| -- { refine λ a b h, units.eq_iff.1 h, }, } | ||
| end | ||
|
|
||
| lemma discrete_topology_of_discrete {X : Type*} [_root_.topological_space X] [discrete_topology X] |
There was a problem hiding this comment.
Can you make that an instance and make sure the name is units.discrete_topology (probably you just need to remove the explicit name)?
| -- { refine λ a b h, units.eq_iff.1 h, }, } | ||
| end | ||
|
|
||
| lemma discrete_topology_of_discrete {X : Type*} [_root_.topological_space X] [discrete_topology X] |
There was a problem hiding this comment.
This _root_ is fishy. Can you mark protected whatever declaration topological_space could refer to here?
| lemma discrete_prod_units {X Y : Type*} [monoid X] [monoid Y] [topological_space X] | ||
| [discrete_topology X] [topological_space Y] [discrete_topology Y] : discrete_topology (X × Y)ˣ := | ||
| embedding.discrete_topology (units.embedding_embed_product) |
There was a problem hiding this comment.
Once you've made the above an instance,
| lemma discrete_prod_units {X Y : Type*} [monoid X] [monoid Y] [topological_space X] | |
| [discrete_topology X] [topological_space Y] [discrete_topology Y] : discrete_topology (X × Y)ˣ := | |
| embedding.discrete_topology (units.embedding_embed_product) |
Adding some properties regarding
zmod nand its units. In particular, we makezmod na discrete space and obtain a discrete topology on its units. There are some arithmetic properties regardingzmod.val. Finally, we add some lemmas regarding coercion with respect to the Chinese Remainder Theorem.