## Stream: new members

### Topic: Constructing chain using DC

#### Kenji Nakagawa (Aug 15 2020 at 19:24):

Hi, I'm relatively new to Lean and am currently trying to prove stuff about Noetherian rings and got stuck here:

import ring_theory.fractional_ideal
universe u
example (R' : Type u) {X : Type u}
[integral_domain R']
[ring R']
[module R' X]
(wf : well_founded (gt : submodule R' X → submodule R' X → Prop))
(A : set (submodule R' X))
(hA : inhabited ↥A)
(a : submodule R' X)
(akey : a ∈ A)
(h' : ∀ (M : submodule R' X),
M ∈ A → (∃ (I : submodule R' X), I ∈ A ∧ M < I)) :
false :=
begin
rw order_embedding.well_founded_iff_no_descending_seq at wf,
apply wf,
refine nonempty.intro _,
--point of h1 is to have a stronger hypothesis by requiring all terms be elements of A
have h1 : ∃(f : ℕ → submodule R' X), ∀ (n : ℕ), f n ∈ A ∧ f (n + 1) > f (n),
{
fconstructor,
--here the fact that f(n) ∈ A needs to be used to construct f(n+1)
intro n,
induction n with n Mn, --another inductive hypothesis MninA (Mn ∈ A)
{--base case
use a, --exact akey
},
{--nat.succ case
--rcases h' Mn MninA with ⟨I, IinA, MltI⟩,
--use I, exact IinA
sorry,
},
--I have no idea what all these nat.rec's are
--exact MltI, (by construction)
repeat {sorry},
},
refine order_embedding.nat_gt _ _,
--rcases h1 with ⟨f, fina, fkey⟩, --induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into  Prop
--exact f, exact fkey
repeat{sorry},
end


Essentially the math proof is that we can start off with a, and using h', construct a strictly larger element of A ad infinitum (we also invoke axiom of dependent choice here, as our next larger elements depends on our previous).
However, the main roadblock is that as is, it's not possible to use h', as the inductive hypothesis doesn't say anything about being members of A. Additionally, rcases h1 doesn't work because it can only reduce into Prop. Any help is appreciated!

#### Kevin Buzzard (Aug 15 2020 at 19:33):

I'm not at lean right now but you should delete ring R' because I'm pretty sure it's implied by integral domain R' and what you have will give R' two independent ring structures

#### Patrick Massot (Aug 15 2020 at 19:37):

You can get f using choose f hf using h1.

#### Patrick Massot (Aug 15 2020 at 19:41):

More specifically, everything after the have block can be replaced by

  choose f hf using h1,
exact order_embedding.nat_gt f (forall_and_distrib.1 hf).2,


#### Patrick Massot (Aug 15 2020 at 19:45):

This is answering your specific question about the end, but clearly something with this proof is not quite right.

#### Kenji Nakagawa (Aug 15 2020 at 19:49):

for some more context, this is more specifically about proving equivalence between some Neotherian module definitions (also, in a previous attempt, I tried to use zorn.zorn_partial_order₀, but to use it, it boiled down to proving this, and the other order.zorn lemmas seemed to not match well)

#### Patrick Massot (Aug 15 2020 at 20:03):

begin
rw order_embedding.well_founded_iff_no_descending_seq at wf,
apply wf,
constructor,
have h'' : ∀ M : A, ∃ I : A, (M : submodule R' X) < I,
{ rintros ⟨M, M_in⟩,
rcases h' M M_in with ⟨I, I_in, hMI⟩,
exact ⟨⟨I, I_in⟩, hMI⟩ },
let f : ℕ → A := λ n, nat.rec_on n ⟨a, akey⟩ (λ n M, classical.some (h'' M)),
exact order_embedding.nat_gt (coe ∘ f) (λ n, classical.some_spec (h'' \$ f n))
end


@Kenji Nakagawa the have h'' in the middle is extremely irritating, but that's the current reality, we spend a lot of time unpacking and repacking the same stuff.

#### Kenji Nakagawa (Aug 15 2020 at 20:12):

Thanks a lot! Yeah, I've noticed that quite a bit of work is usually just reframing it into the right way. Hopefully relatively soon we'll have some lemmas about dedekind domains (although equivalence between definitions might take awhile yet)!

#### Kevin Buzzard (Aug 15 2020 at 20:42):

I think several people are independently thinking any t Dedekind domains, i should chase up what my students are doing

Last updated: May 18 2021 at 16:25 UTC