Module

LocalEtaleFromClosedFiber.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.LocalEtaleFromClosedFiber

1 declaration indexed from sourceView source ↗

Module documentation

Étaleness of a finite projective algebra over a local ring

Étaleness on the closed fibre kills the residue-field extension of the finite module of differentials. Nakayama kills the original differentials. Finite projectivity supplies flatness and finite presentation.

Imports4

Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Mathlib.RingTheory.Kaehler.TensorProduct
Mathlib.RingTheory.LocalRing.Module
Mathlib.RingTheory.Smooth.Fiber

Imported by2

theorem

etale_of_finite_projective_of_etale_closedFiber

L30 ↗

Algebra.etale_of_finite_projective_of_etale_closedFiber

Documentation

A finite projective algebra over a local ring is étale when its actual closed-fibre algebra is étale. No Noetherian hypothesis is needed.

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_closedFiber
    (R : Type u) (B : Type v) [CommRing R] [IsLocalRing R] [CommRing B]
    [Algebra R B] [Module.Finite R B] [Module.Projective R B]
    [Etale (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField R ⊗[R] B)] :
    Etale R B

Module documentation

Étaleness of a finite projective algebra over a local ring

Declarations

etale_of_finite_projective_of_etale_closedFiber