Naming for the setup of almost mathematics

Stream: maths

[Jiang Jiedong]

Hi everyone,

I am formalizing some basic definitions of almost ring theory. This is a pure naming problem. :joy:

In Wikipedia, Gabber and Romero's book, or papers, they simply write "Let $V$ be a ring and $m \subseteq V$ an idempotent ideal." or " Our basic setup consists of ..." without naming this pair $(V, m)$. Now I want to make this pair into a class as the basic setup of almost mathematics. Do you have any suggestions on what it should be called? Currently what is in my mind is AlmostPair, but I believe there must be a better name.

(Note that the nameAlmostRing refers to something else, namely a ring object the category of almost modules.)

[Adam Topaz]

What sort of class do you want to make? Note that you can already write

variable {R : Type*} [CommRing R] (I : Ideal R) (hI : IsIdempotentElem I)

although IsIdempotentElem is not a class.

[Jiang Jiedong]

Adam Topaz said:

What sort of class do you want to make?

Currently it is

open scoped TensorProduct

open Module

variable (V : Type*) [CommRing V] (m : Ideal V)

class AlmostPair : Prop where
  isIdempotent : IsIdempotentElem m
  flat_tensor : Flat V (m ⊗[V] m)

[Adam Topaz]

Aha ok, yes, I think something like this makes sense (note that you can make V implicit since it's in the type of m)

[Adam Topaz]

Maybe even use Ideal.AlmostPair so you can write [m.AlmostPair]

[Jiang Jiedong]

Adam Topaz said:

note that you can make V implicit since it's in the type of m

Yes. Good naming for this ideal only is also hard. :joy:

[Johan Commelin]

If we have Pair in the name, then I think I would prefer that V is explicit...

[Johan Commelin]

Would AlmostBasicSetting make sense?