# Zulip Chat Archive

## Stream: new members

### Topic: type mismatch

#### 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)

#### 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

#### Kevin Buzzard (Feb 27 2019 at 09:04):

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

#### 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)

#### Kenny Lau (Feb 27 2019 at 09:05):

is this more comprehensible?

#### Patrick Massot (Feb 27 2019 at 09:05):

Kenny should have a private stream all for himself

#### 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`

.

#### Kenny Lau (Feb 27 2019 at 09:06):

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

#### Patrick Massot (Feb 27 2019 at 09:06):

Is that a question?

#### Kevin Buzzard (Feb 27 2019 at 09:06):

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

#### Kevin Buzzard (Feb 27 2019 at 09:06):

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

#### Kenny Lau (Feb 27 2019 at 09:06):

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

#### Kevin Buzzard (Feb 27 2019 at 09:06):

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

#### 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

#### Patrick Massot (Feb 27 2019 at 09:07):

We can sympathize, this is probably what we should do

#### Kevin Buzzard (Feb 27 2019 at 09:07):

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

#### Kevin Buzzard (Feb 27 2019 at 09:08):

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

#### Kenny Lau (Feb 27 2019 at 09:10):

but they're defeq

#### Kenny Lau (Feb 27 2019 at 09:10):

as seen in my second post

#### Kevin Buzzard (Feb 27 2019 at 09:12):

Indeed, you have now explained the question coherently.

#### 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

#### Kevin Buzzard (Feb 27 2019 at 09:13):

I recommend you fill in the `_`

#### Kenny Lau (Feb 27 2019 at 09:14):

wat

#### Kevin Buzzard (Feb 27 2019 at 09:14):

but what do I know

#### Kevin Buzzard (Feb 27 2019 at 09:15):

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

#### 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.

#### 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.

#### Kevin Buzzard (Feb 27 2019 at 09:17):

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

#### 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

#### 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⟩)

#### Kenny Lau (Feb 27 2019 at 09:26):

in `(@ideal.is_ring_hom.{u v} R _ ι f)`

, turning `ι`

into underscore creates the error

#### Kenny Lau (Feb 27 2019 at 09:27):

the `R`

is also essential

#### Kevin Buzzard (Feb 27 2019 at 14:04):

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

#### Kevin Buzzard (Feb 27 2019 at 14:04):

Let's try to debug it!

#### Kevin Buzzard (Feb 27 2019 at 14:05):

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

#### 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"

#### 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!

#### Adam Topaz (Sep 01 2020 at 13:50):

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

#### Adam Topaz (Sep 01 2020 at 13:57):

Your code is not compiling for me :-/

#### 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' := _ }
```

#### 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.

#### 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!

#### Adam Topaz (Sep 01 2020 at 15:53):

You need to make $K$ implicit :) (lean will figure out $K$ from $g$)

#### Ashvni Narayanan (Sep 01 2020 at 16:05):

Adam Topaz said:

You need to make $K$ implicit :) (lean will figure out $K$ from $g$)

Ah alright, thank you!

Last updated: May 06 2021 at 21:09 UTC