Documentation

Mathlib.RingTheory.Etale.Weakly

Weakly étale algebras #

In this file we define weakly étale algebras. An R-algebra S is weakly étale if S is R-flat and the multiplication map S ⊗[R] S → S is flat.

TODOs #

source
class Algebra.WeaklyEtale (R : Type u_3) (S : Type u_4) [CommRing R] [CommRing S] [Algebra R S] :
Prop

S is a weakly-étale R-algebra if both R → S and S ⊗[R] S → R are flat. This is also called absolutely flat.

Instances
    source
    theorem Algebra.weaklyEtale_iff (R : Type u_3) (S : Type u_4) [CommRing R] [CommRing S] [Algebra R S] :
    WeaklyEtale R S ↔ autoParam (Module.Flat R S) WeaklyEtale.flat._autoParam ∧ (TensorProduct.lmul' R).Flat
    source
    theorem Algebra.WeaklyEtale.ulift_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] :
    WeaklyEtale (ULift.{u₁, u_1} R) (ULift.{u₂, u_2} S) ↔ WeaklyEtale R S
    source
    @[instance 100]
    instance Algebra.WeaklyEtale.instOfEtale {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Etale R S] :
    WeaklyEtale R S

    Stacks Tag 092N ((2))

    source
    instance Algebra.WeaklyEtale.instTensorProduct {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_3} [CommRing T] [Algebra R T] [WeaklyEtale R S] :
    WeaklyEtale T (TensorProduct R T S)

    Stacks Tag 092H ((2))

    source
    theorem Algebra.WeaklyEtale.trans (R : Type u₁) (S : Type u₂) [CommRing R] [CommRing S] [Algebra R S] (T : Type u₃) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [WeaklyEtale R S] [WeaklyEtale S T] :
    WeaklyEtale R T

    Stacks Tag 092J ((2))