Zulip Chat Archive

Stream: new members

Topic: type mismatch


view this post on Zulip Kenny Lau (Feb 27 2019 at 09:03):

has type
  @is_ring_hom.{u (max v u)} R (Π (b : ι), @ideal.quotient.{u} R _inst_1 (f b)) (@comm_ring.to_ring.{u} R _inst_1)
    (@pi.ring.{v u} ι (λ (b : ι), @ideal.quotient.{u} R _inst_1 (f b))
       (λ (i : ι),
          @comm_ring.to_ring.{u} (@ideal.quotient.{u} R _inst_1 (f i)) (@ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
    (λ (x : R) (b : ι), @ideal.quotient.mk.{u} R _inst_1 (f b) x)
but is expected to have type
  @is_ring_hom.{u (max v u)} R (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i)) (@comm_ring.to_ring.{u} R _inst_1)
    (@comm_ring.to_ring.{(max v u)} (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
       (@pi.comm_ring.{v u} ι (λ (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
          (λ (i : ι), @ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
    (λ (r : R) (i : ι), @ideal.quotient.mk.{u} R _inst_1 (f i) r)

view this post on Zulip Kenny Lau (Feb 27 2019 at 09:04):

have (@pi.ring.{v u} ι (λ (b : ι), @ideal.quotient.{u} R _inst_1 (f b))
       (λ (i : ι),
          @comm_ring.to_ring.{u} (@ideal.quotient.{u} R _inst_1 (f i)) (@ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
=
(@comm_ring.to_ring.{(max v u)} (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
       (@pi.comm_ring.{v u} ι (λ (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
          (λ (i : ι), @ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
, from rfl,

but this works

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 09:04):

Is this thread supposed to be comprehensible to anyone but you?

view this post on Zulip Kenny Lau (Feb 27 2019 at 09:05):

type mismatch at application
  quotient.lift (⨅ (i : ι), f i) (λ (r : R) (i : ι), quotient.mk (f i) r)
term
  pi.is_ring_hom_pi (λ (i : ι) (r : R), quotient.mk (f i) r)
has type
  is_ring_hom (λ (x : R) (b : ι), quotient.mk (f b) x)
but is expected to have type
  is_ring_hom (λ (r : R) (i : ι), quotient.mk (f i) r)

view this post on Zulip Kenny Lau (Feb 27 2019 at 09:05):

is this more comprehensible?

view this post on Zulip Patrick Massot (Feb 27 2019 at 09:05):

Kenny should have a private stream all for himself

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 09:05):

What is your question Kenny? I don't think that other people are going to be carefully scanning your output of pp.all true.

view this post on Zulip Kenny Lau (Feb 27 2019 at 09:06):

well, my question is that, clearly they are equal!

view this post on Zulip Patrick Massot (Feb 27 2019 at 09:06):

Is that a question?

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 09:06):

Well Lean says they're not so they're not.

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 09:06):

But because we have no way of reproducing the error, how can anyone else help?

view this post on Zulip Kenny Lau (Feb 27 2019 at 09:06):

then the question is, why does Lean not know that they are equal?

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 09:06):

you're the only person who can answer that until you post a lot more context

view this post on Zulip Kenny Lau (Feb 27 2019 at 09:06):

import algebra.pi_instances ring_theory.ideal_operations

universes u v

variables {R : Type u} [comm_ring R] {ι : Type v}

open lattice

namespace ideal

def to_prod (f : ι  ideal R) : ( i, f i).quotient  Π i, (f i).quotient :=
@@quotient.lift _ _ ( i, f i) (λ r i, ideal.quotient.mk (f i) r)
  (pi.is_ring_hom_pi _ : is_ring_hom (λ (r : R) (i : ι), quotient.mk (f i) r))
  _

end ideal

view this post on Zulip Patrick Massot (Feb 27 2019 at 09:07):

We can sympathize, this is probably what we should do

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 09:07):

After his last post we can now try to help :-)

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 09:08):

So they're not the same because the implicit terms are different.

view this post on Zulip Kenny Lau (Feb 27 2019 at 09:10):

but they're defeq

view this post on Zulip Kenny Lau (Feb 27 2019 at 09:10):

as seen in my second post

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 09:12):

Indeed, you have now explained the question coherently.

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 09:13):

import algebra.pi_instances ring_theory.ideal_operations

universes u v

variables {R : Type u} [comm_ring R] {ι : Type v}

open lattice

namespace ideal

set_option pp.all true
def to_prod (f : ι  ideal R) : ( i, f i).quotient  Π i, (f i).quotient :=
begin
  have : @is_ring_hom.{u (max v u)} R (Π (b : ι), @ideal.quotient.{u} R _inst_1 (f b)) (@comm_ring.to_ring.{u} R _inst_1)
    (@pi.ring.{v u} ι (λ (b : ι), @ideal.quotient.{u} R _inst_1 (f b))
       (λ (i : ι),
          @comm_ring.to_ring.{u} (@ideal.quotient.{u} R _inst_1 (f i)) (@ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
    (λ (x : R) (b : ι), @ideal.quotient.mk.{u} R _inst_1 (f b) x)
    =
@is_ring_hom.{u (max v u)} R (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i)) (@comm_ring.to_ring.{u} R _inst_1)
    (@comm_ring.to_ring.{(max v u)} (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
       (@pi.comm_ring.{v u} ι (λ (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
          (λ (i : ι), @ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
    (λ (r : R) (i : ι), @ideal.quotient.mk.{u} R _inst_1 (f i) r) := rfl,

exact @@quotient.lift _ _ ( i, f i) (λ r i, ideal.quotient.mk (f i) r)
  (pi.is_ring_hom_pi _ : is_ring_hom (λ (r : R) (i : ι), quotient.mk (f i) r))
  _
  /-
  type mismatch at application
  @ideal.quotient.lift.{u (max v u)} R (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i)) _inst_1
    (@pi.comm_ring.{v u} ι (λ (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
       (λ (i : ι), @ideal.quotient.comm_ring.{u} R _inst_1 (f i)))
    (@lattice.infi.{u v+1} (@ideal.{u} R _inst_1) ι
       (@submodule.lattice.has_Inf.{u u} R R (@comm_ring.to_ring.{u} R _inst_1)
          (@ring.to_add_comm_group.{u} R (@comm_ring.to_ring.{u} R _inst_1))
          (@ring.to_module.{u} R (@comm_ring.to_ring.{u} R _inst_1)))
       (λ (i : ι), f i))
    (λ (r : R) (i : ι), @ideal.quotient.mk.{u} R _inst_1 (f i) r)
    (@pi.is_ring_hom_pi.{v u u} ι (λ (a : ι), @ideal.quotient.{u} R _inst_1 (f a))
       (λ (i : ι),
          @comm_ring.to_ring.{u} (@ideal.quotient.{u} R _inst_1 (f i)) (@ideal.quotient.comm_ring.{u} R _inst_1 (f i)))
       R
       (@comm_ring.to_ring.{u} R _inst_1)
       (λ (i : ι) (r : R), @ideal.quotient.mk.{u} R _inst_1 (f i) r)
       (λ (a : ι), @ideal.quotient.is_ring_hom_mk.{u} R _inst_1 (f a)))
term
  @pi.is_ring_hom_pi.{v u u} ι (λ (a : ι), @ideal.quotient.{u} R _inst_1 (f a))
    (λ (i : ι),
       @comm_ring.to_ring.{u} (@ideal.quotient.{u} R _inst_1 (f i)) (@ideal.quotient.comm_ring.{u} R _inst_1 (f i)))
    R
    (@comm_ring.to_ring.{u} R _inst_1)
    (λ (i : ι) (r : R), @ideal.quotient.mk.{u} R _inst_1 (f i) r)
    (λ (a : ι), @ideal.quotient.is_ring_hom_mk.{u} R _inst_1 (f a))
has type
  @is_ring_hom.{u (max v u)} R (Π (b : ι), @ideal.quotient.{u} R _inst_1 (f b)) (@comm_ring.to_ring.{u} R _inst_1)
    (@pi.ring.{v u} ι (λ (b : ι), @ideal.quotient.{u} R _inst_1 (f b))
       (λ (i : ι),
          @comm_ring.to_ring.{u} (@ideal.quotient.{u} R _inst_1 (f i)) (@ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
    (λ (x : R) (b : ι), @ideal.quotient.mk.{u} R _inst_1 (f b) x)
but is expected to have type
  @is_ring_hom.{u (max v u)} R (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i)) (@comm_ring.to_ring.{u} R _inst_1)
    (@comm_ring.to_ring.{(max v u)} (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
       (@pi.comm_ring.{v u} ι (λ (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
          (λ (i : ι), @ideal.quotient.comm_ring.{u} R _inst_1 (f i))))
    (λ (r : R) (i : ι), @ideal.quotient.mk.{u} R _inst_1 (f i) r)
    -/

end

end ideal

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 09:13):

I recommend you fill in the _

view this post on Zulip Kenny Lau (Feb 27 2019 at 09:14):

wat

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 09:14):

but what do I know

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 09:15):

Maybe some elaboration is taking place in the wrong order or some such nonsense

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 09:17):

Do you understand why

exact @ideal.quotient.lift.{u (max v u)} R (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i)) _inst_1
    (@pi.comm_ring.{v u} ι (λ (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
       (λ (i : ι), @ideal.quotient.comm_ring.{u} R _inst_1 (f i)))
    (@lattice.infi.{u v+1} (@ideal.{u} R _inst_1) ι
       (@submodule.lattice.has_Inf.{u u} R R (@comm_ring.to_ring.{u} R _inst_1)
          (@ring.to_add_comm_group.{u} R (@comm_ring.to_ring.{u} R _inst_1))
          (@ring.to_module.{u} R (@comm_ring.to_ring.{u} R _inst_1)))
       (λ (i : ι), f i))
    (λ (r : R) (i : ι), @ideal.quotient.mk.{u} R _inst_1 (f i) r)
    (@pi.is_ring_hom_pi.{v u u} ι (λ (a : ι), @ideal.quotient.{u} R _inst_1 (f a))
       (λ (i : ι),
          @comm_ring.to_ring.{u} (@ideal.quotient.{u} R _inst_1 (f i)) (@ideal.quotient.comm_ring.{u} R _inst_1 (f i)))
       R
       (@comm_ring.to_ring.{u} R _inst_1)
       (λ (i : ι) (r : R), @ideal.quotient.mk.{u} R _inst_1 (f i) r)
       (λ (a : ι), @ideal.quotient.is_ring_hom_mk.{u} R _inst_1 (f a)))

doesn't work? I have to go and give a lecture on p-adic geometry so I can't think about this any more but this would be one way of trying to fill in the _s to see if that's the issue.

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 09:17):

i.e. look at what the term fully elaborates to and try that instead. I just must have failed somehow.

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 09:17):

[my error was "you got it wrong" not "these are not defeq"]

view this post on Zulip Kenny Lau (Feb 27 2019 at 09:24):

finally this "worked":

import algebra.pi_instances ring_theory.ideal_operations

universes u v

variables {R : Type u} [comm_ring R] {ι : Type v}

open lattice

namespace ideal

def to_pi (f : ι  ideal R) (r : R) : Π i, (f i).quotient :=
λ i, ideal.quotient.mk (f i) r

instance (f : ι  ideal R) : is_ring_hom (to_pi f) :=
pi.is_ring_hom_pi _

def to_prod (f : ι  ideal R) : ( i, f i).quotient  Π i, (f i).quotient :=
@ideal.quotient.lift.{u (max v u)} R (Π (i : ι), @ideal.quotient.{u} R _inst_1 (f i)) _inst_1
    (@pi.comm_ring.{v u} ι (λ (i : ι), @ideal.quotient.{u} R _inst_1 (f i))
       (λ (i : ι), @ideal.quotient.comm_ring.{u} R _inst_1 (f i)))
    (@lattice.infi.{u v+1} (@ideal.{u} R _inst_1) ι
       (@submodule.lattice.has_Inf.{u u} R R (@comm_ring.to_ring.{u} R _inst_1)
          (@ring.to_add_comm_group.{u} R (@comm_ring.to_ring.{u} R _inst_1))
          (@ring.to_module.{u} R (@comm_ring.to_ring.{u} R _inst_1)))
       (λ (i : ι), f i))
    (@ideal.to_pi.{u v} R _inst_1 ι f)
    (@ideal.is_ring_hom.{u v} R _inst_1 ι f)
  (λ r hr, funext $ λ i, quotient.eq_zero_iff_mem.2 $ mem_Inf.1 hr i, rfl)

end ideal

view this post on Zulip Kenny Lau (Feb 27 2019 at 09:26):

minimzed to:

def to_prod (f : ι  ideal R) : ( i, f i).quotient  Π i, (f i).quotient :=
@@ideal.quotient.lift _ _ ( i, f i) (ideal.to_pi f)
    (@ideal.is_ring_hom.{u v} R _ ι f)
  (λ r hr, funext $ λ i, quotient.eq_zero_iff_mem.2 $ mem_Inf.1 hr i, rfl)

view this post on Zulip Kenny Lau (Feb 27 2019 at 09:26):

in (@ideal.is_ring_hom.{u v} R _ ι f), turning ι into underscore creates the error

view this post on Zulip Kenny Lau (Feb 27 2019 at 09:27):

the R is also essential

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 14:04):

So it's some elaborator nonsense, or do you think it's a bug?

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 14:04):

Let's try to debug it!

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 14:05):

Sebastian once told us some set_option to see the rfl machine trying to prove rfl

view this post on Zulip Kevin Buzzard (Feb 27 2019 at 14:05):

I think it was in the thread where he wrote "got into office" "checks Zulip" "leaves office again"

view this post on Zulip Ashvni Narayanan (Sep 01 2020 at 13:44):

I am trying to show that the principal fractional ideals form a subgroup of the group of fractional ideals.

import linear_algebra.finite_dimensional
import ring_theory.ideal.basic
import algebra.field
import ring_theory.subring
import ring_theory.integral_closure
import ring_theory.fractional_ideal
import data.rat.basic
import ring_theory.algebra
import ring_theory.algebraic

open function
open_locale classical big_operators

class number_field (K : Type*) :=
   (fld : field K)
   (alg : algebra  K)
   (fd : finite_dimensional  K)

def number_ring (K : Type*) [number_field K] := @integral_closure  K _ (@field.to_comm_ring K _inst_1.fld) _

noncomputable theory
open_locale classical

open finite_dimensional
namespace number_field
variables (K : Type*) [number_field K]
variables [g : fraction_map (number_ring K) K ]

def principal_fractional_ideal := { P : ring.fractional_ideal g //  a : (number_ring K), submodule.is_principal P.1 }

instance is_group : group (ring.fractional_ideal g) := sorry,

instance is_subgroup : subgroup (ring.fractional_ideal g) :=
begin
  use (principal_fractional_ideal g),
end

The last proof gives me the error

type mismatch at application
  principal_fractional_ideal g
term
  g
has type
  fraction_map (number_ring K) K : Type u_1
but is expected to have type
  Type ? : Type (?+1)
state:
K : Type u_1,
_inst_1 : number_field K,
g : fraction_map (number_ring K) K
 subgroup (ring.fractional_ideal g)

Any help is appreciated, thank you!

view this post on Zulip Adam Topaz (Sep 01 2020 at 13:50):

Sounds like you're missing an underscore before the g.

view this post on Zulip Adam Topaz (Sep 01 2020 at 13:57):

Your code is not compiling for me :-/

view this post on Zulip Adam Topaz (Sep 01 2020 at 14:06):

Okay, looks like there were a bunch of issues.
Here's a hacked together fix.

import linear_algebra.finite_dimensional
import ring_theory.ideal.basic
import algebra.field
import ring_theory.subring
import ring_theory.integral_closure
import ring_theory.fractional_ideal
import data.rat.basic
import ring_theory.algebra
import ring_theory.algebraic

open function
open_locale classical big_operators

class number_field (K : Type*) :=
   (fld : field K)
   (alg : algebra  K)
   (fd : finite_dimensional  K)

namespace number_field
variables (K : Type*) [number_field K]
instance : field K := number_field.fld
instance : algebra  K := number_field.alg
instance : finite_dimensional  K := number_field.fd
end number_field

def number_ring (K : Type*) [number_field K] := @integral_closure  K _ (@field.to_comm_ring K _inst_1.fld) _

noncomputable theory
open_locale classical

open finite_dimensional
namespace number_field
variables (K : Type*) [number_field K]
variables (g : fraction_map (number_ring K) K)

def principal_fractional_ideal := { P : ring.fractional_ideal g |  a : (number_ring K), submodule.is_principal P.1 }

instance is_group : group (ring.fractional_ideal g) := sorry,

#check principal_fractional_ideal

instance is_subgroup : subgroup (ring.fractional_ideal g) :=
{ carrier := principal_fractional_ideal _ g,
  one_mem' := _,
  mul_mem' := _,
  inv_mem' := _ }

view this post on Zulip Adam Topaz (Sep 01 2020 at 14:07):

Note that subgroup takes a set as its carrier, whereas you defined a principal_fractional_ideal as a subtype.
Also, the field, algebra, etc. instances were not recognized since you didn't extend these classes in your definition of number field.

view this post on Zulip Ashvni Narayanan (Sep 01 2020 at 15:51):

Ah, I see. It seems like the _ is K. So essentially I needed g to be explicit. Thank you!

view this post on Zulip Adam Topaz (Sep 01 2020 at 15:53):

You need to make KK implicit :) (lean will figure out KK from gg)

view this post on Zulip Ashvni Narayanan (Sep 01 2020 at 16:05):

Adam Topaz said:

You need to make KK implicit :) (lean will figure out KK from gg)

Ah alright, thank you!


Last updated: May 06 2021 at 21:09 UTC