Module

isReduced_pullback_residue_of_forall_isReduced_stalk_quotient.lean

Nyll.AlgebraicCurves.Geometry.Schemes.isReduced_pullback_residue_of_forall_isReduced_stalk_quotient

7 declarations indexed from sourceView source ↗

Module documentation

is Reduced pullback residue of forall is Reduced stalk quotient

Imports6

Mathlib.AlgebraicGeometry.Properties
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.AlgebraicGeometry.StructureSheaf
Mathlib.RingTheory.LocalProperties.Basic
Mathlib.RingTheory.TensorProduct.Quotient
Mathlib.RingTheory.LocalRing.ResidueField.Defs

Imported by1

Nyll.AlgebraicCurves.Geometry.Schemes.All

theorem

isReduced_quotient_map_of_forall_isReduced_localization

L35 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_pullback_residue_of_forall_isReduced_stalk_quotient.CFSAux.isReduced_quotient_map_of_forall_isReduced_localization

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isReduced_pullback_residue_of_forall_isReduced_stalk_quotient
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace CFSAux

Lean source · statement

theorem isReduced_quotient_map_of_forall_isReduced_localization
    {A R : Type*} [CommRing A] [CommRing R] (φ : A →+* R) (I : Ideal A)
    (h : ∀ (𝔮 : Ideal R) [𝔮.IsPrime], I.map φ ≤ 𝔮 →
      IsReduced (Localization.AtPrime 𝔮 ⧸ I.map ((algebraMap R (Localization.AtPrime 𝔮)).comp φ))) :
    IsReduced (R ⧸ I.map φ)

theorem

isReduced_of_ringEquiv

L70 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_pullback_residue_of_forall_isReduced_stalk_quotient.CFSAux.isReduced_of_ringEquiv

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isReduced_pullback_residue_of_forall_isReduced_stalk_quotient
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace CFSAux

Lean source · statement

theorem isReduced_of_ringEquiv {R S : Type*} [CommRing R] [CommRing S] (e : R ≃+* S) [IsReduced R] :
    IsReduced S

theorem

base_eq_closedPoint_iff

L80 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_pullback_residue_of_forall_isReduced_stalk_quotient.CFSGlue.base_eq_closedPoint_iff

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isReduced_pullback_residue_of_forall_isReduced_stalk_quotient
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace CFSGlue
variable {A : Type u} [CommRing A] [IsLocalRing A]

Lean source · statement

theorem base_eq_closedPoint_iff {R : CommRingCat.{u}} (φ : Spec R ⟶ Spec (CommRingCat.of A)) (𝔮 :
  PrimeSpectrum R) :
    φ.base 𝔮 = IsLocalRing.closedPoint A ↔
      (IsLocalRing.maximalIdeal A).map (Spec.preimage φ).hom ≤ 𝔮.asIdeal

theorem

isReduced_pullback_affine

L101 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_pullback_residue_of_forall_isReduced_stalk_quotient.CFSGlue.isReduced_pullback_affine

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isReduced_pullback_residue_of_forall_isReduced_stalk_quotient
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace CFSGlue
variable {A : Type u} [CommRing A] [IsLocalRing A]

Lean source · statement

theorem isReduced_pullback_affine {R : CommRingCat.{u}} (φ : Spec R ⟶ Spec (CommRingCat.of A))
    (h : ∀ 𝔮 : PrimeSpectrum R, (IsLocalRing.maximalIdeal A).map (Spec.preimage φ).hom ≤ 𝔮.asIdeal →
      _root_.IsReduced (Localization.AtPrime 𝔮.asIdeal ⧸
        (IsLocalRing.maximalIdeal A).map ((algebraMap R (Localization.AtPrime 𝔮.asIdeal)).comp
          (Spec.preimage φ).hom))) :
    IsReduced (pullback φ (Spec.map (CommRingCat.ofHom (IsLocalRing.residue A))))

theorem

isReduced_localization_quotient_of_stalk

L127 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_pullback_residue_of_forall_isReduced_stalk_quotient.CFSGlue.isReduced_localization_quotient_of_stalk

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isReduced_pullback_residue_of_forall_isReduced_stalk_quotient
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace CFSGlue
variable {A : Type u} [CommRing A] [IsLocalRing A]

Lean source · statement

theorem isReduced_localization_quotient_of_stalk {X : Scheme.{u}} (toBase : X ⟶ Spec
  (CommRingCat.of A))
    {R : CommRingCat.{u}} (j : Spec R ⟶ X) [IsOpenImmersion j] (𝔮 : PrimeSpectrum R)
    (hred : _root_.IsReduced (X.presheaf.stalk (j.base 𝔮) ⧸
        Ideal.map ((X.presheaf.germ ⊤ (j.base 𝔮) trivial).hom.comp
          (toBase.appTop.hom.comp (Scheme.ΓSpecIso (CommRingCat.of A)).inv.hom))
          (IsLocalRing.maximalIdeal A))) :
    _root_.IsReduced (Localization.AtPrime 𝔮.asIdeal ⧸
      (IsLocalRing.maximalIdeal A).map
        ((algebraMap R (Localization.AtPrime 𝔮.asIdeal)).comp (Spec.preimage (j ≫ toBase)).hom))

theorem

isReduced_of_openCover

L204 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.isReduced_pullback_residue_of_forall_isReduced_stalk_quotient.CFSGlue.isReduced_of_openCover

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isReduced_pullback_residue_of_forall_isReduced_stalk_quotient
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace CFSGlue
variable {A : Type u} [CommRing A] [IsLocalRing A]

Lean source · statement

theorem isReduced_of_openCover {P : Scheme.{u}} (𝒰 : P.OpenCover) (h : ∀ i, IsReduced (𝒰.X i)) :
    IsReduced P

theorem

isReduced_pullback_residue_of_forall_isReduced_stalk_quotient

L219 ↗

AlgebraicGeometry.isReduced_pullback_residue_of_forall_isReduced_stalk_quotient

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace isReduced_pullback_residue_of_forall_isReduced_stalk_quotient
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open CFSGlue in

Lean source · statement

theorem _root_.AlgebraicGeometry.isReduced_pullback_residue_of_forall_isReduced_stalk_quotient
    {A : Type u} [CommRing A] [IsLocalRing A]
    {X : Scheme.{u}} (toBase : X ⟶ Spec (CommRingCat.of A))
    (h : ∀ x : X, toBase.base x = IsLocalRing.closedPoint A →
      _root_.IsReduced (X.presheaf.stalk x ⧸
        Ideal.map ((X.presheaf.germ ⊤ x trivial).hom.comp
          (toBase.appTop.hom.comp (Scheme.ΓSpecIso (CommRingCat.of A)).inv.hom))
          (IsLocalRing.maximalIdeal A))) :
    IsReduced (pullback toBase (Spec.map (CommRingCat.ofHom (IsLocalRing.residue A))))

Module documentation

is Reduced pullback residue of forall is Reduced stalk quotient

Declarations

isReduced_quotient_map_of_forall_isReduced_localization

isReduced_of_ringEquiv

base_eq_closedPoint_iff

isReduced_pullback_affine

isReduced_localization_quotient_of_stalk

isReduced_of_openCover

isReduced_pullback_residue_of_forall_isReduced_stalk_quotient