Smooth morphism of rings

Stream: mathlib4

[Kevin Buzzard]

OK so we "have smooth morphisms of rings" because docs#Algebra.Smooth. But right now when I try to use it I realise I have to write this:

import Mathlib.RingTheory.Smooth.Basic

variable (R A : Type) [CommRing R] [CommRing A]

def IsSmooth (f : R →+* A) : Prop :=
  @Algebra.Smooth R _ A _ (RingHom.toAlgebra f)

Is this (IsSmooth) a definition we want in mathlib? I don't think that assuming all maps which we want to talk about the smoothness of come from an Algebra class is a sustainable idea? We need to prove various facts about smooth morphisms of rings in order to beef up the definition to smooth morphisms of schemes, and I'm not sure that the Algebra approach is going to scale.

[Kevin Buzzard]

cc @FMLJohn (who is thinking about his right now) and also @Andrew Yang , @Jujian Zhang and @Christian Merten

[Johan Commelin]

Yes, I think that def is good. Although maybe RingHom.IsSmooth as name.

[Eric Wieser]

Is there a notion of smooth morphisms of non-commutative rings? If so, the approach of going via algebras doesn't work.

[Christian Merten]

Johan Commelin said:

Yes, I think that def is good. Although maybe RingHom.IsSmooth as name.

Although I generally like the Is convention, the general pattern seems to keep the Algebra.Property consistent with RingHom.Property (e.g. Algebra.Flat and RingHom.Flat, Algebra.FiniteType and RingHom.FiniteType). So I suggest RingHom.Smooth.

[Johan Commelin]

I agree consistency is good. I think I would be in favor of converging to Algebra.P and RingHom.IsP. If others agree, we should do a large rename in the near future (-;

[Johan Commelin]

Eric Wieser said:

Is there a notion of smooth morphisms of non-commutative rings? If so, the approach of going via algebras doesn't work.

I have never heard of that notion. But I'm not really an expert on non-commutative algebra.

[Christian Merten]

Johan Commelin said:

I agree consistency is good. I think I would be in favor of converging to Algebra.P and RingHom.IsP. If others agree, we should do a large rename in the near future (-;

Why not Algebra.IsP and RingHom.IsP?

[Johan Commelin]

Good point, I don't know what I was thinking :rofl: