Module

isReduced_of_smooth_of_field.lean

Nyll.AlgebraicCurves.Geometry.Schemes.isReduced_of_smooth_of_field

3 declarations indexed from sourceView source ↗

Module documentation

is Reduced of smooth of field

Imports2

Nyll.SchemeTheory.RingTheory.SmoothReduced
Mathlib.AlgebraicGeometry.Morphisms.Smooth

Imported by9

theorem

ringHomSmooth_appTop

L32 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_of_smooth_of_field.ringHomSmooth_appTop

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_of_smooth_of_field
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
universe u
section SchemeLevel

Lean source · statement

theorem ringHomSmooth_appTop {K : Type u} [Field K] {X : Scheme.{u}}
    [IsAffine X] (g : X ⟶ Spec (CommRingCat.of K)) [Smooth g] :
    RingHom.Smooth ((g.appTop).hom.comp ((Scheme.ΓSpecIso (CommRingCat.of K)).inv.hom))

theorem

isReduced_of_smooth_field

L44 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_of_smooth_of_field.AlgebraicGeometry.isReduced_of_smooth_field

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_of_smooth_of_field
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
universe u
section SchemeLevel
open scoped _root_.AlgebraicGeometry in

Lean source · statement

theorem AlgebraicGeometry.isReduced_of_smooth_field
    {K : Type u} [Field K] {X : Scheme.{u}} (sX : X ⟶ Spec (.of K)) [Smooth sX] :
    IsReduced X

theorem

isReduced_of_smooth_of_field

L62 ↗

AlgebraicGeometry.isReduced_of_smooth_of_field

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_of_smooth_of_field
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
universe u

Lean source · statement

theorem _root_.AlgebraicGeometry.isReduced_of_smooth_of_field {K : Type u} [Field K] {X :
  Scheme.{u}} (sX : X ⟶ Spec (.of K)) [Smooth sX] :
    IsReduced X

Module documentation

is Reduced of smooth of field

Declarations

ringHomSmooth_appTop

isReduced_of_smooth_field

isReduced_of_smooth_of_field