commutative squares

Stream: mathlib4

[Kevin Buzzard]

IsScalarTower is the way of telling the typeclass inference system that we have a commuting triangle of commutative rings. The "AKLB set-up" (notation commonly used when L / K is a finite Galois extension of number fields, A is the algebraic integers of K and B is the algebraic integers of L) is similarly a way of carrying round a commutative square of ring morphisms. But then this:

import Mathlib.GroupTheory.GroupAction.Defs

-- notation "AKLB" is taken from this 2017 MIT course
--  https://mitocw.ups.edu.ec/courses/mathematics/18-785-number-theory-i-fall-2017/lecture-notes/
-- (see lecture 5)
/-
     K ----> L
     /\      /\
     |       |
     A ----> B
-/
class IsAKLB (A K L B : Type*) [SMul A B]
  [SMul A K] [SMul B L]
  [SMul K L] [SMul A L]
  extends IsScalarTower A B L, IsScalarTower A K L where -- error
/-
parent field type mismatch, field 'smul_assoc' from parent 'IsScalarTower' has type
  ∀ (x : A) (y : K) (z : L), (x • y) • z = x • y • z : Prop
but is expected to have type
  ∀ (x : A) (y : B) (z : L), (x • y) • z = x • y • z : Prop
-/

[Joël Riou]

The two IsScalarTower both have a smul_assoc field, so that you should probably do something like:

class IsAKLB (A K L B : Type*) [SMul A B] [SMul A K] [SMul B L] [SMul K L] [SMul A L] where
  isScalarTowerABL : IsScalarTower A B L := by infer_instance
  isScalarTowerAKL : IsScalarTower A K L := by infer_instance

[Joël Riou]

(But, it is unclear this would be useful as we cannot make isScalarTowerABL an instance because it depends only on the three rings A, B, L, and not on K.)

[Kevin Buzzard]

I am very interested to see where we need all of the AKLB set-up here. Jou claimed she needed for docs#galRestrictHom but I bet that works with L ->_a[A] L rather than L ->_a[K] L and I bet they're the same.

@Andrew Yang how much of RingTheory.IntegralRestrict goes through if you replace [FiniteDimensional K L] by the assumption that $L/K$ is algebraic? I suspect that all the galrestrict stuff will be fine.

[Andrew Yang]

I'm not aware of a definition of field norm or trace for infinite extensions, but yes RingTheory.IntegralRestrict only needs algebraicity.

[Kevin Buzzard]

oh yeah I wouldn't expect norms and traces to work.

[Andrew Yang]

file#Mathlib/RingTheory/DedekindDomain/Different is one place where the AKLB setup is actually needed.

[Joël Riou]

I was thinking that if a finite group G acts on a commutative ring B in such a way that A identifies to the subring of B fixed by G, then the topological space Spec(A) is the quotient of Spec(B) by the action of G (SGA 1 V 1.1, which refers to Bourbaki). In particular, G acts transitively on the prime ideals of B over a given prime ideal of A. Also, given q over p, the residual extension is quasi-Galois, and the decomposition group surjects onto the residual Galois group (which also gives the existence of Frob). Still, Bourbaki assumes G is finite.