Constructing chain using DC

Stream: new members

[Kenji Nakagawa]

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']
  [add_comm_group X]
  [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]

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]

You can get f using choose f hf using h1.

[Patrick Massot]

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]

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

[Kenji Nakagawa]

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]

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]

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]

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