Chains to LTSeries

Stream: mathlib4

[Quinn La Fond]

I am at the tail end of finishing my formalization of the statement: "integral extensions preserve Krull dimension". Unfortunately, , since I was bad at parsing the mathlib4 library when I started this mini project, I formalized all of my "helper" lemmas in terms of finite subsets of PrimeSpectrum A which were totally ordered. In other words, the objects I was dealing with, and inductively applying Going Up to were things like S : Set (PrimeSpectrum A) with attributes S.Finite and IsChain ( . < . ) S.

In hindsight, this was probably not the best way to write everything as Krull DImension is defined using LTSeries which seem to me to be injective functions from Fin(n) to Set(PrimeSpectrum A) preserving the order on Fin(n). Rather than rewrite all of my Lemma's I thought I could prove the following:

lemma krullDim_chain_leq
    {α β : Type*} [PartialOrder α] [PartialOrder β]
    (H : ∀ {S : Set α},
    IsChain (· < ·) S → S.Finite → ∃ T : Set β,
    IsChain (· < ·) T ∧ T.Finite ∧ (Nat.card S = Nat.card T)) :
    krullDim α ≤ krullDim β

The strategy of the proof is as follows:
1) Start with an LTSeries in alpha
2) Turn the LTSeries into a set
3) Show this set is finite and is a chain
4) Use the hypothesis H to get a finite chain T of the same cardinality in beta
5) Turn T back into an LTSeries

I am stuck on step 5, i.e. I have a finite chain T of the same cardinality of the set in alpha, but I cannot seem figure out how to get it to be an LTSeries. Does anyone have any advice on how one could approach this?

[Aaron Liu]

repeatedly extract the minimum

[Quinn La Fond]

@Aaron Liu I agree that that makes sense from a mathematical pov, but I am unsure of how to implement in this procedure in lean.

[Aaron Liu]

There should be a theorem that says a finite chain has a minimum element

[Aaron Liu]

you can recursively define the nth element from the bottom as the minimum element of the chain minus all the ith elements for which i < n

[Quinn La Fond]

Yes I have the minimum element, I meant how do I recursively define an LTSeries? It is a function from Fin(n) for some n to a partially ordered set. I don't know how to actually construct such a function.

[Aaron Liu]

Same as you do normally (or have you never done so before?)

[Aaron Liu]

Call the function from inside itself

[Aaron Liu]

If you can trouble come back with an error message and we can help you fix it

[Quinn La Fond]

I have never done so before lol I am very much learning by doing atm

[Quinn La Fond]

(I also emberrasingly do not know what it means to call the function from inside itself)

[Aaron Liu]

Have you done recursive functions in other programming languages before?

[Aaron Liu]

Do you know what it means to call a function?

[Quinn La Fond]

I vaguely recall doing this in C like 4 years ago for a computational physics course but that was my only prior exposure to programming languages before this

[Quinn La Fond]

Aaron Liu said:

Do you know what it means to call a function?

This is like asking the computer to invoke something you've already defined right?

[Kevin Buzzard]

Quinn La Fond said:

I am stuck on step 5, i.e. I have a finite chain T of the same cardinality of the set in alpha, but I cannot seem figure out how to get it to be an LTSeries. Does anyone have any advice on how one could approach this?

My advice is: post a #mwe

[Quinn La Fond]

@Kevin Buzzard I read the mean working example page, but I am not totally sure how to provide such an example. I would say that I am essentially trying to prove the following lemma:

import Mathlib
open Order

lemma chain_to_LTseries  {β : Type* } [PartialOrder β]
  (T : Set β)  (T_chain : IsChain (· < · ) T) (T_finite : T.Finite) (T_nonempty : T.Nonempty) :
  ∃ T_series : LTSeries β , T_series.length  = Nat.card T -1 := by

  sorry

I think my main problem is that I don't really know how to recursively define a function...

[Quinn La Fond]

@Aaron Liu Do you have any further insight on this?

[Aaron Liu]

Maybe try something simpler first

[Quinn La Fond]

Such as?

[Aaron Liu]

define a function recursively

[Aaron Liu]

try the fibonacci sequence

[Quinn La Fond]

I understand conceptually how recursion is supposed to work, I just don't fully understand how it is supposed to work in Lean from a syntax pov.

[Kenny Lau]

I think that's why he suggested fibonacci

[Kenny Lau]

More specifically, in the NNG you have only been exposed to proving theorems (and in Lean, theorems have no data), so now you're stepping onto a new zone

[Kenny Lau]

it's a non-trivial step to go from proving theorems to constructing "data"

[Quinn La Fond]

I see, I will search for some way of doing this then.

[Quinn La Fond]

thank you

[Kenny Lau]

you can look into the library and see how various functions are defined

[Kenny Lau]

which would naturally include the Fibonacci

[Aaron Liu]

docs#Nat.fib is defined with some stream iterator to make it more efficient

[Aaron Liu]

don't know why they couldn't have just used a @[csimp] lemma

[Quinn La Fond]

what doe this mean

[Aaron Liu]

you'll have to be a bit more specific

[Aaron Liu]

wow I checked to source and it's not even a stream iterator

[Aaron Liu]

the docstring is outdated

[Quinn La Fond]

Kenny stated I should look at how the Fibonacci sequence is defined in library, you then remarked that Nat.fib is defined with some stream iterator; why the remark?

[Aaron Liu]

it's not the most obvious choice

[Kenny Lau]

@Quinn La Fond look at Nat.add then

[Kenny Lau]

(and try to ignore the @&)

[Quinn La Fond]

Hmm, so should I be defining my LTSeries as function outside of the lemma I am trying to prove?

[Aaron Liu]

yes definitely

[Quinn La Fond]

Ok and so the naive idea is something like:

def f : Fin( Nat.card T) \rightarrow \beta
|zero => minimal element of T
|succ b => minimal elment of T\ {f(b),\dots, f(0)}

I need to specify that \beta is partially ordered, and that T is a finite nonempty chain, and it looks like I can declare these things before the colon as I would with a lemma. Am I allowed to prove things inside this def though? I tried using an rcases tactic to get a minimal element of T but lean yelled at me...

[Aaron Liu]

you can't use rcases here since you're creating data

[Aaron Liu]

try docs#Exists.choose instead

[Quinn La Fond]

Should I not be using an := by after the def f : Fin (Nat.card T) \rightarrow \beta?

[Kenny Lau]

you generally shouldn't use tactics in defs

[Aaron Liu]

the reason is because since you are making data you care about which data you end up making, and when using tactics you don't get to control what they output

[Quinn La Fond]

I see. How do I get the minimum the set T inductively then? Do I specify such a hypothesis?

[Aaron Liu]

you should prove a theorem saying that there exists a minimum and then choose one out noncomputably

[Aaron Liu]

in order to get it computably you will need a few more assumptions

[Quinn La Fond]

I mean there is a theorem already written because T is a chain. T_finite.exists_minmal T_Nonempty gives the the hypothesis exists minimal element of T.

[Aaron Liu]

great

[Aaron Liu]

now use docs#Exists.choose to choose one out

[Quinn La Fond]

How does that syntax work without tactics? like naively I want to do H :=T_finite.exists_minmal T_Nonempty and then apply Exists.choose at H.

[Aaron Liu]

how about let H := (T_finite.exists_minimal T_Nonempty).choose

[Aaron Liu]

does that work for you

[Quinn La Fond]

This worked:

def order_chain {β : Type*} [PartialOrder β]
  (T : Set β) (T_chain : IsChain (· < ·) T)
  (T_finite : T.Finite) (T_nonempty : T.Nonempty) :
  Fin (Nat.card T) → β
  | zero =>  (T_finite.exists_minimal T_nonempty).choose

I am not sure if this the best way forward though...

[Quinn La Fond]

I have to run, but I will be back in an hour or two. Thank you for all the help.

[Quinn La Fond]

What do you think of the zero case?

[Aaron Liu]

I would need a #mwe

[Quinn La Fond]

Hmm, what would that look like in this case?

[Quinn La Fond]

Like in particular, if I do not know how to finish the rest of the construction yet, what is a minimum working example?

[Aaron Liu]

just sorry out the rest

[Quinn La Fond]

def order_chain {β : Type*} [PartialOrder β]
  (T : Set β) (T_chain : IsChain (· < ·) T)
  (T_finite : T.Finite) (T_nonempty : T.Nonempty) :
  Fin (1) → β
  | 0 =>  (T_finite.exists_minimal T_nonempty).choose

For some reason sorry doesn't help but if I just look at Fin(1) instead this works I think

[Aaron Liu]

you're missing imports

[Quinn La Fond]

oh right:

import Mathlib

open PrimeSpectrum
open Order
noncomputable
def order_chain {β : Type*} [PartialOrder β]
  (T : Set β) (T_chain : IsChain (· < ·) T)
  (T_finite : T.Finite) (T_nonempty : T.Nonempty) :
  Fin (1) → β
  | 0 =>  (T_finite.exists_minimal T_nonempty).choose

[Quinn La Fond]

Oh I think this how I should sorry out the rest:

import Mathlib

open PrimeSpectrum
open Order
noncomputable
def order_chain {β : Type*} [PartialOrder β]
  (T : Set β) (T_chain : IsChain (· < ·) T)
  (T_finite : T.Finite) (card_T : Nat.card T > 0 ) (T_nonempty : T.Nonempty) :
  Fin (Nat.card T) → β
  | ⟨0, _⟩ =>  (T_finite.exists_minimal T_nonempty).choose
  | ⟨Nat.succ a, _⟩ => sorry

[Aaron Liu]

oh yeah so far it's good

[Aaron Liu]

but matching on Fin like that is not something I would recommend if you're going to make it recursive

[Quinn La Fond]

Why not/what do you mean

[Aaron Liu]

since it will force you to do well-founded recursion

[Quinn La Fond]

what does that mean

[Quinn La Fond]

I don't really have another option an LTSeries S is a function from Fin(length)\rightarrow to Beta

[Aaron Liu]

I would suggest you use docs#Fin.induction instead

[Quinn La Fond]

OK, how do I change my zero case to use Fin.induction?

[Aaron Liu]

unfortunately I don't think it will work in this case

[Aaron Liu]

how about currying it and doing (n : Nat) → n < Nat.card T → β instead?

[Quinn La Fond]

I still don't understand what is wrong. If I can prove some generalization of exists_minimal for T\{b_0,\dots, b_i} for all i < n, and any b_i it should be fine right?

[Aaron Liu]

the problem is it won't reduce definitionally

[Aaron Liu]

this causes trouble sometimes so I try to avoid it if possible

[Quinn La Fond]

What do you mean currying it? And what do you mean it won't reduce definitionally?

[Quinn La Fond]

import Mathlib

open PrimeSpectrum
open Order

lemma set_diff_finite {β : Type*} [PartialOrder β] (T : Set β) (T_finite : T.Finite)
(S : Set β) :
(T \ S).Finite := by
exact T_finite.subset (by
  intro x hx
  exact hx.1)



lemma strict_set_diff_nonempty {β : Type*} [PartialOrder β] (T : Set β) (T_finite : T.Finite)
(S : Set β) (S_subset_T : S ≤ T)
(S_strict : Nat.card S < Nat.card T) :  (T \ S).Nonempty := by
have h := set_diff_finite T T_finite S
have S_finite := T_finite.subset S_subset_T
have h1 := Set.ncard_diff S_subset_T S_finite
simp at S_strict
have h2 := Nat.sub_pos_of_lt S_strict
rw [← h1] at h2
rw [(T\S).ncard_pos h] at h2

exact h2

noncomputable
def order_set {β : Type*} [PartialOrder β]
  (T : Set β) --(T_chain : IsChain (· < ·) T)
  (T_finite : T.Finite) (card_T : Nat.card T > 0) (T_nonempty : T.Nonempty) :
  Fin (Nat.card T) → T
  | ⟨0, _⟩ => by
    let m := (T_finite.exists_minimal T_nonempty).choose
    have hm : m ∈ T := (T_finite.exists_minimal T_nonempty).choose_spec.1
    exact ⟨ m , hm⟩

  | ⟨Nat.succ a, ha⟩ => by
    let S : Set β := {b | ∃ i : Fin (Nat.succ a ),  (order_set T T_finite card_T T_nonempty
    ⟨i ,  lt_trans i.is_lt ha ⟩ )=b}
    have S_eq : S= ({b | ∃ i : Fin (Nat.succ a ),  (order_set T T_finite card_T T_nonempty
    ⟨i ,  lt_trans i.is_lt ha ⟩ )=b} : Set β) := by tauto
    have TS_finite := set_diff_finite T T_finite S
    have S_subset_T : S ⊆ T := by
      intro x hx
      rw [S_eq] at hx
      simp at hx
      rcases hx with ⟨ i , i_mapto_x ⟩
      rw [← i_mapto_x]
      simp

    have S_strict : Nat.card S < Nat.card T := by
      let g : Fin (a.succ) → β :=
        fun i => (order_set T T_finite card_T T_nonempty
        ⟨i, Nat.lt_trans i.is_lt ha⟩).1
      have S_eq' : S = Set.image g Set.univ := by
        simp
        ext c
        constructor
        intro cin
        rw [S_eq] at cin
        tauto
        intro cin
        rw [S_eq]
        tauto
      have S_card_le_a : Nat.card S ≤  Nat.succ a :=by
        simp
        rw [S_eq']
        have h : (Set.univ : Set (Fin (a.succ))).Finite := by
          have a : Finite (Fin (a.succ)) := by infer_instance
          exact Set.finite_univ_iff.2 a
        have H := Nat.card_image_le h (f:=g)
        have h1 :
          Nat.card (Set.univ : Set (Fin (Nat.succ a))) = a+1:= by simp
        rw [h1] at H
        simp at H
        simp
        exact H

      exact LE.le.trans_lt S_card_le_a ha
    have TS_nonempty :=   strict_set_diff_nonempty T T_finite S S_subset_T S_strict
    let m := (TS_finite.exists_minimal TS_nonempty).choose
    have hm : m ∈ T\S := (TS_finite.exists_minimal TS_nonempty).choose_spec.1
    simp at hm
    have hmin : m ∈ T := by
      rcases hm with ⟨ alpha , beta⟩
      exact alpha




    exact ⟨ m , hmin ⟩

Is it not recommended to use tactics like this ? I tried my best to figure out how to write this but at the end of the day I fell back into what I was more comfortable with. At the moment it seems like it will do what I want it to do, but I guess we will see later when I have try and post compose with inclusion function into beta (is this something I can do?)

[Aaron Liu]

If you're just doing let and have then the tactics aren't buying you anything since term mode also have those

[Quinn La Fond]

Well I use exact at the end and simp a couple of times

Also if I don't have by then the hypotheses from have don't show up on the right side of the screen

[Aaron Liu]

oh don't use simp

[Aaron Liu]

that's not good

[Aaron Liu]

Quinn La Fond said:

Also if I don't have by then the hypotheses from have don't show up on the right side of the screen

This usually means you cursor is not in the right place

[Quinn La Fond]

Why is simp bad?

[Aaron Liu]

it gives you casts

[Quinn La Fond]

Is it ok to use simp when proving the have statements

[Aaron Liu]

only use simp if the type of your goal is Prop

[Aaron Liu]

for example if your goal is ⊢ a = b then it's okay to use simp

[Quinn La Fond]

ok I actually didnt need the simp at all so I removed it

[Aaron Liu]

if your goal is ⊢ Fin (m + n) then don't use simp

[Quinn La Fond]

ok that makes sense I think

[Quinn La Fond]

So I am now running into the problem that when I call the function I defined, I can't access the hypothesis that that the value of this function is a minimum of some subset of T. is there a way to get this after using .choose?

[Yaël Dillies]

Would be easier if you had a #mwe, but from just reading your question the answer should be .choose_spec

[Quinn La Fond]

import Mathlib

open PrimeSpectrum
open Order
noncomputable
def order_chain {β : Type*} [PartialOrder β]
  (T : Set β) (T_chain : IsChain (· < ·) T)
  (T_finite : T.Finite) (T_nonempty : T.Nonempty) :
  Fin (1) → β
  | 0 =>  (T_finite.exists_minimal T_nonempty).choose

If I define the above function, then given a finite nonempty chain T, something like

rcases order_chain T T_chain T_finite T_nonempty 0 with \< a, b\>

gives the hypothesis a : Beta, b : a \in T, but I don't get any hypotheses of the form Minimal (fun x ↦ x ∈ T) a

[Quinn La Fond]

In particular I cannot change .choose to .choose_spec because then I don't have the element Beta, I have the element in beta+something else.

[Yaël Dillies]

The above wasn't quite a MWE :sweat: Is the following one accurate?

import Mathlib

variable {α β : Type*} [PartialOrder α] [PartialOrder β]

noncomputable
def order_chain (T : Set β) (T_finite : T.Finite) (T_nonempty : T.Nonempty) :
    Fin 1 → β
  | 0 => (T_finite.exists_minimal T_nonempty).choose

example (T : Set (α × β)) (T_finite : T.Finite) (T_nonempty : T.Nonempty) :
    True := by
  rcases order_chain T T_finite T_nonempty 0 with ⟨a, b⟩
  have : Minimal (· ∈ T) (a, b) := sorry
  trivial

[Yaël Dillies]

If so, then indeed you won't be able to fill in that sorry

[Quinn La Fond]

Why did you write T : Set (\alpha \times Beta)?

[Quinn La Fond]

Oh I see, my \< a , b\> is a : N and b : a <1 which are the necessary hypotheses to feed something to Fin 1.

[Aaron Liu]

you can use docs#Finset.orderIsoOfFin on the subtype of your chain which is a linear order

[Quinn La Fond]

Is this a different approach than defining my function from Fin (Nat.card T)\rightarrow Beta?

[Aaron Liu]

well you get an order isomorphism instead

[Quinn La Fond]

My beta is a partial order thought not a linear order.

[Aaron Liu]

the subtype of your chain is a linear order

[Quinn La Fond]

I see so this would give me a function Fin Nat.card T \rightarrow T?

[Quinn La Fond]

Is there not a way to just carry this hypothesis with me though? Like it seems odd to me that wit the expression (something).choose I can't access the propositions of that something.

[Aaron Liu]

can you provide a #mwe?

[Quinn La Fond]

import Mathlib

variable {α β : Type*} [PartialOrder α] [PartialOrder β]

noncomputable
def order_chain (T : Set β) (T_finite : T.Finite) (T_nonempty : T.Nonempty) :
    Fin 1 → β
  | 0 => (T_finite.exists_minimal T_nonempty).choose

example (T : Set (β)) (T_finite : T.Finite) (T_nonempty : T.Nonempty) :
    True := by
  rcases order_chain T T_finite T_nonempty 0 with a
  have h : Minimal (fun x => x ∈ T) a := sorry
  trivial

I am essentially just trying to fill in that sorry, but the only hypothesis (T_finite.exists_minimal T_nonempty).choose gives me is that a \in beta.

[Aaron Liu]

the problem is rcases forgets the value you pass it

[Aaron Liu]

you should use let instead

[Quinn La Fond]

import Mathlib

variable {α β : Type*} [PartialOrder α] [PartialOrder β]

noncomputable
def order_chain (T : Set β) (T_finite : T.Finite) (T_nonempty : T.Nonempty) :
    Fin 1 → β
  | 0 => (T_finite.exists_minimal T_nonempty).choose

example (T : Set (β)) (T_finite : T.Finite) (T_nonempty : T.Nonempty) :
    True := by
  let a : β := order_chain T T_finite T_nonempty 0
  have a_eq : a = order_chain T T_finite T_nonempty 0 := by tauto
  have h : Minimal (fun x => x ∈ T) a := by
   simp [order_chain] at a_eq
   sorry

  trivial

So this gives me that a= (T_finite.exists_minimal T_nonempty).choose, but how I don't how to access the hypothesis that a is now minimal with respect T.

[Aaron Liu]

it's (T_finite.exists_minimal T_nonempty).choose_spec

[Quinn La Fond]

import Mathlib

variable {α β : Type*} [PartialOrder α] [PartialOrder β]

noncomputable
def order_chain (T : Set β) (T_finite : T.Finite) (T_nonempty : T.Nonempty) :
    Fin 1 → β
  | 0 => (T_finite.exists_minimal T_nonempty).choose

example (T : Set (β)) (T_finite : T.Finite) (T_nonempty : T.Nonempty) :
    True := by
  let a : β := order_chain T T_finite T_nonempty 0
  have a_eq : a = order_chain T T_finite T_nonempty 0 := by tauto
  have h : Minimal (fun x => x ∈ T) a := by
   simp [order_chain] at a_eq
   exact  (T_finite.exists_minimal T_nonempty).choose_spec


  trivial

I don't totally understand why this works...like how does lean know that a is the same as this arbitrary (T_finite.exists_minimal T_nonempty).choose_spec?

[Aaron Liu]

because a let variable is definitionally equal to its value

[Aaron Liu]

You can try #check (T_finite.exists_minimal T_nonempty).choose_spec to see its type

[Quinn La Fond]

ok thank you i think that makes sense.