Module

Descent.lean

Nyll.SchemeTheory.Pi1.FiniteEtale.Algebra.Descent

1 declaration indexed from sourceView source ↗

Module documentation

Faithfully flat descent of finite etale algebras

An algebra whose tensor product with a faithfully flat base algebra is finite etale is itself finite etale, by descending etaleness and module finiteness separately.

Imports2

Mathlib.RingTheory.Etale.Descent
Nyll.SchemeTheory.Pi1.FiniteEtale.Algebra.Basic

Imported by2

lemma

of_finiteEtale_tensorProduct_of_faithfullyFlat

L36 ↗

Algebra.FiniteEtale.of_finiteEtale_tensorProduct_of_faithfullyFlat

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
universe u v w
open TensorProduct

Lean source · statement

lemma Algebra.FiniteEtale.of_finiteEtale_tensorProduct_of_faithfullyFlat {R S : Type u}
    [CommRing R] [CommRing S] [Algebra R S]
    (T : Type u) [CommRing T] [Algebra R T] [Module.FaithfullyFlat R T]
    [Algebra.FiniteEtale T (T ⊗[R] S)] :
    Algebra.FiniteEtale R S

Module documentation

Faithfully flat descent of finite etale algebras

Declarations

of_finiteEtale_tensorProduct_of_faithfullyFlat