NYLL
Module

FiniteGeometricallyReducedEtale.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.FiniteGeometricallyReducedEtale
2 declarations indexed from sourceView source ↗

Module documentation

Finite geometrically reduced algebras over fields

The geometric-fibre algebra in the proper-family argument is finite étale: after extending the field to an algebraic closure it is a finite product of fields, and étaleness descends along the field extension.

Imports3
  • Mathlib.RingTheory.Etale.Field
  • Mathlib.RingTheory.Etale.Descent
  • Mathlib.RingTheory.Nilpotent.GeometricallyReduced
Imported by2

Declarations

theorem

etale_of_finite_of_isReduced_of_perfectField

L28 ↗
Algebra.etale_of_finite_of_isReduced_of_perfectField
Documentation

A finite reduced algebra over a perfect field is étale.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace Algebra
universe u
Lean source · statement
theorem etale_of_finite_of_isReduced_of_perfectField
    (K A : Type u) [Field K] [PerfectField K] [CommRing A] [Algebra K A]
    [Module.Finite K A] [IsReduced A] : Etale K A
theorem

etale_of_finite_of_isReduced_algebraicClosure_tensorProduct

L42 ↗
Algebra.etale_of_finite_of_isReduced_algebraicClosure_tensorProduct
Documentation

Reducedness after algebraic closure is sufficient for a finite algebra over a field to be étale.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace Algebra
universe u
Lean source · statement
theorem etale_of_finite_of_isReduced_algebraicClosure_tensorProduct
    (K A : Type u) [Field K] [CommRing A] [Algebra K A]
    [Module.Finite K A] [IsReduced (AlgebraicClosure K ⊗[K] A)] : Etale K A

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.