Confusion about S.Nonempty/Finite and Nonempty/FinteS syntax

Stream: mathlib4

[Quinn La Fond]

Hi All,

I am new to Lean and have come across some syntax I do not really understand. I apologize if this is a silly question, or if this covered in Mathematics in Lean.

For context so that I do not ask an XY problem, my main goal is to show that if

$$A\rightarrow B$$

is an integral extension of rings, then their Krull Dimensions are equal. In the part of showing dim A < dim B, the crux of the proof should be that given a chain of prime ideals in A of length n we can construct a chain of prime ideals in B of the same length. I believe this is potentially best said with the following lemma:

lemma chainA_to_chainB : (∀ S : Set (PrimeSpectrum A), IsChain (· < ·) S → S.Finite
   → ∃ T : Set (PrimeSpectrum B),
    IsChain (· < ·) T ∧  T.Finite ∧ (Nat.card S = Nat.card T) )

and then proving this by induction and the going up lemma ( I declared commutative rings A and B and an injective integral map \phi between them earlier).

The base case is easy to formalize, but in the inductive case I am running into a problem during the following conceptual step: remove the maximal element from S and apply the inductive hypothesis to get a chain of prime ideals in B. In particular, it seems the lemma I should use here is Set.Finite.exists_maximal, but this requires a proof of S.Nonempty. This shouldn't be hard because by assumption Nat.card S>0 in this step, but the only statement I can find that related Nat.card S >0 to non emptiness is Nat.card_pos_iff which can be used to rewrite Nat.card S>0 as Nonempty S. I suspect that I am mixing up things across libraries, since Nat.card_pos_iff is in Mathlib.SetTheory.Cardinal.Finite and uses things like Nonempty S everywhere, while Set.Finite.exists_maximal is in Mathlib.Order.Preorder.Finite and uses things like S.Nonempty everywhere.

Ultimately, after reading the libraries I see that S.Nonempty "expresses the fact that S is non empty" and
that Nonempty S says that S is not an empty type, but I don't understand why they are seemingly used interchangeably without an obvious way to relate the two statements (my apologies if this is not true, I just haven't found one). Any help or advice on this matter would be greatly appreciated. I will note that in the set theory chapter on Mathemtics in Lean, which I have worked a bit through, they use statements like Nonempty S and not S.Nonempty.

Best,

Quinn

[Aaron Liu]

@loogle Finset.Nonempty, Nonempty

[loogle]

:search: Finset.Nonempty.to_type, Finset.Nonempty.coe_sort, and 15 more

[Yaël Dillies]

The lemma linking the two notions is docs#Set.nonempty_coe_sort

[Quinn La Fond]

@Aaron Liu thank you I was unaware of Looggle

[Quinn La Fond]

@Yaël Dillies Thank you as well, I don't know why I could not find that, and that has fixed this problem. Do you know what the actual difference between these two things is though? I don't quite understand the point of it

[Yaël Dillies]

See recent discussion about it: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Filter.2ENeBot.20typeclass/near/527433305