Zulip Chat Archive

Stream: maths

Topic: lift from subring to field


view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 02:12):

K: Type u_1
_inst_4: field K
_inst_5: discrete_valuation_field K
S: ideal (val_ring K)
h: ¬S = 
x: (val_ring K)
a: x  S
h: ¬x = 0
h_1: x = 0
 x = 0

val_ring K is a subring of K. As far as I understand, I am given that the lift of x to K is 0, and need to prove that x = 0. I don't know how to proceed.
Any help is appreciated, thank you!

view this post on Zulip Mario Carneiro (Jul 09 2020 at 02:14):

Does exact subtype.eq h_1 work?

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 02:15):

Yes, that works!

view this post on Zulip Jalex Stark (Jul 09 2020 at 02:21):

does assumption_mod_cast work?

view this post on Zulip Mario Carneiro (Jul 09 2020 at 02:23):

I don't think norm_cast knows about subtype casts

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 02:27):

Jalex Stark said:

does assumption_mod_cast work?

No, it gives the error

assumption_mod_cast failed:
exact tactic failed, type mismatch, given expression has type
  Type u_1
but is expected to have type
  x = 0

view this post on Zulip Adam Topaz (Jul 09 2020 at 02:28):

Alternatively, you can rewrite using h_1 (probably after doing a case split on x)

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 02:39):

I am now having the same problem, with \le :

K: Type u_1
_inst_4: field K
_inst_5: discrete_valuation_field K
x: (val_ring K)
 0  v x

The definition of val_ring K is:

def val_ring (K : Type*) [field K] [discrete_valuation_field K] := { x : K | 0  v x }

Any help is appreciated, thank you!

view this post on Zulip Adam Topaz (Jul 09 2020 at 02:40):

Try the same thing -- split x, and see what you get.

view this post on Zulip Adam Topaz (Jul 09 2020 at 02:41):

(I think exact x.2 should take care of this in one line.)

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 02:47):

Ah ok, cases x does it, as does exact x.2 . Thank you!

view this post on Zulip Johan Commelin (Jul 09 2020 at 04:19):

Adam Topaz said:

(I think exact x.2 should take care of this in one line.)

@Ashvni Narayanan This is (strictly speaking) leaking an implementation detail. Hence it is encouraged to prove a lemma val_ring.zero_le as one of the first things after you define val_ring. It is part of the basic API.

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 14:12):

Ok sure. Thank you!


Last updated: May 06 2021 at 19:30 UTC