preferred spelling

Stream: mathlib4

[Andrew Yang]

(deleted)

[Andrew Yang]

I have some questions regarding the preferred spelling of various notions when working on some algebraic NT

1. Should primes in a dedekind domain be Prime p or [p.IsPrime] (_ : p ≠ ⊥) or [p.IsMaximal].
2. Should the multiplicity of some ideal p in I be multiplicity p I or (normalizedFactors I).count p or (factors I).count p?
3. Should an ring extension be (_ : Function.injective (algebraMap R S)) or [NoZeroSMulDivisors R S]
4. What is the preferred way do a standard AKLB setup? I'm currently using

variable (R K L S : Type*) [CommRing R] [CommRing S] [Algebra R S] [Field K] [Field L]
    [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] [Algebra S L]
    [Algebra K L] [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L]
    [IsIntegralClosure S R L] [FiniteDimensional K L]

But the first lines of almost all my proofs are setting up various IsNoetherian R S, NoZeroSMulDivisors R S IsDedekindDomain S IsFractionRing S L Algebra.IsIntegral R S instances.

5. Why is Algebra.IsIntegral R S not a class?

[Anne Baanen]

I don't think we have any consistent answers to this, so here are my weak preferences unhindered by the actual state of the library:

1. docs#Ideal.IsMaximal, since it works with the docs#Ideal.Quotient.field instance.
2. None of these options are satisfactory. docs#multiplicity seems like the obvious choice but since it takes values in docs#PartENat it's more annoying to work with than factors.count. I generally find docs#UniqueFactorizationMonoid.normalizedFactors to be more convenient to work with.
3. Even better would be a class that states Function.injective (algebraMap R S). But in this case that's equivalent to docs#NoZeroSMulDivisors, so I use the latter.
4. During development I generally make all of these hypotheses an extra variable, because it often turns out we can drop quite a few of the hypotheses. Only in the final theorem statement do I set up those instances from the AKLB setup.
5. It isn't? I recall being surprised by the same thing a couple of years ago and refactoring it into a class.

[Andrew Yang]

Thanks for the reply!

[Andrew Yang]

I remembered after asking the question that fields are dedekind domains in mathlib so p.IsMaximal isn't really equivalent to the other two...

[Anne Baanen]

Ah right, that explains why we have a lot of [I.IsPrime] (_ : I ≠ ⊥) too.

[Andrew Yang]

By the way, do you have a working definition of unramified extensions (of global fields) living somewhere? I heard on zulip that you had a chunk of global theory done.

[Anne Baanen]

I don't have a secret project to reveal, unfortunately! :) Since the port all my energy has gone into my thesis and tactics, and everything before that should already be in Mathlib.

[Filippo A. E. Nuccio]

With @María Inés de Frutos Fernández we have something about unramified extensions of local fields, but it is not in mathlib yet.