Documentation

Mathlib.RingTheory.Flat.Algebra

Flat algebras and flat ring homomorphisms #

We define flat algebras and flat ring homomorphisms.

Main definitions #

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

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

Instances
    theorem Algebra.Flat.out {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [self : Algebra.Flat R S] :
    instance Algebra.Flat.self (R : Type u) [CommRing R] :
    Equations
    • =
    theorem Algebra.Flat.comp (R : Type u) (S : Type v) [CommRing R] [CommRing S] (T : Type w) [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.Flat R S] [Algebra.Flat S T] :

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

    instance Algebra.Flat.baseChange (R : Type u) (S : Type v) [CommRing R] [CommRing S] (T : Type w) [CommRing T] [Algebra R S] [Algebra R T] [Algebra.Flat R S] :

    If S is a flat R-algebra and T is any R-algebra, then T ⊗[R] S is a flat T-algebra.

    Equations
    • =
    theorem Algebra.Flat.isBaseChange (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (R' : Type w) (S' : Type t) [CommRing R'] [CommRing S'] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : Algebra.IsPushout R S R' S'] [Algebra.Flat R R'] :

    A base change of a flat algebra is flat.

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

    A ring homomorphism f : R →+* S is flat if S is flat as an R algebra.

    Instances
      theorem RingHom.Flat.out {R : Type u} {S : Type v} [CommRing R] [CommRing S] {f : R →+* S} [self : f.Flat] :

      The identity of a ring is flat.

      Equations
      • =
      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) [f.Flat] [g.Flat] :
      (g.comp f).Flat

      Composition of flat ring homomorphisms is flat.

      Equations
      • =