NYLL
Module

GeometricallyReduced_of_isReduced_of_perfectField.lean

Nyll.AlgebraicCurves.Geometry.Schemes.GeometricallyReduced_of_isReduced_of_perfectField
3 declarations indexed from sourceView source ↗

Module documentation

Geometrically Reduced of is Reduced of perfect Field

Imports7
Imported by2

Declarations

instance

isReduced_isClosedUnderIsomorphisms

L34 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.GeometricallyReduced_of_isReduced_of_perfectField.F2aux.isReduced_isClosedUnderIsomorphisms
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.GeometricallyReduced_of_isReduced_of_perfectField
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u v w
namespace F2aux
Lean source · full declaration
instance isReduced_isClosedUnderIsomorphisms :
    ObjectProperty.IsClosedUnderIsomorphisms (IsReduced : ObjectProperty Scheme.{u}) where
  of_iso e _ := isReduced_of_isOpenImmersion e.inv
lemma

isReduced_pullback_Spec

L38 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.GeometricallyReduced_of_isReduced_of_perfectField.F2aux.isReduced_pullback_Spec
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.GeometricallyReduced_of_isReduced_of_perfectField
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u v w
namespace F2aux
Lean source · statement
lemma isReduced_pullback_Spec {k : Type u} [Field k] [PerfectField k]
    {R : CommRingCat.{u}} (g : Spec R ⟶ Spec (CommRingCat.of k)) (hred : IsReduced (Spec R))
    (hft : LocallyOfFiniteType g) (K : Type u) [Field K] [Algebra k K] :
    IsReduced (pullback g (Spec.map (CommRingCat.ofHom (algebraMap k K))))
theorem

of_isReduced_of_perfectField

L64 ↗
AlgebraicGeometry.GeometricallyReduced.of_isReduced_of_perfectField
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.GeometricallyReduced_of_isReduced_of_perfectField
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u v w
attribute [local instance] F2aux.isReduced_isClosedUnderIsomorphisms
Lean source · statement
theorem _root_.AlgebraicGeometry.GeometricallyReduced.of_isReduced_of_perfectField {k : Type u}
  [Field k] [PerfectField k] {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of k)) [LocallyOfFiniteType f] [IsReduced X] :
    GeometricallyReduced f

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