action of Galois groups / "univalence" / auto-generate thms?

Stream: Is there code for X?

[Kevin Buzzard]

I've been talking to @Suryansh Shrivastava about their work on Stickelberger elements etc whilst visiting IISc. To state Stickelberger's theorem one needs an action of Galois groups on class groups, and my instinct on how this would work is that one should prove that class groups are functorial under isomorphisms. So something like this:

import number_theory.cyclotomic.gal
import ring_theory.class_group

def foo (R : Type) [comm_ring R] [is_domain R] (S : Type) [comm_ring S] [is_domain S]
  (e : R ≃+* S) : (class_group R) ≃* (class_group S) := sorry

--lemma foo_id : foo R R equiv.refl = equiv.refl
--lemma foo_comp : (foo R S eRS).comp (foo S T eST) = foo S R (eRS.comp eST)

def bar (L : Type) [field L] [number_field L] (M : Type) [field M] [number_field M] (e : L ≃+* M) :
  number_field.ring_of_integers L ≃+* number_field.ring_of_integers M := sorry

-- bar_id, bar_comp

Once one has this one can get an action of Gal(L/K) on the class group of (the integers of) L (whenever this makes sense, e.g. if $K\subseteq L$ are number fields), because an element of the Galois group is an automorphism of L, so induces an automorphism of the integers of L, so induces an automorphism of the class group, and the fact that id and comp are true give you that the action is a group action. Are these the kinds of definitions/theorems things which we can generate automatically or do they have to be written as boilerplate? I guess one would also need non-formal statments of the form "if g : L \iso M induces g_* : O_L -> O_M then the obvious square commutes" and "if g : R \iso S" sends ideal I to ideal J then g_* sends class of I to class of J".

[Alex J. Best]

We have

/-- The class group of `R` is isomorphic to that of `S`, if `R` is isomorphic to `S`. -/
noncomputable def class_group.congr {R : Type u} {S : Type v}
  [comm_ring R] [is_domain R] [comm_ring S] [is_domain S]
  (e : R ≃+* S) : class_group R ≃* class_group S

in the mordell project https://github.com/lean-forward/class-group-and-mordell-equation/blob/baba2049f3bfe4d2cc184f8205997333e7c58638/src/number_theory/class_number_computing.lean#L290 (with Anne, Sander and Nirvana)

[Eric Wieser]

I guess Kevin's id and comp claim would give you ring_aut R →* mul_aut (class_group R) as the homogeneous special case, which maybe gives the mul_action it sounds like Kevin is asking for?

[Reid Barton]

FWIW with univalence all this Galois action stuff just happens automatically.

[Adam Topaz]

Does univalence really save any work here? I have the impression that the definition of class_group itself in a univalent system would require essentially the same work as would be required to show what Kevin mentions in lean.

[Reid Barton]

The type of algebraic closures of K will have higher structure (its points L have automorphism groups Gal(L/K)), so any construction that takes as input an algebraic closure L will automatically acquire a Galois action by transport

[Adam Topaz]

Is it the right higher structure? It’s BG where G is the absolute Galois group as a profinite group. Does HoTT let you see such profinite things?

[Reid Barton]

I mainly mention this because Kevin sometimes says he only wants to regard "canonical" isomorphisms as equalities, but here the noncanonical isomorphisms (the nonidentity elements of Gal(L/K)) are also very useful to have.

[Reid Barton]

Oh I didn't notice we might be talking about a profinite group, then I would have to think more.

[Johan Commelin]

We need a type theory with condensed foundations...

[Reid Barton]

I guess you would get the right action of the underlying group, but you wouldn't know for free that the action was continuous, unless... yes what Johan said.

[Kevin Buzzard]

Can a machine construct these terms? The proof in the Mordell project is long but presumably content-free

[Reid Barton]

It can as long as the definitions of class_group etc. don't use choice in weird ways.

[Junyan Xu]

one should prove that class groups are functorial under isomorphisms.

This should work for any homomorphisms, not just isomorphisms. It's straightforward that R ↦ Pic (Spec R) is a functor from CommRing to AbelianGroup, and if R is a domain we have a canonical isomorphism class_group R ≃* Pic (Spec R). Note that Pic_Spec can be defined using R-modules without mentioning schemes or sheaves of modules. I was working towards the isomorphism for the purpose of elliptic curve reduction and I have simple informal proofs of some facts needed, which I can elaborate if people are interested in working on the formalization; otherwise I'll come back to formalize it after one week.

[Adam Topaz]

Reid Barton said:

The type of algebraic closures of K will have higher structure (its points L have automorphism groups Gal(L/K)), so any construction that takes as input an algebraic closure L will automatically acquire a Galois action by transport

I’m still not convinced whether univalence makes anything easier. Is it not the case that in order to even construct, say class_group in HoTT, that one would have to ensure some compatibility with this higher structure as part of the construction itself? It seems to me like the work required to construct the Galois action is just moved into the construction itself, but that it still exists.

[Reid Barton]

You don't have do anything to ensure this compatibility. Although you probably would want to work with things in a more bundled way.

[Reid Barton]

Everything is compatible with equality (just like in Lean), but now the equalities of the type Field are the isomorphisms of fields.

[Reid Barton]

So if you have a g : L = L where L : Field or L : FieldExt K or whatever, you can eq.rec it through fun F => class_group (number_field.ring_of_integers F) to get an equality of abelian groups (or whatever).

[Adam Topaz]

Okay, this I understand. But maybe the point I'm trying to make is that we will not be able to construct a function out of this type which is not compatible with isomorphisms of fields (because that IS equality), so it seems to me that there must be some work required when constructing a function out of this type that boils down (in some way which I don't understand) to verifying that something is compatible with isomorphisms. Something has to happen somewhere, but I don't understand where!

[Adam Topaz]

Anyway, the HoTT folks should just construct class_group.

[Reid Barton]

Adam Topaz said:

Something has to happen somewhere, but I don't understand where!

It happens in the metatheory, when constructing a model of HoTT. Or also in the implementation of the proof assistant itself, in cubical type theory.

[Reid Barton]

More specifically, since Field is built from the universe Type, it will have a higher path structure that is induced by the path structure of the universe. The problem is to identify the path types of the universe with something useful (isomorphisms). That is postulated in book HoTT (but there is a simplicial set model that shows soundness), or given a computational interpretation in cubical HoTT.

[Reid Barton]

If we built Field by manually "putting in" the field isomorphisms as the higher structure somehow, then you're right that constructions that use a Field would need to also specify what they do on those isomorphisms.

[Trebor Huang]

For path structures to also carry topological information, we have cohesive homotopy type theory

[Johan Commelin]

@Trebor Huang But is that cohesion doing the right thing in the case of profinite groups? That's not so clear to me.

[Kevin Buzzard]

Topological spaces are not a Cartesian closed category and so currying gives the wrong answer. I don't know if this is relevant but my experience working with univalent people is that many of them are not really interested in the questions I'm interested in, they have their own research program. My feeling is that the only way one can answer questions such as "is this easier or harder in a univalent theory" is to find someone interested in both univalence and class groups, and this seems hard.

What I really want to know is whether I have to write these functions above (or more precisely the one which the Mordell people didn't write) or whether some tactic can do it for me.

[Yaël Dillies]

How many such functions are there?

[Kevin Buzzard]

This is what Mario always says and it seems that there aren't that many. Maybe more will show up when we start doing Galois representations but at the end of the day I bet it's dead easy to write these things manually, which of course is an argument against automation. The reason we need to_additive is that there are 500 applications not 5

[Mario Carneiro]

note that making it easy (or at least straightforward) to write these manually is actually a prerequisite for making automation that does it

[Kevin Buzzard]

I remember doing this once when proving that if R and S were isomorphic rings and R was a UFD then so was S. It took a while but I never had to move my brain, it was just a case of proving all the sublemmas of this form first.

[Kevin Buzzard]

Here was the boilerplate I wrote at the time. Note that other than the last example (which was the motivation for proving UFD transfers along isomorphisms) every other lemma is just transferring mathematically sensible predicates along isomorphisms.

[Reid Barton]

This is possible and the way to do it is to understand what the HoTT people are doing. It's on my to do list but it's not likely to happen before the port.

[Trebor Huang]

So a trivial observation is: There cannot be (even in the form of tactics) a way in Lean to transfer every property along an isomorphism. For instance, the property of being equal to A cannot be transferred, or else it would already imply univalence!

[Eric Wieser]

If you're talking about (= A) where A : Type, then that property is pretty much never meaningful in lean anyway. It's not even possible to state unless A and B are in the same universe.

[Reid Barton]

Right, Lean lets you say some "bad things" that can't be transferred automatically, but most definitions won't use them (precisely because they are not mathematically meaningful in the first place), and most of the ones that do should be fixable without too much work.

[Pedro Sánchez Terraf]

Kevin Buzzard said:

I remember doing this once when proving that if R and S were isomorphic rings and R was a UFD then so was S. It took a while but I never had to move my brain, it was just a case of proving all the sublemmas of this form first.

Hasn't this issue come up in combinatorics already? (honest question, out of curiosity--if you understand my poor grammar). I mean, there are a lot of combinatorial proofs that involve changing the "base set", and in this case one would need transport along bijections.

[Eric Wieser]

It's pretty common in these cases that a bijection is overkill and an injection/surjection alone will suffice

[Kevin Buzzard]

Yes -- and the same thing is going on here. For example an injection of number fields gives you an injection of the ring of integers (and this should be in the library and it's not formal univalence nonsense) and similarly Junyan explained that class groups should also be functorial for a more general class of maps, but I'm not sure that our definition is, because "field of fractions" is well known not to be functorial (it doesn't sheafify well, there are several famous errors in the literature concerning this). For example the surjection Z -> Z/2 doesn't give rise to a ring map Q -> Z/2.

[Trebor Huang]

Reid Barton said:

Right, Lean lets you say some "bad things" that can't be transferred automatically, but most definitions won't use them (precisely because they are not mathematically meaningful in the first place), and most of the ones that do should be fixable without too much work.

This following paper may be of interest, as it established what kinds of properties can be transferred by tactics along isomorphisms. A quote from the author:

I've worked on this "metatheoretic univalence", see my paper https://arxiv.org/abs/2211.07487.
In short, you can transfer everything in MLTT+funext+UIP, as long as you don't have any function code : Type_n -> Tm(U_n) that gives the code of a type.

You cannot form the predicate (A = -) when A is a type, because (x = y) only makes sense when x and y are terms. Given code, you could write (code(A) =_{U_n} -).