Notation for group(module,ideal) quotients

Stream: maths

[Anne Baanen]

I am currently dealing with quotients of the form I^i / I^e modulo I^(i+1) / I^e, and the result is completely unreadable types. What do we think about introducing notation along the following lines:

• G /ᵍ H is docs#quotient_group.quotient
• A /ᵃ B or A /⁺ B is docs#quotient_add_group.quotient
• M /ᵐ N is docs#submodule.quotient
• R /ⁱ I is docs#ideal.quotient

And I guess for submonoids we can have:

• M /ᶜ c is docs#con.quotient
• M /ᶜ⁺ c or M /ᵃᶜ c is docs#add_con.quotient

[Johan Commelin]

Could a notation typeclass unify these?

[Johan Commelin]

Also, for your application, do you think life might become easier by reasoning with surjective maps and claims about what their kernels look like?

[Anne Baanen]

Johan Commelin said:

Could a notation typeclass unify these?

Hmm, that could probably work. The issue I foresee is that ideal.quotient is (reducibly) defined as submodule.quotient, which should probably be redefined in terms of add_group.quotient anyway. I don't know how much the elaborator will enjoy that.

[Johan Commelin]

class has_quotient {A : Type u} (B : Type v) [set_like A B] :=
(quotient : B → Type (max u v))

notation `G` /// `H` := @has_quotient.quotient G _ _ _ H

or something like that.

[Anne Baanen]

Johan Commelin said:

Also, for your application, do you think life might become easier by reasoning with surjective maps and claims about what their kernels look like?

Probably not much: I'm defining the ramification index and inertia degree of P over p, Following Neukirch 8.2 I want to show e * rank p.quotient P.quotient = rank p.quotient (P^e).quotient by considering the inclusions (P^e).quotient = map (P^e).quotient.mk (P^0) ≥ map (P^e).quotient.mk (P^1) ≥ ... ≥ map (P^e).quotient.mk (P^e) = ⊥. Since these are all p.quotient-linear and injective, it suffices (docs#dim_range_add_dim_ker, docs#dim_quotient_add_dim) to show the successive quotients (P^i / P^e) / (P^(i+1) / P^e) are isomorphic to P.quotient, which follows from the 3rd isomorphism theorem.

So I don't see how to avoid those quotients - without quotienting by P^e we can't talk about being p.quotient-linear, and the other quotient is needed to do the 3rd isomorphism theorem.

[Kevin Buzzard]

The 3rd isomorphism theorem just tells you that (P^i/P^e)/(P^{i+1}/P^e) is isomorphic to P^i/P^{i+1}. It's non-formal to show that this is R/P; this would not be true for a random UFD like $\R[X,Y]$ with $P=(X,Y)$.

[Anne Baanen]

Of course, in general this wouldn't be true. But everything should work out in a Dedekind domain :)

[Kevin Buzzard]

Yes indeed :-) Dedekind domains are smooth and 1-dimensional, that's the key thing.

[Kevin Buzzard]

One should really be doing this in a relative setting I guess? I think the FLT-regular people would like to know that if $L/K$ is a finite extension of number fields of degree $n$ then $\sum_i e_if_i=n$ where $P$ is a prime of $\mathcal{O}_K$ and $P\mathcal{O}_L$ factors as $\prod_i Q_i^{e_i}$.

[Anne Baanen]

I think my approach should work for that case if there are no unexpectedly hard sorrys. My statement goes: if L = Frac(S) is a finite separable extension of K = Frac(R), S is Dedekind and p : ideal R is maximal, then Σ P ∈ (factors pS).to_finset, multiplicity P pS * [S / P : R / p] = [L : K].

[Kevin Buzzard]

Oh great! I had misunderstood what you were doing! I had assumed p was a prime number not a prime ideal. Sorry to derail

[Kevin Buzzard]

This is wonderful because it will also apply to extensions of $p$-adic local fields.

[Anne Baanen]

Ah, I was already worried I had missed something in setting up my theory :P

[Kevin Buzzard]

Back to your question, being p.quotient-linear is the same as being R-linear and p happening to act as 0 everywhere. So you could just let everything be an R-module and then at the end when you're down to P^i/P^{i+1} then deduce that things are p.quotient-modules maps are p.quotient-linear. Does this help?

[Anne Baanen]

Johan Commelin said:

class has_quotient {A : Type u} (B : Type v) [set_like A B] :=
(quotient : B → Type (max u v))

notation `G` /// `H` := @has_quotient.quotient G _ _ _ H

or something like that.

I have implemented something like your suggestion, it looks like everything is working without issues: branch#quotient-notation.

[Eric Wieser]

I guess the nice thing about this is it forces G to be visible in the doc-gen type, rather than just showing H.quotient.

[Eric Wieser]

Do you even gain anything by assuming set_like there?

[Eric Wieser]

I think that might just make more work for typeclass inference without any gain

[Anne Baanen]

Not really I guess. Maybe it secretly helps out by forcing A to be an out_param :P

[Eric Wieser]

You don't even need A if you remove set_like

[Anne Baanen]

Yes, but then it won't appear in the notation anymore!

[Eric Wieser]

That's probably worth a comment explaining the motivation when you PR it

[Anne Baanen]

I would also like to keep the A for Lean-technical reasons: if we create a class of "set_likes extending add_subgroup" so we can uniformly define all the quotients listed above, we can't deduce A from the structure of B anymore.

[Anne Baanen]

That is, I think it would be neat to have

@[to_additive]
class subgroup_class S G extends set_like S G := ...

@[to_additive]
instance [subgroup_class S G] : has_quotient S G := <current subgroup.quotient implementation>

and then we can transfer results from quotient groups to quotient modules with a lot less friction.

[Johan Commelin]

That sounds promising!