triggering `is_scalar_tower`

Stream: maths

[Kevin Buzzard]

In this code I have L a K-algebra and then given some auxiliary data I construct an L-algebra M. Lean seems to be happy to make M into a K-algebra but I was expecting the is_scalar_tower instance to be there too (assuming it did the only thing it could have done to make M a K-algebra).

import field_theory.splitting_field

universes u v

variables (K L : Type) [field K] [field L] [algebra K L]

example (p : polynomial L) : (0 : K) = 1 :=
begin
  let M := p.splitting_field,
  have : algebra K L := infer_instance,
  have : algebra L M := infer_instance,
  have : algebra K M := infer_instance, -- all three work
  have : is_scalar_tower K L M := infer_instance, -- fails
  sorry,
end

[Kevin Buzzard]

Oh! Examining things further the algebra K M instance is coming from something specific to splitting field, so I can just add the instance myself here.

[Kevin Buzzard]

What does "this" refer to on the first line of this comment? Is this something which didn't used to be an instance but is now an instance?

[Kevin Buzzard]

docs#polynomial.splitting_field.algebra' is giving the algebra K M instance and the map seems to be a strange one.

So splitting_field_aux f with f : polynomial K gets given the structure of an R-algebra for any R such that algebra R K. This looks to me like it's part of an implementation detail. But by the time we've got to splitting_field f surely we just want the structure of a K-algebra, and then everything else induced from that? Or not?

So in fact this is my question:

import field_theory.splitting_field

/-
@[instance]
protected noncomputable def
polynomial.splitting_field.algebra' :
  Π {K : Type u_1} [_inst_1 : field K] (f : polynomial K) {R : Type u_2} [_inst_4 : comm_semiring R]
  [_inst_5 : algebra R K], algebra R f.splitting_field
-/

variables {K : Type*} [field K] (f : polynomial K) {R : Type*} [comm_semiring R]
  [algebra R K]

instance : is_scalar_tower R K f.splitting_field :=
sorry -- compiles

[Kevin Buzzard]

Am I doing this right?

local attribute [-instance] polynomial.splitting_field.algebra'

def algebra.comp {K L M : Type*} [field K] [field L] [field M] [algebra K L] [algebra L M] :
  algebra K M :=
{ smul := λ k m, algebra_map L M (algebra_map K L k) * m,
  to_fun := λ k, algebra_map L M (algebra_map K L k),
  map_one' := by simp only [map_one],
  map_mul' := λ _ _, by simp only [map_mul],
  map_zero' := by simp only [map_zero],
  map_add' := λ _ _, by simp only [map_add],
  commutes' := λ a b, by simp only [mul_comm],
  smul_def' := λ r x, rfl }

local attribute [instance] algebra.comp

instance is_scalar_tower' {K L M : Type*} [field K] [field L] [field M] [algebra K L]
  [algebra L M] : is_scalar_tower K L M := ⟨λ x y z, begin
    simp only [algebra.smul_def],
    rw (show ∀ k, algebra_map K M k = algebra_map L M (algebra_map K L k), from λ k, rfl),
    simp only [map_mul, mul_assoc],
  end⟩

I suspect that either we have this or for some reason we don't want it...

[Kevin Buzzard]

Oh OK the linter is telling me what the problem is :-/

[Eric Wieser]

Don't use have for algebra, it throws away the data for the duration of the tactic block

[Eric Wieser]

Which means when you come to look for is_scalar_tower, you're asking lean "Do the actions of [algebra you're not allowed to know the definition of] and [algebra you're not allowed to know the definition of] commute"

[Kevin Buzzard]

Oh those have were precisely not to start adding things that were there already

[Eric Wieser]

Kevin Buzzard said:

What does "this" refer to on the first line of this comment? Is this something which didn't used to be an instance but is now an instance?

I have no idea what I was thinkign there (in #10220). I can only assume I intended to make that not an instance

[Eric Wieser]

Your algebra.comp can be implemented in one line with docs#restrict_scalars.algebra

[Eric Wieser]

Kevin Buzzard said:

So in fact this is my question:

The answer is

import field_theory.splitting_field

variables {K : Type*} [field K] (f : polynomial K) {R : Type*} [comm_semiring R]
  [algebra R K]

instance : is_scalar_tower R K f.splitting_field :=
polynomial.splitting_field_aux.is_scalar_tower _ _ _ _

[Kevin Buzzard]

Is there anything else like splitting_field f? What is the logic of giving a K-algebra some obscurely-defined algebra structure over any field for which K is an algebra over that field?

[Anne Baanen]

The reasoning behind these algebra R A → algebra R (some_construction_of A) instances is that we ideally want algebra to be closed under transitivity. For example, when showing the trace of an integral element is integral we have a tower of extensions F / L / R and take the algebraic closure of F. We want to talk about the inclusion algebra_map L (algebraic_closure F), which would be the composition of the maps L → F and F → algebraic_closure F and exists because of docs#algebraic_closure.algebra which is one of these left-hand-side-free instances.

[Eric Wieser]

I think the logic for defining the R-algebra this way on splitting_field was that the R-algebra almost comes for free when building the K-algebra

[Eric Wieser]

I think originally I was hoping it would resolve the nat/int diamonds described in the comment linked earlier, but it does not.

[Kevin Buzzard]

The R-algebra structure on the splitting field comes for free because the splitting field is a K-algebra and there's a map R->K. But the same statement is true for any K-algebra!