ModuleEtaleSource.lean
Nyll.SchemeTheory.RingTheory.Descent.EtaleSource
2 declarations indexed from sourceView source ↗ Module documentation
Étaleness descends through a faithfully flat étale source cover
For a tower R → A → B, faithful flatness of A → B reflects the ideal injectivity criterion for flatness. The existing iterated-base-change identity supplies the comparison, without any new tensor construction.
If both R → B and A → B are étale, the existing differential equivalence reflects formal unramifiedness to R → A. Source-side finite-presentation descent supplies the remaining finite-presentation condition, so R → A is genuinely étale.
Imports8
- Nyll.SchemeTheory.RingTheory.Descent.FinitePresentation
- Mathlib.LinearAlgebra.TensorProduct.Tower
- Mathlib.RingTheory.Etale.Kaehler
- Mathlib.RingTheory.Flat.Basic
- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
- Mathlib.RingTheory.Flat.Tensor
- Mathlib.RingTheory.Smooth.Fiber
- Mathlib.RingTheory.Smooth.Flat
Imported by2
Declarations
SchemeTheory.flat_of_faithfullyFlat_of_flat
DocumentationFlatness descends through a faithfully flat source extension.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped TensorProduct
namespace SchemeTheory
universe u v w
variable (R : Type u) (A : Type v) (B : Type w)
[CommRing R] [CommRing A] [CommRing B]
[Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
SchemeTheory.etale_of_faithfullyFlat_of_etale
DocumentationA faithfully flat étale source cover detects genuine étaleness of the original algebra. Both finite-presentation inputs come from the two given étale maps and are descended by the existing source-side owner.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped TensorProduct
namespace SchemeTheory
universe u v w
variable (R : Type u) (A : Type v) (B : Type w)
[CommRing R] [CommRing A] [CommRing B]
[Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B]