Module

EtaleFromLocalizations.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.EtaleFromLocalizations

1 declaration indexed from sourceView source ↗

Module documentation

Étaleness of a finite-projective algebra from base localizations

The differentials vanish after every maximal localization of the base, because the actual tensor algebra there is étale. Localization detects vanishing, and finite projectivity supplies flatness and finite presentation.

Imports5

Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Mathlib.RingTheory.Kaehler.TensorProduct
Mathlib.RingTheory.LocalProperties.Submodule
Mathlib.RingTheory.Localization.BaseChange
Mathlib.RingTheory.Smooth.Fiber

Imported by3

theorem

etale_of_finite_projective_of_etale_localizations

L31 ↗

Algebra.etale_of_finite_projective_of_etale_localizations

Documentation

A finite-projective algebra is étale if its actual base changes to all maximal localizations of the base ring are étale.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace Algebra
universe u v

Lean source · statement

theorem etale_of_finite_projective_of_etale_localizations
    (R : Type u) (B : Type v) [CommRing R] [CommRing B] [Algebra R B]
    [Module.Finite R B] [Module.Projective R B]
    (hLocal : ∀ (p : Ideal R) [p.IsMaximal],
      Etale (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] B)) :
    Etale R B

Module documentation

Étaleness of a finite-projective algebra from base localizations

Declarations

etale_of_finite_projective_of_etale_localizations