Module

ReducedEtale.lean

Nyll.SchemeTheory.Divisors.ReducedEtale

1 declaration indexed from sourceView source ↗

Module documentation

Reduced boundaries after etale pullback

The closed subscheme of a pulled-back ideal sheaf is the corresponding scheme-theoretic fibre product. An etale morphism over a locally Noetherian reduced base has reduced source, so radical boundary ideals remain radical.

Imports3

Mathlib.AlgebraicGeometry.Noetherian
Nyll.SchemeTheory.Divisors.Reduced
Nyll.SchemeTheory.Morphisms.EtaleReduced

Imported by2

theorem

comap_of_etale

L33 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsReduced.comap_of_etale

Documentation

A reduced ideal sheaf remains reduced after pullback by an etale morphism.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X Y : Scheme.{u}}

Lean source · statement

theorem IsReduced.comap_of_etale (I : X.IdealSheafData)
    (hI : I.IsReduced) (f : Y ⟶ X) [Etale f]
    [IsLocallyNoetherian X] : (I.comap f).IsReduced

Module documentation

Reduced boundaries after etale pullback

Declarations

comap_of_etale