Module

Smooth_isReduced_of_isReduced_of_isLocallyNoetherian.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_isReduced_of_isReduced_of_isLocallyNoetherian

2 declarations indexed from sourceView source ↗

Module documentation

Smooth is Reduced of is Reduced of is Locally Noetherian

Imports6

Mathlib.AlgebraicGeometry.Geometrically.Reduced
Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Noetherian
Mathlib.AlgebraicGeometry.Properties
Mathlib.CategoryTheory.MorphismProperty.Limits
Nyll.AlgebraicCurves.Geometry.Schemes.isReduced_of_smooth_of_field

Imported by4

theorem

geometricallyReduced_of_smooth

L36 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_isReduced_of_isReduced_of_isLocallyNoetherian.REDsol.geometricallyReduced_of_smooth

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Smooth_isReduced_of_isReduced_of_isLocallyNoetherian
universe u
open CategoryTheory AlgebraicGeometry
namespace REDsol

Lean source · statement

theorem geometricallyReduced_of_smooth {X Y : Scheme.{u}} (f : X ⟶ Y) [Smooth f] :
  GeometricallyReduced f

theorem

isReduced_of_isReduced_of_isLocallyNoetherian

L44 ↗

AlgebraicGeometry.Smooth.isReduced_of_isReduced_of_isLocallyNoetherian

Source context 5 commands