Documentation

Mathlib.AlgebraicGeometry.Morphisms.Etale

Etale morphisms #

A morphism of schemes f : X ⟶ Y is étale if it is smooth of relative dimension zero. We also define the category of schemes étale over X.

@[reducible, inline]

A morphism of schemes is étale if it is smooth of relative dimension zero.

Equations

The forgetful functor from schemes étale over X to schemes over X is fully faithful.

Equations
  • One or more equations did not get rendered due to their size.