Zulip Chat Archive

Stream: maths

Topic: use?


Ashvni Narayanan (Oct 27 2020 at 09:18):

I am trying to prove

?m_1  submodule.comap (localization_map.lin_coe (fraction_ring.of A)) I.val

and I have

g': y  submodule.comap (localization_map.lin_coe (fraction_ring.of A)) I.val

where ?m_1 must be of type A, and y is of type A. However, none of exact, refine, assumption or use work.

Any help is appreciated. Thank you!

Anne Baanen (Oct 27 2020 at 09:19):

Try convert g'

Ashvni Narayanan (Oct 27 2020 at 09:20):

Doesn't work :(

Anne Baanen (Oct 27 2020 at 09:20):

Does it fail or result in new goals?

Ashvni Narayanan (Oct 27 2020 at 09:20):

invalid type ascription, term has type
  ?m_1
but is expected to have type
  ?m_1  submodule.comap (localization_map.lin_coe (fraction_ring.of A)) I.val

Ashvni Narayanan (Oct 27 2020 at 09:21):

Well the next goal is to prove that ?m_1 : A.

Anne Baanen (Oct 27 2020 at 09:21):

Hmm, could you post a #mwe? It looks like Lean is getting confused earlier on.

Ashvni Narayanan (Oct 27 2020 at 09:24):

https://github.com/leanprover-community/mathlib/blob/d008b1c22ad3f20f61915a66f95a64615709d07f/src/ring_theory/dedekind_domain.lean#L286

Ashvni Narayanan (Oct 27 2020 at 09:24):

Ashvni Narayanan said:

https://github.com/leanprover-community/mathlib/blob/d008b1c22ad3f20f61915a66f95a64615709d07f/src/ring_theory/dedekind_domain.lean#L286

Does this help? If not, I'll make an mwe.

Anne Baanen (Oct 27 2020 at 09:26):

That should be enough, thanks! One moment please...

Anne Baanen (Oct 27 2020 at 09:30):

Aha, the problem seems to be this: you define y in one subgoal, but it should be used in another subgoal.

Anne Baanen (Oct 27 2020 at 09:32):

(I'm guessing you did this because you got errors when writing cases (g : ∃ (x : localization (non_zero_divisors A)), x ∈ I)?

Ashvni Narayanan (Oct 27 2020 at 09:32):

I did try rotate, but that ended up giving me other issues with using cases, hence I did not proceed..

Ashvni Narayanan (Oct 27 2020 at 09:32):

Anne Baanen said:

(I'm guessing you did this because you got errors when writing cases (g : ∃ (x : localization (non_zero_divisors A)), x ∈ I)?

Haha yes exactly

Anne Baanen (Oct 27 2020 at 09:36):

Hmm, I don't know to fix the proof because I'm not quite sure what you're trying to prove here actually. Your goal ↥(submodule.comap (localization_map.lin_coe (fraction_ring.of A)) I.val) means "we can compute an element of the ideal" (let's just call it J), but surely we have 0 \in J?

Ashvni Narayanan (Oct 27 2020 at 09:39):

What I actually want to prove is that if we have a fractional ideal I, and I \leq 1, then (the preimage of) I must be an ideal of A.

Anne Baanen (Oct 27 2020 at 09:40):

Ah, this turns out to be called submodule.comap, as in the function you used to construct your goal :)

Anne Baanen (Oct 27 2020 at 09:42):

(In fact, this holds for all fractional ideals: everything outside of A is just discarded by comap.)

Ashvni Narayanan (Oct 27 2020 at 09:46):

Ah I see, hence the I \le 1 is not needed!

Ashvni Narayanan (Oct 27 2020 at 09:46):

Apologies for this, and thank you for your help! :)

Anne Baanen (Oct 27 2020 at 09:47):

You're welcome!


Last updated: Dec 20 2023 at 11:08 UTC