ring properties: local -> global

Stream: maths

[Kenny Lau]

(This is not a fully-formed idea yet, I'm just throwing something out there.)
I'm wondering if there's a way to make sense of the philosophy of going from local to global. For example, I would like to define the term "locally free" correctly. This means that I would have the property "free" defined, and then a function "locally" defined, say:

Free: R-Module -> Prop
Locally: (R-Module -> Prop) -> (R-Module -> Prop)

so that I can do Locally Free : R-Module -> Prop.

I want to make sense of the type R-Module -> Prop in terms of category theory. It's clear that this type is nonsense until it respects all isomorphisms, which sounds like a category theory statement.

PS: I feel like meta-theoretically, all definable terms R-Module -> Prop respect isomorphisms anyway.

[Christian Merten]

Are you aware of docs#RingHom.Locally, which is something similar for properties of ring homomorphisms?

[Kenny Lau]

Christian Merten said:

Are you aware of docs#RingHom.Locally, which is something similar for properties of ring homomorphisms?

aha, thanks! that is not about modules, but it's still useful to know that it exists for ring homs. do you know what it's used for?

[Christian Merten]

(btw: for locally free, we typically just say finite projective or finitely presented + flat. Things around docs#Module.isOpen_freeLocus and docs#Module.free_of_flat_of_isLocalRing will be useful)

[Kenny Lau]

Wow!

[Christian Merten]

Kenny Lau said:

Christian Merten said:

Are you aware of docs#RingHom.Locally, which is something similar for properties of ring homomorphisms?

aha, thanks! that is not about modules, but it's still useful to know that it exists for ring homs. do you know what it's used for?

It is used to force certain properties of ring homs into the framework of docs#RingHom.PropertyIsLocal that are not necessarily local on the target (i.e., geometric source). It is used to characterise smooth morphisms of schemes as locally standard smooth (see docs#AlgebraicGeometry.instHasRingHomPropertyIsSmoothLocallyIsStandardSmooth)

[Kenny Lau]

import Mathlib

class Module.LocallyFree (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M] : Prop
  extends Module.Free R M, Module.Projective R M

variable (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M]

class Module.Invertible : Prop extends Module.LocallyFree R M where
  rank1 : ∀ p : PrimeSpectrum R, Module.rankAtStalk M p = 1

@Christian Merten so, is this the "canonical" way to write this?

[Christian Merten]

Did you mean to say Module.Finite instead of Module.Free in the first class?

[Kenny Lau]

ah, yes, nice catch

[Kenny Lau]

oh wait, then it's not mathematically accurate unless for finite modules... lol

[Kenny Lau]

does anyone think that R[X] is "locally free"?

[Christian Merten]

I would say "locally free" is rarely used in a non-finite context. I am not sure if you need a name for it anyway, you can just assume [Module.Finite R M] [Module.Projective R M].

[Kenny Lau]

https://stacks.math.columbia.edu/tag/00NV
yes, I can confirm that people usually assume "finite", i'm just complaining about the name, i guess this is fine

[Christian Merten]

Note that there is an open PR (#22341) with some more API for docs#Module.rankAtStalk

[Kenny Lau]

nice, thanks

[Christian Merten]

Also @Junyan Xu has thought about invertible modules and the picard group earlier this year (only thread I could find on the spot: #maths > Puzzles around Picard group )

[Kenny Lau]

well, yeah i'm sure i'm not the first one to ask about this; kevin buzzard already asked this back in 2020: #Is there code for X? > invertible modules are f.g.