Module

isReduced_of_smooth_over_field.lean

Nyll.AlgebraicCurves.Geometry.Schemes.isReduced_of_smooth_over_field

4 declarations indexed from sourceView source ↗

Module documentation

Smooth schemes over a field are reduced

Reducedness of étale algebras and local standard-smooth presentations establish reducedness of smooth schemes over a field.

Imports8

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Properties
Mathlib.RingTheory.RingHom.LocallyStandardSmooth
Mathlib.RingTheory.Unramified.Field
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.Etale.Basic
Mathlib.RingTheory.Smooth.Flat
Mathlib.RingTheory.Flat.Basic

Imported by3

theorem

etale_isReduced

L39 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_of_smooth_over_field.IsReducedOfSmoothFieldAux.etale_isReduced

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_of_smooth_over_field
universe u
open TensorProduct
namespace IsReducedOfSmoothFieldAux

Lean source · statement

theorem etale_isReduced (K A : Type*) [Field K] [CommRing A] [Algebra K A]
    [Algebra.Etale K A] : IsReduced A

theorem

isStandardSmooth_isReduced_of_isDomain

L45 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_of_smooth_over_field.IsReducedOfSmoothFieldAux.isStandardSmooth_isReduced_of_isDomain

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_of_smooth_over_field
universe u
open TensorProduct
namespace IsReducedOfSmoothFieldAux

Lean source · statement

theorem isStandardSmooth_isReduced_of_isDomain
    {R A : Type u} [CommRing R] [CommRing A] [IsDomain R] {φ : R →+* A}
    (hφ : φ.IsStandardSmooth) : IsReduced A

theorem

smooth_isReduced_of_isDomain

L62 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_of_smooth_over_field.IsReducedOfSmoothFieldAux.smooth_isReduced_of_isDomain

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_of_smooth_over_field
universe u
open TensorProduct
namespace IsReducedOfSmoothFieldAux

Lean source · statement

theorem smooth_isReduced_of_isDomain
    {R A : Type u} [CommRing R] [CommRing A] [IsDomain R] {φ : R →+* A}
    (hφ : φ.Smooth) : IsReduced A

theorem