Inserting into `is_scalar_tower`

Stream: Is there code for X?

[Kevin Buzzard]

I have rings $A\subseteq B\subseteq C\subseteq D$. The rings $A,B,D$ are given, and I can build $C$ as an $A$-subalgebra of $D$ which contains $B$. I'm now having trouble putting the finishing touches to the is_scalar_tower glue. Am I doing it wrong?

import field_theory.intermediate_field

constants (A B D : Type)
-- A ⊆ B ⊆ D
variables [comm_ring A] [comm_ring B] [comm_ring D]
  [algebra A B] [algebra B D] [algebra A D]
  [is_scalar_tower A B D]

-- I now have a ring C sitting between B and D, but defined initially
-- as sitting between A and D

constant C : subalgebra A D -- A ⊆ C ⊆ D; I will be thinking of C as a type not a term.

example : is_scalar_tower A B D := infer_instance
example : is_scalar_tower A C D := infer_instance -- so far so good

-- in fact I can prove B ⊆ C
lemma B_subset_C : (is_scalar_tower.to_alg_hom A B D).range ≤ C := sorry

-- need to build this somehow
noncomputable instance : algebra B C := ring_hom.to_algebra
((subalgebra.inclusion (B_subset_C)).comp
  ((is_scalar_tower.to_alg_hom A B D).range_restrict)) -- is this a bad idea?

-- this one I can do
instance : is_scalar_tower A B C := ⟨λ a b ⟨d, hd⟩, by simp⟩

-- this one I can't
example : is_scalar_tower B C D :=
⟨λ b ⟨c, hc⟩ d, begin
  sorry,
end⟩

[Eric Wieser]

is this a bad idea?

Both noncomputable and ring_hom.to_algebra are red flags to me, so I think yes

[Eric Wieser]

def C' : subalgebra B D :=
{ carrier := C,
  algebra_map_mem' := λ r, B_subset_C ⟨r, rfl⟩,
  ..C }

-- need to build this somehow
noncomputable instance : algebra B C :=
subalgebra.algebra C'

instance : is_scalar_tower A B C :=
(by apply_instance : is_scalar_tower A B C')

example : is_scalar_tower B C D :=
(by apply_instance : is_scalar_tower B C' D)

[Eric Wieser]

Saves you from having to prove anything

[Eric Wieser]

My guess is that the best answer is actually to just build C' directly, since you didn't mention where C came from

[Kevin Buzzard]

I make C as a sup (of objects including B), so it's coming from the lattice structure on subalgebra A D. I'm more than happy to do it this way! Your code makes me think that my C should be called C_aux and your C' should be my C. Is ring_hom.to_algebra a code smell? I hadn't realised.

[Eric Wieser]

docs#ring_hom.to_algebra is pretty much guaranteed to introduce a diamond in smul

[Eric Wieser]

Because it implements it as f r * x

[Eric Wieser]

Your code makes me think that my C should be called C_aux and your C' should be my C.

This sounds good to me

[Kevin Buzzard]

Hmm. In my use case I run into an exciting new problem:

import field_theory.normal
import field_theory.is_alg_closed.algebraic_closure

variables (L : Type) [field L]

noncomputable def middle_field : intermediate_field L (algebraic_closure L) := ⊥ -- or anything

example : is_scalar_tower L (middle_field L) (algebraic_closure L) :=
(middle_field L).is_scalar_tower_mid' -- works fine and this is an instance

example : is_scalar_tower L (middle_field L) (algebraic_closure L) := infer_instance -- deterministic timeout :-(

Looking at the trace with set_option trace.class_instances true it seems to me that typeclass inference actually does succeed and finds a monster term and then for some reason falls over later. Should I be worried about this? I can just add the instance manually I guess, or will this cause problems later on?

[Eric Wieser]

I think you probably are in trouble here and I'm not sure there's all that much you can do about it. Adding special cases of instances manually that already exist like you do above is a fairly typical workaround, which has the main drawback of forcing you to come up with stupid names for your instances