feat(zmod/basic)

[laughinggas]

Adding some properties regarding zmod n and its units. In particular, we make zmod n a discrete space and obtain a discrete topology on its units. There are some arithmetic properties regarding zmod.val. Finally, we add some lemmas regarding coercion with respect to the Chinese Remainder Theorem.

---

[YaelDillies]

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.

[eric-wieser]

Its true that a ∣ b → (zmod b → zmod a)? I think this follows trivially from that.

[laughinggas]

It is a single line proof, yes. Shall I remove it? I possibly need it for future work but I can add it then.

[kbuzzard]

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 :-/

[YaelDillies]

I think this works, no?

Suggested change

	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

[laughinggas]

No, it does not. The topology is not canonical.

[YaelDillies]

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?

[laughinggas]

The embedding is from (X × Y)ˣ to (X × Y) × (X × Y)ᵐᵒᵖ . I don't think (X × Y)ᵐᵒᵖ has the discrete topology as an instance

[YaelDillies]

Ah then can you add it? That seems like an obvious omission.

[YaelDillies]

Does apply_instance now work?

[laughinggas]

Yes

[YaelDillies]

Then can you remove it entirely?

[laughinggas]

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..

[kbuzzard]

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

[YaelDillies]

l

[YaelDillies]

This sounds like you're mixing two steps at once.

Suggested change

	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:

Suggested change

	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 :=

[YaelDillies]

The question now is: What makes you need that non-canonical topology?

[YaelDillies]

Can you make that an instance and make sure the name is units.discrete_topology (probably you just need to remove the explicit name)?

[YaelDillies]

This _root_ is fishy. Can you mark protected whatever declaration topological_space could refer to here?

[YaelDillies]

Once you've made the above an instance,

Suggested change

	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)