Scaling commutative diagrams.

Stream: mathlib4

[Kevin Buzzard]

There has been some talk recently about making a 4-variable version of IsScalarTower ("this triangle commutes"), corresponding to "this square commutes". The canonical example is when B/A is an extension of integral domains and L/K is the corresponding extension of their field of fractions. The reason one might want to bundle everything up into a structure IsCommSquare A B K L is that sometimes you want things like Gal(L/K) to act on B (e.g. if K,L are number fields with integer rings A,B), but typeclass inference won't let that happen without something gluing L and K to B.

I've been thinking about Frobenius elements recently and how to implement them in the right level of generality. Following a suggestion of Joel Riou I've been formalising a lemma from Bourbaki Comm Alg (note: in French), and part (b) of it involves a pair of commuting squares

B ---> B / P -----> K = Frac(B/P)
/\       /\        /\
|        |         |
|        |         |
A ---> A / p ----> k = Frac(A/p)

Here A,B are comm rings, P a prime ideal of B with preimage p, and k,K are the fields of fractions of A/p and B/P. This is now two commuting squares, and if you draw in some of the missing arrows then you get something like..erm.. 11(?) IsScalarTower instances (i.e. 11 pairs of composable morphisms), most of which we seem to use in practice in the proof, and most of which cannot be discovered by typeclass inference unless you explicitly put it in there.

I learnt from Jou Glasheen's FM24 project (and apparently she learnt this trick from Amelia) that if this diagram commutes then you don't need the assumption that the preimage of P is p, it follows from a diagram chase. Here's what that diagram chase looks like:

import Mathlib.RingTheory.Ideal.Pointwise
import Mathlib.RingTheory.Ideal.Over
import Mathlib.FieldTheory.Normal

open scoped algebraMap

-- Let A be a comm ring and let B be an A-algebra.
variable {A : Type*} [CommRing A]
  {B : Type*} [CommRing B] [Algebra A B]

/-
Mathematically I now want to say "let P be a prime ideal of B above p of A, and
let `k` and `K` be the fields of fractions of the integral domains `A/p` and `B/P`.

In diagrams:

B ---> B / P -----> K = Frac(B/P)
/\       /\        /\
|        |         |
|        |         |
A ---> A / p ----> k = Frac(A/p)

In Lean:
-/
-- first the objects for the LH square.
variable (P : Ideal B) [P.IsPrime] (p : Ideal A) [p.IsPrime]
  -- Use a trick I learnt from Jou and which she learnt from Amelia to encode
  -- `Ideal.comap (algebraMap A B) P = p` into the typeclass system:
  [Algebra (A ⧸ p) (B ⧸ P)] [IsScalarTower A (A ⧸ p) (B ⧸ P)] -- this implies p ⊆ P ∩ A
  -- Now draw in top line of RH square
  (K : Type*) [Field K] [Algebra (B ⧸ P) K] [IsFractionRing (B ⧸ P) K]
  -- It's convenient that `B` be a `K`-algebra but typeclass inference doesn't know this
  [Algebra B K] [IsScalarTower B (B ⧸ P) K]
  -- It's convenient that `K` is an `A/p`-algebra so make the triangle commute
  [Algebra (A ⧸ p) K] [IsScalarTower (A ⧸ p) (B ⧸ P) K]
  -- That's 5/6 of the objects and 3/4 of the area.
  -- now introduce k
  (k : Type*) [Field k] [Algebra (A ⧸ p) k] [IsFractionRing (A ⧸ p) k]
  -- Turns out that it's convenient for `k` to be an `A`-algebra
  [Algebra A k] [IsScalarTower A (A ⧸ p) k]
  -- Now draw the final edge
  [Algebra k K]
  -- and make the final triangle commute
  [IsScalarTower (A ⧸ p) k K]

  -- Turns out that we will need that other triangles commute.
  -- For example there are now maps A -> B/P -> K, A -> B -> K, A -> A/p -> K, A -> k -> K
  -- (all eight of these arrows are `Algebra` instances!)
  -- and all four pairs, when composed, give the same map A -> K but we don't have `Algebra A K` yet.

-- API, should probably be elsewhere
lemma obvious (x : A) : x ∈ p ↔ (x : A ⧸ p) = 0 := by
  change _ ↔ algebraMap A (A ⧸ p) x = 0
  simp only [Ideal.Quotient.algebraMap_eq, ← RingHom.mem_ker, Ideal.mk_ker]

-- Do we want lemmas like this? This says "If W -> X -> Y and X -> Y -> Z commute,
-- then Z is randomly a W-algebra, then W -> X -> Z commutes iff W -> Y -> Z does"
open IsScalarTower in
lemma isScalarTower_iff_isScalarTower_of_isScalarTower_isScalarTower
    (W X Y Z : Type*) [CommSemiring W] [CommSemiring X] [CommSemiring Y] [CommSemiring Z]
    [Algebra W X] [Algebra W Y] [Algebra W Z] [Algebra X Y] [Algebra X Z] [Algebra Y Z]
    [IsScalarTower W X Y] [IsScalarTower X Y Z] : IsScalarTower W X Z ↔ IsScalarTower W Y Z := by
  constructor
  · intro h
    apply IsScalarTower.of_algebraMap_eq
    intro w
    rw [algebraMap_apply W X Z, algebraMap_apply W X Y, algebraMap_apply X Y Z]
  · intro h
    apply IsScalarTower.of_algebraMap_eq
    intro w
    rw [algebraMap_apply W Y Z, algebraMap_apply W X Y, algebraMap_apply X Y Z]

-- Should I be proving that or adding it in our application as a hypothesis?

-- Let's now prove that the preimage of P is p; this follows from commutativity of the diagram.
open IsScalarTower in
-- we'd better now draw in that long diagonal and say that it commutes with *something*
example [Algebra A K] [IsScalarTower A k K] :
-- and now this means that there are three more IsScalarTower instances which we don't
-- have but which we will probably want.
    Ideal.comap (algebraMap A B) P = p := by
  ext x
  simp only [Ideal.mem_comap]
  rw [obvious, obvious]
  rw [← map_eq_zero_iff _ <| IsFractionRing.injective (A ⧸ p) k]
  rw [← map_eq_zero_iff _ <| IsFractionRing.injective (B ⧸ P) K]
  rw [← map_eq_zero_iff _ <| RingHom.injective ((algebraMap k K) : k →+* K)]
  simp only [Algebra.cast, Algebra.algebraMap_eq_smul_one]
  simp only [IsScalarTower.smul_assoc, _root_.smul_assoc]
  have : IsScalarTower A (B ⧸ P) K := by
    rw [← isScalarTower_iff_isScalarTower_of_isScalarTower_isScalarTower _ B _ _]
    apply IsScalarTower.of_algebraMap_eq
    intro a
    rw [algebraMap_apply A k K]
    rw [algebraMap_apply A (A ⧸ p) k]
    rw [← algebraMap_apply (A ⧸ p) k K]
    rw [algebraMap_apply B (B ⧸ P) K]
    rw [algebraMap_apply (A ⧸ p) (B ⧸ P) K]
    congr
    rw [← algebraMap_apply]
    rw [← algebraMap_apply]
  simp

I've tried to add details in case anyone actually cares or can significantly golf this. But basically my point is that the way I've got things set up here it's getting as bad as differential geometry ;-) (and that is not a good thing). Should I be considering bundling up stuff into "Let these 4 things be a commuting square", or just pressing on regardless? Note that I haven't even started the one page long proof yet: those 100 lines are just the set-up necessary to state part (b) of the theorem (in fact they're not enough because I haven't mentioned the group G in the lemma, but the G part is short).

[Yakov Pechersky]

Your obvious seems to be docs#Ideal.Quotient.eq_zero_iff_mem.

[Scott Carnahan]

Here's my attempt to restate part of your problem: you have a commutative diagram (of algebraMaps in this case), but typeclass inference needs a lot of handholding to recognize the commutativity of certain sub-diagrams.

[Kevin Buzzard]

I'm not sure that typeclass inference is even the right tool for keeping track of all ten or so assertions of the form "the algebra maps from X to Y, from Y to Z and from X to Z are compatible" because some proofs of statements like this are of the form "true for (X,Y,T) and (Y,T,Z) and (X,T,Z) hence true" and typeclass inference doesn't want to go on a wild goose chase looking for T in case it's not there.

[Adam Topaz]

This is where we need some custom tactics and metaprogramming. Something that could look at some diagram encoded as a graph, and generate algebra and/or scalar tower instances on the fly as they’re needed. This algebraize tactic from the AIM workshop is a small step toward something like this!

[Calle Sönne]

Adam Topaz said:

This is where we need some custom tactics and metaprogramming. Something that could look at some diagram encoded as a graph, and generate algebra and/or scalar tower instances on the fly as they’re needed. This algebraize tactic from the AIM workshop is a small step toward something like this!

Yes, it wouldn't be too hard to let it accept a CommSq of RingHoms and add all possible IsScalarTower instances. But then one would need to have the individual ringhoms instead of the algebra instances as parameters, which maybe is not ideal. I think that developing API forIsCommSquare A B K L sounds like a good idea, as this situation is surely common enough.

[Johan Commelin]

So maybe we should have a smart_goose_chase tactic that we can call at the beginning of a proof?

[Johan Commelin]

And it will add all those scalar tower instances, starting from the 4 "fundamental" triangles?

[Johan Commelin]

But you would still need 11 algebra instances?

[Johan Commelin]

ooh, I guess there are 6 fundamental triangles... also the horizontal pairs

[Kevin Buzzard]

My instinct, which I'll be refining on the 15 hour flight that I'm about to get on, is that one commutative square is two scalar tower triangles, and my diagram is two commutative squares (not three) and hence four scalar towers (not six or 11).

Part of the argument I'm formalising involves the assertion "WLOG p is maximal because just localise duh", and it will be interesting to see how many hundreds of lines of code this spirals into (I'll need to make several more commuting squares). I suspect this will teach me a lot!

[Johan Commelin]

It is 6 because you need two scalar towers to encode the horizontal rows

[Kevin Buzzard]

Right -- I only added them because I could see that they were there. Right now I only formalised the statements of things I wanted and I'm not 100% sure exactly for which pairs (X,Y) I want to be able to explicitly claim that Y is an X-algebra. The bare minimum is the seven arrows in the diagram. And then right now you also need the two diagonals of the squares in order to use IsScalarTower to assert that the diagram commutes. But of course we only need these under the assumption that we want typeclass inference to know that the square commutes, there are other ways to say this, eg some tactic which creates coercions between any two objects in the diagram which can be reached by composing explicit arrows, without creating algebra instances. The design space seems quite big to me.

[Eric Wieser]

Johan Commelin said:

And it will add all those scalar tower instances, starting from the 4 "fundamental" triangles?

This might not help if the instances are needed in the statement

[Kevin Buzzard]

That's a good point!

[Yaël Dillies]

Sounds like you want a macro taking in a commutative diagram and spitting out the relevant IsScalarTower instances, in the same style as the [[VectorSpace K V]] notation

[Kevin Buzzard]

I think that instead of just moaning I might want to launch into some proofs and then see what's painful. The code above looks a bit hectic but if I can push the base change argument through then arguably we don't need any new tooling

[Eric Wieser]

Yaël Dillies said:

Sounds like you want a macro taking in a commutative diagram and spitting out the relevant IsScalarTower instances, in the same style as the [[VectorSpace K V]] notation

Or maybe variable_for_diagram <some ASCII art>

[Eric Wieser]

Maybe another good option here is to have something that generates a structure for a given diagram, which bundles all the types. Typeclass search would then be happy to find IsScalarTower s.A s.B s.C etc

[Adam Topaz]

What I envision wouldn’t add all possible instances, but would let you add only the instances you need when you need them.

[Adomas Baliuka]

Yaël Dillies said:

the [[VectorSpace K V]] notation

Is there documentation about this notation? I haven't been able to find anything.

[Ruben Van de Velde]

It doesn't exist (yet?)

[Kim Morrison]

It is variable?:

import Mathlib

@[variable_alias]
structure VectorSpace (k V : Type*) [Field k] [AddCommGroup V] [Module k V]

variable? [VectorSpace K V]