## Stream: maths

### Topic: cardinality of integers modulo n

#### Joey van Langen (Jan 14 2019 at 15:58):

I am trying to prove the following result

example (n : ℕ) (h : n ≠ 0) : ideal.quotient (ideal.span {(n : ℤ)}) ≃ fin n := sorry


This seems a simple result in math, but I am having a lot of trouble making a simple proof in lean. Anyone got any suggestions?

#### Johan Commelin (Jan 14 2019 at 16:02):

I don't think you want that fintype there.

#### Johan Commelin (Jan 14 2019 at 16:02):

fintype means as much as "Hey Lean, this type is finite".

#### Joey van Langen (Jan 14 2019 at 16:03):

That is right, I first wanted to split proving finite and the exact cardinality separately, but realized I could combine the two

#### Johan Commelin (Jan 14 2019 at 16:04):

If you want to construct a map from ideal.quotient ... to the right, look for things called lift in the file of ideal quotients.

#### Johan Commelin (Jan 14 2019 at 16:05):

Maybe the easiest way would be to compute the kernel of the cast : int → zmod n

#### Johan Commelin (Jan 14 2019 at 16:05):

And then use the isomorphism theorem (that we probably don't have :rolling_on_the_floor_laughing:)

#### Joey van Langen (Jan 14 2019 at 16:06):

We don't have an isomorphism theorem. At least not for rings

#### Joey van Langen (Jan 14 2019 at 16:07):

zmod may also be fin since I am not necessarily interested in the ring structure of it

#### Chris Hughes (Jan 14 2019 at 16:08):

There is already a construction of zmod n in data.zmod.basic

#### Joey van Langen (Jan 14 2019 at 16:09):

But there it is not constructed using the integers. The thing on the left naturally arises from a problem I have and I want to relate the two

#### Joey van Langen (Jan 14 2019 at 16:09):

Or at least get the necessary result about cardinality of the quotient on the left

#### Johan Commelin (Jan 14 2019 at 16:14):

I agree that the lemma you state should be proven at some point. So we might as well do it now.

#### Joey van Langen (Jan 14 2019 at 16:14):

This is what I have thus far:

let nℤ := @span ℤ _ {(n : ℤ)} in
let ℤmodnℤ := ideal.quotient nℤ in
have g : fin n → ℤmodnℤ, from λ m : fin n, ideal.quotient.mk nℤ $of_nat$ m.val,
have f : ℤ → fin n, from λ x : ℤ,
{ val := nat_abs (x % n),
is_lt := sorry},
have f' : ℤmodnℤ → fin n, from sorry


#### Johan Commelin (Jan 14 2019 at 16:15):

I think it is better to prove the isomorphism theorem. Because you will need that time and again

#### Johan Commelin (Jan 14 2019 at 16:16):

@Chris Hughes @Kenny Lau Do you have anything in that direction?

#### Chris Hughes (Jan 14 2019 at 16:16):

I'm not sure on your application, but I think the best way to do quotient rings in Lean is to not prove things about the quotient construction, but prove lemmas about quotient rings for any quotient, even if it isn't constructed using the quot constant. For example, ideal.lift, should have been defined with a type like this.

def lift {γ : Type*} [comm_ring γ] (f : α → β) [is_ring_hom f] (q : α → γ) [is_ring_hom q] (hq : surjective q)
(H : ∀ (a : α), q a = 0 → f a = 0) : γ → β :=


Would refactoring the library like this help?

#### Chris Hughes (Jan 14 2019 at 16:17):

For the cardinality, all you need is the isomorphism theorem on groups, which is already there.

#### Johan Commelin (Jan 14 2019 at 16:18):

Aah, if we have it for groups, then proving it for rings shouldn't be too hard. But I agree that we don't need it for the cardinality result.

#### Joey van Langen (Jan 14 2019 at 16:19):

So working with the predefined group structure on zmod n should do the trick

#### Joey van Langen (Jan 14 2019 at 16:19):

I will try to make that work

#### Johan Commelin (Jan 14 2019 at 16:21):

@Chris Hughes Don't you need your q to be a ring hom as well?

#### Johan Commelin (Jan 14 2019 at 16:22):

I mean, you can probably define this... But then you can't really prove things about it.

#### Johan Commelin (Jan 14 2019 at 16:22):

... without extra assumptions

#### Chris Hughes (Jan 14 2019 at 16:23):

Yes, I missed that out.

#### Joey van Langen (Jan 14 2019 at 16:27):

Would refactoring the library like this help?

I think the current version of lift is fine, as you most often want maps from a quotient

#### Chris Hughes (Jan 14 2019 at 16:28):

Why do you need to construct ℤmodnℤ using quotient instead of using zmod n?

#### Joey van Langen (Jan 14 2019 at 16:30):

For finite fields, to show that they are field extensions of some field with p elements, I make use of the natural map from $\mathbb{Z}$ to the field which factors over a quotient of that form.

#### Chris Hughes (Jan 14 2019 at 16:33):

So if you had lift with the type I suggested, you could show the field homomorphism directly from zmodp p hp instead of mentioning ideal.quotient right?

#### Joey van Langen (Jan 14 2019 at 16:36):

I would need to prove that the map to zmod p hp is surjective, which is I think the difficult part of the proof I want

#### Joey van Langen (Jan 14 2019 at 16:37):

A priori you do not know that there is a map from zmod p hp to the field

#### Chris Hughes (Jan 14 2019 at 16:38):

There's a proof somewhere that fin.val is a one-sided inverse of int.cast or perhaps only nat.cast

#### Neil Strickland (Jan 14 2019 at 16:50):

I vote in favour of @Chris Hughes 's suggestion for refactoring. I have thought about the technicalities of formalizing a number of arguments, both for arbitrary commutative rings and for rings arising in algebraic topology, and it is clear that the more flexible form of the lift construction will be much more convenient in many places. The same applies for localisations: instead of a theorem about homomorphisms $A[S^{-1}]\to B$ , there should be an is_localization predicate for maps $A\to A'$ and a theorem about maps $A'\to B$ when that predicate is satisfied.

#### Kevin Buzzard (Jan 14 2019 at 17:27):

I don't quite understand this yet, but I'd like to [NB $A\to A'$for maths mode on Zulip]. Currently given a commutative ring A and a submonoid S of A we have some localisation type loc A Splus a proof it's a ring, and the universal property theorems.

This approach gave me trouble. I was a Lean amateur at the time. I wanted to prove things like $A[1/f][1/g]=A[1/fg]$ (that's the mathematician's "=" there -- "canonical isomorphism" if you'd rather) from the universal property and if I remember correctly there was a lot of kerfuffle. See https://github.com/kbuzzard/lean-stacks-project/blob/ad816148cd9292f9205efd2674e180418d2680ec/src/localization_UMP.lean#L230 for example. In fact https://github.com/kbuzzard/lean-stacks-project/blob/ad816148cd9292f9205efd2674e180418d2680ec/src/localization_UMP.lean#L288 was even worse -- I briefly explain what I was trying to do in the comments above. I was hoping @Ramon Fernandez Mir would refactor all this, this month.

Is the idea instead that if $f:A\to B$ and $S\subseteq A$ then we have a predicate which mathematically means that the induced $A$-algebra structure on $B$ is isomorphic to $A[1/S]$?

#### Patrick Massot (Jan 14 2019 at 19:37):

Compare with https://github.com/leanprover/mathlib/blob/19e7b1f574d813b9b305b41f8c0820c01bf99c84/analysis/topology/continuity.lean#L379-L382 and how it appears in different statements, including https://github.com/leanprover/mathlib/blob/19e7b1f574d813b9b305b41f8c0820c01bf99c84/analysis/topology/continuity.lean#L934 but not only

#### Kenny Lau (Jan 14 2019 at 21:35):

import ring_theory.ideals

example (n : ℕ) (h : n ≠ 0) : ideal.quotient (ideal.span ({n} : set ℤ)) ≃ fin n :=
{ to_fun := λ x, quotient.lift_on' x (λ i, (⟨int.nat_abs (i%n),
int.coe_nat_lt.1 $by rw [int.nat_abs_of_nonneg (int.mod_nonneg _ (int.coe_nat_ne_zero.2 h))]; exact int.mod_lt_of_pos _ (int.coe_nat_pos.2$ nat.pos_of_ne_zero h)⟩ : fin n))
(λ i j hij, let ⟨k, hk⟩ := ideal.mem_span_singleton.1 hij in fin.eq_of_veq $show int.nat_abs _ = int.nat_abs _, by rw [eq_add_of_sub_eq hk, add_comm, int.add_mul_mod_self_left]), inv_fun := λ k, ideal.quotient.mk _ k, left_inv := λ x, quotient.induction_on' x$ λ i, quotient.sound' $ideal.mem_span_singleton'.2 ⟨_, show _ = ↑(int.nat_abs (i%n)) - i, by rw [int.nat_abs_of_nonneg (int.mod_nonneg _ (int.coe_nat_ne_zero.2 h)), int.mod_def, sub_sub, add_comm, sub_add_eq_sub_sub, sub_self, zero_sub, neg_mul_eq_mul_neg, mul_comm]⟩, right_inv := λ k, fin.eq_of_veq$ show int.nat_abs (k.1%n) = _, by rw [← int.coe_nat_mod, int.nat_abs_of_nat, nat.mod_eq_of_lt k.2] }


#### Mario Carneiro (Jan 15 2019 at 00:17):

@Kevin Buzzard Yes, this is the idea. Something just like it came up during the mathlib maintenance discussion at lean together, where we had an equality theorem quotient (separation_setoid A) = (\bot : ideal A).quotient, IIRC. If we could say that something is a quotient rather than having a quotient construction, then this typal equality could be avoided

#### Mario Carneiro (Jan 15 2019 at 00:18):

Topology already has the notion of a "quotient map" that is already performing this exact thing, we just need to extend it to quotient maps of rings, groups, etc, as well as localization maps and maps for other kinds of constructions

#### Mario Carneiro (Jan 15 2019 at 00:20):

Of course we still want the construction - it's no good having theorems about quotient maps if we can't prove they exist - but being able to quantify over things isomorphic to a particular construction is actually a really powerful way to avoid DTT hell

#### Mario Carneiro (Jan 15 2019 at 00:21):

I think we've also talked about having a euclidean_space A typeclass that basically means "isomorphic to R^n" which seems silly but is useful for exactly this kind of thing - you don't want to build in a dependence on the precise way a type is constructed

#### Patrick Massot (Jan 15 2019 at 07:59):

Yes, this is exactly why I posted the cryptic link in my previous message in this thread.

#### Patrick Massot (Jan 15 2019 at 08:01):

And I wanted to mention this quotient (separation_setoid A) = (\bot : ideal A).quotient (which is here) in my Amsterdam talk but I didn't have time. Note that I did find a workaround in the mean time, but we should still do something more systematic.

#### Kevin Buzzard (Jan 15 2019 at 08:07):

One big difference between localisations and Euclidean space is that if the $A$-algebra $B$ is isomorphic to $A[1/S]$ as an $A$-algebra then it's uniquely isomorphic to $A[1/S]$ as an $A$-algebra. However if a space is isomorphic to $\mathbb{R}^n$ as an $\mathbb{R}$-vector space, then there is in general more than one isomorphism, and you may or may not want to keep track of an isomorphism I guess, depending on what you're doing.

#### Kevin Buzzard (Jan 15 2019 at 09:00):

Is the idea instead that if $f:A\to B$ and $S\subseteq A$ then we have a predicate which mathematically means that the induced $A$-algebra structure on $B$ is isomorphic to $A[1/S]$?

Aah! The penny has just dropped. Instead of the definition of the predicate being "B is isomorphic to the A[1/S] we constructed", it says "B satisfies the universal property we want". Is that the idea? We have predicates for universal properties?

#### Kenny Lau (Jan 15 2019 at 09:02):

Are all isomorphisms isomorphic?

#### Kenny Lau (Jan 15 2019 at 09:02):

but universal property is not a property... it is a function and has data right

#### Kevin Buzzard (Jan 15 2019 at 09:03):

Given f:A->B and S in A, the universal property just says that for all A -> C sending S to units, there's a unique B -> C making the diagram commute. Does this have data?

#### Kevin Buzzard (Jan 15 2019 at 09:04):

Universal property is more than isomorphism, it's unique isomorphism.

#### Kenny Lau (Jan 15 2019 at 09:04):

of course this has data

?

#### Johan Commelin (Jan 15 2019 at 09:04):

But modulo choice it doesn't

#### Reid Barton (Jan 15 2019 at 09:21):

The data is the unique B -> C that fits

#### Reid Barton (Jan 15 2019 at 09:21):

Right, it's constructively data but classically a property, because we also assert that it is unique

#### Kenny Lau (Jan 15 2019 at 09:22):

I think we really need a typeclass that is nonempty + subsingleton

#### Kenny Lau (Jan 15 2019 at 09:22):

and another that is inhabited+subsingleton

#### Kevin Buzzard (Jan 15 2019 at 09:25):

You can't make the map constructively unless you have an explicit inverse for your units. I am unclear about whether as a mathematician I should even care about this discussion. For sure I want something that works if I just know abstractly that something is a unit

#### Kevin Buzzard (Jan 15 2019 at 09:26):

Generalising Kenny's argument one should have two definitions of unit as well -- existence of an inverse, and the inverse

#### Johan Commelin (Jan 15 2019 at 09:27):

Generalising Kenny's argument one should have two definitions of unit as well -- existence of an inverse, and the inverse

We do... there is units and is_unit, if I'm not mistaken.

#### Reid Barton (Jan 15 2019 at 09:34):

Good point about needing to have an actual inverse in order to construct the induced map constructively.
The good news is that any constructively reasonable definition will also be at least usable classically, because you can always conjure up the witness you need using choice. The question is what is most convenient.

#### Reid Barton (Jan 15 2019 at 09:35):

is_unit a is defined as ∃u:units α, a = u, the other version would be with a sigma instead of an exists

#### Reid Barton (Jan 15 2019 at 09:40):

Is the idea instead that if $f:A\to B$ and $S\subseteq A$ then we have a predicate which mathematically means that the induced $A$-algebra structure on $B$ is isomorphic to $A[1/S]$?

Aah! The penny has just dropped. Instead of the definition of the predicate being "B is isomorphic to the A[1/S] we constructed", it says "B satisfies the universal property we want". Is that the idea? We have predicates for universal properties?

In general this is the idea but in some cases you can also give an equivalent but more hands-on description of the predicate, e.g., R -> S being a quotient map of rings can be defined either in terms of a universal property or just as a surjective map.

#### Reid Barton (Jan 15 2019 at 09:58):

Another way of looking at this is that a map being of the form R -> R/I is something that is either true by definition or not, while a map being a quotient map is a theorem you can prove using any methods at your disposal.
The tradeoff is that it's not quite as convenient to use the quotient map hypothesis because you need to pass it to the place it is used, while Lean "just knows" when a ring is defined as a quotient ring.

#### Kevin Buzzard (Jan 15 2019 at 10:38):

The analogue of is_surjective in the localisation situation is not something I think I can write down without simply saying something like "image of $S$ lands in the units, and induced map from concrete localisation is a bijection". Is such a predicate useful?

#### Mario Carneiro (Jan 15 2019 at 11:27):

You can't directly use the universal property as the definition, because of universe issues (it can't quantify over all universes), so you have to find an "internal" characterization roughly equivalent to the construction itself

boggle

#### Kevin Buzzard (Jan 15 2019 at 11:28):

How about "is isomorphic to Kenny's explicit construction" then?

#### Chris Hughes (Jan 15 2019 at 11:28):

The is_quotient  class could include a truncated inverse to the quotient map.

#### Kevin Buzzard (Jan 15 2019 at 11:29):

I don't even want to use universes. How about I make everything in Type?

#### Mario Carneiro (Jan 15 2019 at 11:29):

I think for localization it is something like "there is a surjective map from A x S and some additional about it"

#### Kevin Buzzard (Jan 15 2019 at 11:30):

It's much worse than that

#### Kevin Buzzard (Jan 15 2019 at 11:30):

It's "it's what Kenny wrote when he defined localisation"

#### Mario Carneiro (Jan 15 2019 at 11:30):

you don't need the proofs though

#### Kevin Buzzard (Jan 15 2019 at 11:31):

but you probably need to spell out the equivalence relation again

#### Mario Carneiro (Jan 15 2019 at 11:31):

you may need the equivalence relation

#### Mario Carneiro (Jan 15 2019 at 11:31):

but there may also be a way to characterize it via ideals or something

#### Kevin Buzzard (Jan 15 2019 at 11:31):

Kenny's definition of $A[1/S]$ is a quotient of $A\times S$ by an equivalence relation.

#### Mario Carneiro (Jan 15 2019 at 11:31):

so that it looks more like a universal property

#### Kevin Buzzard (Jan 15 2019 at 11:32):

So the predicate we need is "it satisfies the universal property that the quotient by an equivalence relation satisfies"

#### Mario Carneiro (Jan 15 2019 at 11:32):

that is is_quotient the way we are going

#### Kevin Buzzard (Jan 15 2019 at 11:32):

Here $A\times S$ is little more than a monoid

#### Mario Carneiro (Jan 15 2019 at 11:33):

you might also be able to get away with just maps from A -> loc and S -> loc since it's a ring

#### Mario Carneiro (Jan 15 2019 at 11:34):

or just what you said - a ring hom A -> loc and an assertion that the image of S are units

#### Mario Carneiro (Jan 15 2019 at 11:39):

oh but you still have to say surjective using a map from A x S

#### Mario Carneiro (Jan 15 2019 at 11:45):

If you have that situation, and (s₁ * r₂ - s₂ * r₁) * t = 0 where t \in S, then mapping across f : A -> loc, you have (f s₁ * f r₂ - f s₂ * f r₁) * f t = 0 and f t is invertible so f s₁ * f r₂ = f s₂ * f r₁, and f s₁ and f s₂ are invertible so f r₁ / f s₁ = f r₂ / f s₂. So this direction is already provable. The other direction can be asserted: if f r₁ / f s₁ = f r₂ / f s₂ then there exists t \in S such that (s₁ * r₂ - s₂ * r₁) * t = 0

#### Neil Strickland (Jan 15 2019 at 15:49):

I have put some stuff about localization at
https://github.com/NeilStrickland/lean_comm_alg/blob/master/src/localization.lean
It is not finished, but I would be interested in comments on the general architecture.
The idea is to set things up so that you can make computable maps out of a localisation
if you have enough data, and you can make non-computable maps if you only have
existence statements, and as much stuff as possible is shared between the two cases.

#### Kevin Buzzard (Jan 15 2019 at 16:19):

So in your definition of is_localization you do not write "it satisfies the universal property", you instead write down some explicit ring-theoretic criterion following Mario's suggestion that such a criterion should exist.

#### Kevin Buzzard (Jan 15 2019 at 16:21):

Whilst I am no Lean expert, I am slightly worried about lines 102-120 because you are defining data in tactic mode, and I think that data constructed in this way usually turns out to be very unwieldy because tactic mode was not really designed for this. Possibly.

#### Patrick Massot (Jan 15 2019 at 16:22):

This is totally fake tactic mode, it could be rewritten as a term without any effort.

#### Patrick Massot (Jan 15 2019 at 16:23):

I think it also means that writing it as Neil did should be harmless

#### Kevin Buzzard (Jan 15 2019 at 16:24):

I totally agree that it's fake tactic mode. I was less sure than you about whether writing it as Neil did would be harmless.

#### Kevin Buzzard (Jan 15 2019 at 16:24):

I checked the maths and it seems to me that this does indeed characterise rings isomorphic to the localisation.

#### Kevin Buzzard (Jan 15 2019 at 16:25):

I am still a bit unclear as to why one can't just write "it satisfies the universal property", but I've seen this sort of thing be problematic before.

#### Kevin Buzzard (Jan 15 2019 at 16:26):

def submonoid_ann (S : set A) [is_submonoid S] : ideal A :=
{ carrier := λ a, ∃ as : ann_aux S, as.1.1 = a,
zero := ⟨ann_aux.zero S,rfl⟩,
smul := λ a _ ⟨⟨⟨b,t⟩,eb0⟩,rfl⟩, ⟨ann_aux.smul S a ⟨⟨b,t⟩,eb0⟩,begin rw ann_aux.smul,refl,end⟩
}


#### Kevin Buzzard (Jan 15 2019 at 16:29):

Oh, everything other than carrier is a prop anyway, so i'm really fussing about nothing.

#### Mario Carneiro (Jan 15 2019 at 16:36):

By the way, regarding getting this is_localization information around, it can easily be a typeclass (with a not so interesting search problem) and so get this data to where it needs to be

#### Mario Carneiro (Jan 15 2019 at 16:38):

Note that has_denom_data is a bit problematic because it is not a subsingleton

#### Kevin Buzzard (Jan 15 2019 at 16:45):

def is_localization_initial
(hf : is_localization_data S f) (g : A → C) [is_ring_hom g] (hg : inverts_data S g)
: B → C :=
begin
intro b,
rcases (hf.has_denom b) with ⟨⟨s,a⟩,e⟩,
rcases (hg s) with ⟨gsi,e3⟩,
exact (g a) * gsi,
end


Here's another place (the only other place?) where Neil uses tactics to define data.

#### Patrick Massot (Jan 15 2019 at 16:49):

This is even more fake tactic

#### Neil Strickland (Jan 15 2019 at 16:52):

I hadn't heard this kind of deprecation of tactics-for-data before. It seems to me to be a very natural translation of how I would write definitions in ordinary mathematics. Is there something that I am missing?

#### Mario Carneiro (Jan 15 2019 at 16:53):

tactics tend to produce ugly proof terms, which is fine for proofs (well not really, but that's another discussion) and causes problems for defs, because defs are later unfolded and their definitions matter

#### Mario Carneiro (Jan 15 2019 at 16:54):

Some tactics are fine and produce exactly what you expect, like exact and intro, while things like rw and simp are hell to work with

#### Kevin Buzzard (Jan 15 2019 at 16:54):

def is_localization_initial'
(hf : is_localization_data S f) (g : A → C) [is_ring_hom g] (hg : inverts_data S g)
: B → C := λ b, g (hf.has_denom b).1.2 * (hg (hf.has_denom b).1.1).1


This is what I would have written. But I don't understand things well enough to know whether it makes a difference.

#### Kevin Buzzard (Jan 15 2019 at 16:55):

Because Neil only used intro, rcases and exact maybe it doesn't matter.

#### Mario Carneiro (Jan 15 2019 at 16:56):

rcases and cases will use the corresponding cases_on recursor, which is sometimes what you want and sometimes not. We often prefer to use projections when applicable, as in Kevin's version

#### Kevin Buzzard (Jan 15 2019 at 16:57):

Neil -- the bottom line is that the sorries you have at the end of the file -- if they are easier to fill in using my suggestion then this is why my suggestion is better, and if they aren't then I'm talking nonsense :-)

#### Mario Carneiro (Jan 15 2019 at 16:58):

You could also use let ⟨⟨s,a⟩,e⟩ := hf.has_denom b in ... in place of the rcases application, which is more or less the same but produces an auxiliary definition that you can unfold on command. Sometimes this is good, sometimes not

#### Patrick Massot (Jan 15 2019 at 16:58):

def is_localization_initial
(hf : is_localization_data S f) (g : A → C) [is_ring_hom g] (hg : inverts_data S g)
: B → C :=
λ b, let ⟨⟨s,a⟩,e⟩ := (hf.has_denom b),
⟨gsi,e3⟩ := hg s in (g a) * gsi


#### Patrick Massot (Jan 15 2019 at 16:58):

Arg, Mario was faster

#### Patrick Massot (Jan 15 2019 at 16:59):

set_option eqn_compiler.zeta true

#### Patrick Massot (Jan 15 2019 at 17:00):

You can also put underscores instead of creating names you won't use

#### Kevin Buzzard (Jan 15 2019 at 17:01):

My definition unfolds to  g (((hf.has_denom b).val).snd) * (hg (((hf.has_denom b).val).fst)).val, Neil's to

subtype.cases_on (hf.has_denom b)
(λ (val : ↥S × A) (e : f ↑(val.fst) * b = f (val.snd)),
prod.cases_on val
(λ (s : ↥S) (a : A) (e : f ↑((s, a).fst) * b = f ((s, a).snd)),
subtype.cases_on (hg s) (λ (gsi : C) (e3 : g ↑s * gsi = 1), g a * gsi))
e)


#### Kevin Buzzard (Jan 15 2019 at 17:04):

Patrick's becomes

 is_localization_initial._match_2 S f g hg b (hf.has_denom b)


and is_localization_initial._match_2 becomes

 subtype.cases_on _a
(λ (val : ↥S × A) (property : f ↑(val.fst) * b = f (val.snd)),
prod.cases_on val
(λ (val_fst : ↥S) (val_snd : A) (property : f ↑((val_fst, val_snd).fst) * b = f ((val_fst, val_snd).snd)),
id_rhs C (is_localization_initial''._match_1 S g val_fst val_snd (hg val_fst)))
property)


#### Patrick Massot (Jan 15 2019 at 17:07):

What about the defeq equivalence classes?

#### Mario Carneiro (Jan 15 2019 at 17:07):

Patrick's and Neil's definitions should be defeq, but Kevin's is different

#### Neil Strickland (Jan 15 2019 at 17:08):

So I have some visible instances of cases_on and you don't. My guess is that the framework for structures effectively defines fst and snd in terms of cases_on. But perhaps that's wrong. And even if it's right, perhaps it is somehow better to bury the call to cases_on deeper down. I don't feel that I understand the issues very well here.

#### Kevin Buzzard (Jan 15 2019 at 17:08):

Me neither, that's why I brought it up here.

#### Mario Carneiro (Jan 15 2019 at 17:09):

Technically the projections are defined in terms of cases_on, but they are buried really deep and lean has special support for them

#### Kevin Buzzard (Jan 15 2019 at 17:09):

The rcases tactic is getting from <b,c> to b and c using cases_on, whereas my direct approach is going from a:=<b,c> to b using a.1. But you're saying that a.1 is defined using cases_on anyway?

#### Mario Carneiro (Jan 15 2019 at 17:10):

But it is useful to do the cases late rather than at the beginning because then you can prove things about the shape of the expression even when it's not a pair or whatever

#### Mario Carneiro (Jan 15 2019 at 17:11):

To take a simpler example, we've discussed the difference between the definitions

prod.map (f : A -> C) (g : B -> D) : A x B -> C x D | <a, b> := <f a, g b>


and

prod.map (f : A -> C) (g : B -> D) : A x B -> C x D := \lam p : A x B, <f p.1, g p.2>


#### Mario Carneiro (Jan 15 2019 at 17:13):

The advantage of the second definition is that prod.map f g p already unfolds to a pair, while the first definition does not

#### Mario Carneiro (Jan 15 2019 at 17:13):

In both cases prod.map f g <a, b> = <f a, g b> is definitional

#### Mario Carneiro (Jan 15 2019 at 17:14):

So as an application (prod.map f g p).1 = f p.1 is definitional only with the second definition

#### Kevin Buzzard (Jan 15 2019 at 17:43):

instance (hf : is_localization_data S f) (g : A → C) [is_ring_hom g] (hg : inverts_data S g) :
is_ring_hom (is_localization_initial S f hf g hg) :=
{ map_one := begin
unfold is_localization_initial,
rcases (hf.has_denom 1) with ⟨⟨s,a⟩,h⟩,
show g a * (hg s).val = 1,
change f s * 1 = f a at h,
rw mul_one at h,
have h2 := (hg s).property,
have h3 : a - s ∈ ker f,
show f (a - s) = 0,
rw is_ring_hom.map_sub f,
rw h,
rw sub_self,
suffices : g a = g s,
rw this; exact h2,
have h4 := hf.ker_eq,
rw h4 at h3,
cases h3 with t Ht,
rcases t with ⟨⟨b,t⟩,h5⟩,
change b = a - s at Ht,
change b * t = 0 at h5,
rw Ht at h5,
rw sub_mul at h5,
rw sub_eq_zero at h5,
have h6 : g (a * t) = g (s * t),
rw h5,
rw is_ring_hom.map_mul g at h6,
rw is_ring_hom.map_mul g at h6,
rcases hg t with ⟨u,hu⟩,
calc g a = g a * 1 : by rw mul_one
...      = g a * (g t * u) : by rw hu
...      = (g a * g t) * u : by rw mul_assoc
...      = (g s * g t) * u : by rw h6
...      = g s * (g t * u) : by rw mul_assoc
... = g s : by rw [hu,mul_one]
end,
...


@Kenny Lau can you do any better?

My bet: yes.

#### Kevin Buzzard (Jan 15 2019 at 17:44):

I wondered whether he would just answer "yes" and leave it at that :-)

#### Chris Hughes (Jan 15 2019 at 17:45):

Technically the projections are defined in terms of cases_on, but they are buried really deep and lean has special support for them

Why doesn't this work?

example {α β : Type} (x : α × β) : x.fst = prod.rec (λ a b, a) x := rfl -- doesn't work


#### Kevin Buzzard (Jan 15 2019 at 17:45):

The question boils down to proving that if $f(a)=f(s)$ then $g(a)=g(s)$, which looks suspicious until you realise that we know something about the kernel of $f$, namely that $t(a-s)=0$ for some $t\in S$; the fact that $g(t)$ is also a unit is what gets us home.

#### Kevin Buzzard (Jan 15 2019 at 17:47):

Actually I think Kenny would far rather refactor my proof than write his own.

#### Gabriel Ebner (Jan 15 2019 at 18:06):

@Chris Hughes Lean has two type checkers: the kernel and the type context. The kernel is the small low-level one, and the type context is the high-level one used for tactics, etc., which also supports unification, type class inference, etc. The kernel only does the final check when you add a theorem to the environment. Now, the kernel knows that prod.fst is defined in terms of rec, but the type context pretends projections are opaque definitions that only reduce when applied to the mk constructor. With a bit of creativity (i.e., circumventing the type context), you can still prove your example using just rfl:

run_cmd tactic.add_decl \$ declaration.thm prod.fst_def []
(∀ α β : Type, ∀ x : α × β, x.fst = prod.rec (λ a b, a) x)
(pure (λ α β : Type, λ x : α × β, eq.refl x.fst))
attribute [_refl_lemma] prod.fst_def

#print prod.fst_def


#### Kenny Lau (Jan 15 2019 at 18:10):

@Kevin Buzzard mwe?

#### Kevin Buzzard (Jan 15 2019 at 18:11):

Ramon and me just isolated a lemma, and we now know how to prove is_ring_hom (is_localization_initial S f hf g hg)

#### Kevin Buzzard (Jan 15 2019 at 18:16):

The lemma is that if is_localization_data S f and inverts_data S g then $f(a)=f(b)\implies g(a)=g(b)$

#### Kevin Buzzard (Jan 15 2019 at 18:18):

and the proof is that $a-b$ is in the kernel of $f$ so by ker_eq on $f$ we know $s(a-b)=0$ for some $s\in S$; hence $g(sa)=g(sb)$, but we can cancel $g(s)$ because of inverts_data S

#### Kevin Buzzard (Jan 15 2019 at 18:18):

Everything now follows after some algebra

#### Kevin Buzzard (Jan 15 2019 at 18:54):

@Kevin Buzzard mwe?

@Kenny Lau -- what is going on here is that Neil has defined a predicate is_localisation f S where f:A -> B and S : set A; the predicate is true iff B is isomorphic to A[1/S]. I just wanted to write the universal property (for all C, if I have h:A -> C such that h(s) is invertible for all s then there's a unique B -> C making the diagram commute) but Mario seems to think that there are universe issues with this approach. Neil has taken a completely different approach, noting that given f : A -> B and the hypothesis that f(s) is a unit for all s in S implies that there's a map A x S - >B sending (a,s) to f(a)/f(s). The claim is that B = A[1/S] in the maths sense iff this map A x S -> B is surjective and the kernel of f : A -> B is the a such that there's s with a*s=0. This is not proved in the file but looks OK to me -- the hypothesis gives a map A[1/S] -> B, the surjectivity claim implies it's surjective, and the kernel claim implies that it's injective.

#### Kevin Buzzard (Jan 15 2019 at 18:57):

I think @Ramon Fernandez Mir might fill in the proofs. I guess we also need that A -> loc A S satisfies the predicate -- this might be something which would be easier for you to do.

#### Chris Hughes (Jan 15 2019 at 18:58):

The universal property is actually more like (forall u: universe, forall C : Type u, ...), but this predicate isn't definable in Lean, so you have to find an equivalent things that doesn't quantify over universes.

#### Kevin Buzzard (Jan 15 2019 at 18:59):

Right -- so I just want to quantify over the universe that A and S are in.

#### Kevin Buzzard (Jan 15 2019 at 18:59):

Because that's what I do in real live maths in ZFC with no universes -- this "stick to one universe" approach doesn't usually cause me problems.

#### Reid Barton (Jan 15 2019 at 19:12):

Surely we can prove that the universal property for one universe (if chosen correctly) implies it for all universes, which is a statement we can write down because it only involves prefix quantification of universes, and we can apply it wherever needed when applying the universal property.
(The proof can be that we already constructed the localization within the original universe, so another candidate which has the universal property within that universe must be isomorphic to it, and we know the localization we constructed actually has the universal property for all universes.)

#### Kevin Buzzard (Jan 15 2019 at 19:25):

I just came here to say the same thing. What is wrong with this strategy? Somehow Neil's version seems cleaner though.

#### Reid Barton (Jan 15 2019 at 19:31):

The test case would be to prove that a composition of is_localization maps is is_localization

#### Reid Barton (Jan 15 2019 at 19:32):

which should be easy with the universal property

#### Neil Strickland (Jan 15 2019 at 19:38):

Here are some basic test cases:
1. Can we identity $A[a^{-1}][b^{-1}]$ with $A[(ab)^{-1}]$?
2. If $e^2=e$, can we identify $A[e^{-1}]$ with $A/(1-e)$?
3. If we define $\mathbb{Z}_{(p)}$ as a subring of $\mathbb{Q}$, can we produce the ring map $\mathbb{Z}_{(p)}\to\mathbb{Z}/p$?
I think that all of the maps implicit in these examples should be computable under very mild assumptions.

#### Mario Carneiro (Jan 15 2019 at 19:51):

there is nothing wrong with Reid's strategy, it's just less direct and possibly leads to worse defeqs

#### Kevin Buzzard (Jan 15 2019 at 19:57):

Neil's test 1 came up a lot in the schemes repo.

I guess the idea that everything should be proved constructively and then we just deduce the classical stuff from it.

#### Reid Barton (Jan 15 2019 at 19:57):

Yeah, if you want the constructive version then it's not as nice.

#### Mario Carneiro (Jan 15 2019 at 19:58):

Do we care about being constructive here? At the very least I would want any constructive version to be a subsingleton like fintype

#### Mario Carneiro (Jan 15 2019 at 19:59):

also, why the sudden focus on localization? I think the quotient case is far more prevalent and pressing

#### Mario Carneiro (Jan 15 2019 at 20:03):

I think the constructive version should use an indexed family rather than a set S

#### Mario Carneiro (Jan 15 2019 at 20:04):

That is, S should be the image of a monoid hom rather than a submonoid

#### Kevin Buzzard (Jan 15 2019 at 20:04):

because we're refactoring the schemes repo and we had just been trying to make sense of the stuff I wrote about universal properties of localisation, that's why I jumped on this. I had arranged to meet Ramon at 4pm today and Neil's post arrived shortly beforehand so I thought it was a really good time to understand this alternative approach. I think it's beautiful!

#### Kevin Buzzard (Jan 15 2019 at 20:05):

I think that S should be an arbitrary set, and we should localise at the monoid generated by S.

#### Mario Carneiro (Jan 15 2019 at 20:06):

I mean that for constructive purposes you want S to be enumerated by a concrete structure (the domain of the monoid hom). Predicates have no data

#### Kevin Buzzard (Jan 15 2019 at 20:06):

Neil was already doing this with $A[1/ab]$ etc. When I was doing schemes I had loc A S and then loc A (powers f) came up so much that Kenny made a bunch of lemmas for it. I am now beginning to wonder whether we should be working in this generality in general.

#### Mario Carneiro (Jan 15 2019 at 20:06):

Of course for powers f the indexing monoid is just N

#### Kevin Buzzard (Jan 15 2019 at 20:07):

I think that demanding that S is a monoid is a pain, because Neil wants me to check that f(s) is invertible for all s in S, and in the case S=<x> I only want to check that f(x) is invertible.

#### Kevin Buzzard (Jan 15 2019 at 20:07):

Sorry for over-use of f there.

#### Mario Carneiro (Jan 15 2019 at 20:08):

If S = <x> then the analogous monoid hom is \lam n, add_monoid.smul n x (which we know is a monoid hom, I think)

#### Kevin Buzzard (Jan 15 2019 at 20:09):

It also occurred to me that we could just set everything up with monoids, and then write different functions for arbitrary subsets. Mario is suggesting a different generalisation though.

#### Mario Carneiro (Jan 15 2019 at 20:19):

I think if we actually want to do this we should forget about computation for now, or until we have an actual application

#### Reid Barton (Jan 15 2019 at 20:30):

By the way, what happens in the noncommutative case? Is there anything to write down simpler than "the map from the localization is an isomorphism"?

#### Patrick Massot (Jan 15 2019 at 20:50):

The real test case for localization is decimal numbers. Can mathlib handle schoolkid maths?

#### Mario Carneiro (Jan 15 2019 at 20:55):

noncommutative fields of fractions are really complicated

#### Kevin Buzzard (Jan 15 2019 at 21:29):

Eew yeah. We number theorists had to learn this stuff about a decade ago when non-commutative Iwasawa theory became a thing.

#### Patrick Massot (Jan 16 2019 at 10:00):

Neil, your file has been Kennied™.

#### Neil Strickland (Jan 16 2019 at 10:14):

That's great, thanks to @Kenny Lau . I am also working on a slightly different framework which I will report on later.

#### Kevin Buzzard (Jan 16 2019 at 11:13):

Many thanks @Kenny Lau ! Neil, you might either find it instructive to see how Kenny rewired your code, or intimidating, depending on how much you can make sense of it I guess. Kenny will have liked your approach because he is at heart a constructivist.

#### Kevin Buzzard (Feb 05 2019 at 17:03):

@Kenny Lau @Neil Strickland I think that demanding that S is a submonoid of A is too restrictive. When I told Kenny to develop the theory of localisations of rings at multiplicative sets it was something like November 2017 and I knew nothing about Lean. I told him to assume S was multiplicative because that's what it says in the books. But I can localise A at an arbitrary subset S, just by localising at the monoid generated by S.

Kenny, when I delete is_submonoid S your code above breaks :-)

#### Neil Strickland (Feb 05 2019 at 17:24):

You can see the version that I am working on sporadically at https://github.com/NeilStrickland/lean_comm_alg/blob/master/src/localization_b.lean

• I did it for semirings rather than rings. There are some applications of that kind of thing in stable homotopy theory.
• I have a monoid S with a map i to the multiplicative monoid of R, rather than a submonoid. That's a structure that you want for log geometry anyway, and seems more natural for some other reasons as well.
• We can regard R × S as the set of unreduced fractions. This already has commutative and associative addition and multiplication, and the distributive laws fail in a well-controlled way. To make everything as computable as possible, there are some advantages to setting up this structure explicitly. So I do that.
• I did everything in a very bundled way. I felt forced to do that because of some technical issue about the way that things depend on the map i : S → R`, but I'm not sure I can reconstruct the details of that.
• If you want to localise with respect to something that is not a monoid, I think that it is better to do that as a separate construction layered on top of the monoid case.

There is plenty left to do but I haven't had time to look at it for a while. However, we will start running a working group in Sheffield next week, so I can maybe get some more people involved.

Last updated: May 18 2021 at 08:14 UTC