Flat algebras and flat ring homomorphisms

We define flat algebras and flat ring homomorphisms.

Main definitions

• Algebra.Flat: an R-algebra S is flat if it is flat as R-module
• RingHom.Flat: a ring homomorphism f : R → S is flat, if it makes S into a flat R-algebra

class Algebra.Flat (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Prop

An R-algebra S is flat if it is flat as R-module.

• out : Module.Flat R S

instance Algebra.Flat.self (R : Type u) [CommRing R] : Algebra.Flat R R

Equations

• (_ : Algebra.Flat R R) = (_ : Algebra.Flat R R)

theorem Algebra.Flat.comp (R : Type u) (S : Type v) (T : Type w) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.Flat R S] [Algebra.Flat S T] : Algebra.Flat R T

If T is a flat S-algebra and S is a flat R-algebra, then T is a flat R-algebra.

class RingHom.Flat {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) : Prop

A RingHom is flat if R is flat as an S algebra.

• out : Algebra.Flat R S

instance RingHom.Flat.identity (R : Type u) [CommRing R] : RingHom.Flat 1

The identity of a ring is flat.

Equations

• (_ : RingHom.Flat 1) = (_ : RingHom.Flat 1)

instance RingHom.Flat.comp {R : Type u} {S : Type v} {T : Type w} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) [RingHom.Flat f] [RingHom.Flat g] : RingHom.Flat (RingHom.comp g f)

Composition of flat ring homomorphisms is flat.

Equations

• (_ : RingHom.Flat (RingHom.comp g f)) = (_ : RingHom.Flat (RingHom.comp g f))