Timeout using particular ring hom in general universe

Stream: maths

[Amelia Livingston]

Hi - could someone help me understand why this times out when the universe is general u? I also get an excessive memory consumption error if I replace Scheme.Spec_map with quiver.hom.op. Feel free to move this to new members if the answer is easy, wasn't sure where to put it.

import algebraic_geometry.Scheme
import ring_theory.tensor_product
import data.polynomial.laurent

noncomputable theory
universes u
open algebraic_geometry
open_locale tensor_product

local notation R`[T;T⁻¹]`:9000 := laurent_polynomial R
variables (R : Type u) [comm_ring R] (f : polynomial R →+* R[T;T⁻¹] ⊗[R] R[T;T⁻¹])

def comultiplication : R[T;T⁻¹] →+* R[T;T⁻¹] ⊗[R] R[T;T⁻¹] :=
@is_localization.lift (polynomial R) _ _ _ _ _ _ _ laurent_polynomial.is_localization f sorry

#check Scheme.Spec_map (CommRing.of_hom $ comultiplication R f)

[Junyan Xu]

Again, here #check Scheme.Spec_map (CommRing.of_hom $ by apply comultiplication R f) works in an instant.