Module

RingHom.lean

Nyll.SchemeTheory.Pi1.Etale.RingHom

4 declarations indexed from sourceView source ↗

Module documentation

Local criteria for étale ring homomorphisms

Étaleness is characterized by local standard smoothness of relative dimension zero, including the degenerate subsingleton algebra case.

Imports1

Mathlib.RingTheory.RingHom.LocallyStandardSmooth

Imported by3

instance

(anonymous instance)

L40 ↗

Source context 4 commands

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

@[expose] public section
universe u
namespace Algebra
variable {ι : Type*}

Lean source · statement

instance {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [Subsingleton S]
    (n : ℕ) : IsStandardSmoothOfRelativeDimension n R S

instance

(anonymous instance)

L56 ↗

Source context 4 commands

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

@[expose] public section
universe u
namespace Algebra
variable {ι : Type*}

Lean source · statement

instance (priority := low) {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [IsStandardSmooth R S] [FormallyUnramified R S] :
    IsStandardSmoothOfRelativeDimension 0 R S

lemma

eq_and

L71 ↗

RingHom.Etale.eq_and

Source context 3 commands

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

@[expose] public section
universe u
namespace RingHom

Lean source · full declaration

lemma Etale.eq_and :
    @Etale = fun R S (_ : CommRing R) (_ : CommRing S) f ↦ f.FormallyUnramified ∧ f.Smooth := by
  ext
  rw [etale_iff_formallyUnramified_and_smooth]

theorem

iff_locally_isStandardSmoothOfRelativeDimension

L76 ↗

RingHom.Etale.iff_locally_isStandardSmoothOfRelativeDimension

Source context 3 commands

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

@[expose] public section
universe u
namespace RingHom

Lean source · statement

theorem Etale.iff_locally_isStandardSmoothOfRelativeDimension
    {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) :
    f.Etale ↔ Locally (IsStandardSmoothOfRelativeDimension 0) f

Module documentation

Local criteria for étale ring homomorphisms

Declarations

(anonymous instance)

(anonymous instance)

eq_and

iff_locally_isStandardSmoothOfRelativeDimension