Documentation

Mathlib.RingTheory.Flat.Algebra

Flat algebras and flat ring homomorphisms #

We define flat algebras and flat ring homomorphisms.

Main definitions #

source
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.

Instances
    source
    theorem Algebra.Flat.out {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [self : Algebra.Flat R S] :
    Module.Flat R S
    source
    instance Algebra.Flat.self (R : Type u) [CommRing R] :
    Algebra.Flat R R
    Equations
    • ⋯ = ⋯
    source
    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] :
    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.

    source
    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] :
    Algebra.Flat T (TensorProduct R T S)

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

    Equations
    • ⋯ = ⋯
    source
    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'] :
    Algebra.Flat S S'

    A base change of a flat algebra is flat.

    source
    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.

    Instances
      source
      theorem RingHom.Flat.out {R : Type u} {S : Type v} [CommRing R] [CommRing S] {f : R →+* S} [self : f.Flat] :
      Algebra.Flat R S
      source
      instance RingHom.Flat.identity (R : Type u) [CommRing R] :
      RingHom.Flat 1

      The identity of a ring is flat.

      Equations
      • ⋯ = ⋯
      source
      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
      • ⋯ = ⋯