Module

Algebra_Etale_isReduced_of_isReduced_of_isNoetherianRing.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_Etale_isReduced_of_isReduced_of_isNoetherianRing

2 declarations indexed from sourceView source ↗

Module documentation

Algebra Etale is Reduced of is Reduced of is Noetherian Ring

Imports5

Mathlib.AlgebraicGeometry.Geometrically.Reduced
Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.RingTheory.Etale.Basic
Mathlib.RingTheory.Smooth.Flat
Mathlib.RingTheory.Unramified.Field

Imported by3

theorem

geometricallyReduced_specMap

L35 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Algebra_Etale_isReduced_of_isReduced_of_isNoetherianRing.EtaleReducedAux.geometricallyReduced_specMap

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Algebra_Etale_isReduced_of_isReduced_of_isNoetherianRing
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleReducedAux

Lean source · statement

theorem geometricallyReduced_specMap (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
  [Algebra.Etale R S] :
    GeometricallyReduced (Spec.map (CommRingCat.ofHom (algebraMap R S)))

theorem

isReduced_of_isReduced_of_isNoetherianRing

L54 ↗

Algebra.Etale.isReduced_of_isReduced_of_isNoetherianRing

Source context 6 commands