ideal.quotient

Stream: maths

[Kevin Buzzard]

@Anne Baanen or someone else who's paying attention, is ideal.quotient supposed to be not there any more in master? I have some ring which has an extremely long name, and I have Q := (ideal.span {a | ∃ b, a = f b}).quotient and this doesn't work any more. Do I now have to write down the full name of the ring?

[Adam Topaz]

Does _ / (ideal.span ...) work?

[Kevin Buzzard]

Yes! :D I just had that idea as you posted

[Johan Commelin]

It's now an instance ideal.has_quotient of has_quotient.

[Johan Commelin]

Type \bigsolidus or \quot or \/ to type that / (and make sure you have an up-to-date VScode extension)

[Kevin Buzzard]

Right, but do you think I.quotient is better than _ / I? Anyway. Oh, I used \quot for the quotient symbol ;-)

[Johan Commelin]

I,quotient??

[Kevin Buzzard]

Sorry, mistyped. I.quotient.

[Johan Commelin]

R / I looks way better to me

[Kevin Buzzard]

But in this situation I'm in (trying to debug this blasted timeout which the Imperial algebraic number theorists are running into) I am never ever going to be mentioning any of the explicit R's showing up ;-)

[Adam Topaz]

Kevin have you tried the following approach?

import field_theory.is_alg_closed.algebraic_closure

universe u
theorem exists_algebraic_closure (K : Type u) [field K] :
  ∃ (L : Type u) [field L], by resetI; exact ∃ [algebra K L], by resetI; exact is_alg_closure K L  :=
begin
  use [algebraic_closure K, infer_instance, infer_instance],
  exact algebraic_closure.is_alg_closure K,
end

def algebraic_closure' (K : Type u) [field K] : Type u :=
(exists_algebraic_closure K).some

noncomputable instance {K : Type u} [field K] : field (algebraic_closure' K) :=
(exists_algebraic_closure K).some_spec.some

noncomputable instance {K : Type u} [field K] : algebra K (algebraic_closure' K) :=
(exists_algebraic_closure K).some_spec.some_spec.some

instance {K : Type u} [field K] : is_alg_closure K (algebraic_closure' K) :=
(exists_algebraic_closure K).some_spec.some_spec.some_spec

[Adam Topaz]

I assume your timeouts are with algebraic closures again?

[Kevin Buzzard]

The issue isn't finding the workarounds, it's finding the underlying problem.

[Adam Topaz]

Oh, I thought that we realized the issue is that lean thinks something is computable when it's not....

[Kevin Buzzard]

Right, but if I want to get Gabriel to fix it then I need to get an example which doesn't depend on mathlib.

[Adam Topaz]

fair point

[Kevin Buzzard]

But I've passed the trick onto Amelia anyway :-) I guess what I am slightly worried about is that these workarounds are just kicking the problem down the road and it'll be back to bite us later.

[Adam Topaz]

I think the above is how algebraic_closure should be defined anyway.

[Adam Topaz]

I was hoping

noncomputable instance nonempty.has_zero {α} [nonempty α] : has_zero α :=
has_zero.mk $ classical.choice ‹_›

noncomputable instance nonempty.has_one {α} [nonempty α] : has_one α :=
has_one.mk $ classical.choice ‹_›

noncomputable instance nonempty.has_add {α} [nonempty (α → α → α)] : has_add α :=
has_add.mk $ classical.choice $ infer_instance

def bar (α : Type*) [nonempty α] [nonempty (α → α → α)] := { t : α // ∃ u : α, u = 10 }

def baz (α : Type*) [nonempty α] [nonempty (α → α → α)] : bar α → α := λ t, t.1

would reproduce the timeout, but, alas, this just works.

[Yakov Pechersky]

The noncomputable issue that I remember is when an equation compiler has two match statements, and only the latter one of them is noncomputable. The compiler doesn't know that it itself is noncomputable until the whole term is compiled, and checking whether any of the terms it uses are noncomputable might lead to a deep check that times out. I might remember wrong.