Module

exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd

32 declarations indexed from sourceView source ↗

Module documentation

exists mem and smooth Of Relative Dimension one of smooth Of Relative Dimension pullback

snd

Imports33

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCechSectionsOf
Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Mathlib.AlgebraicGeometry.Morphisms.Affine
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Restrict
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
Mathlib.Algebra.Algebra.Equiv
Mathlib.RingTheory.TensorProduct.Basic
Mathlib.RingTheory.TensorProduct.Maps
Mathlib.RingTheory.Smooth.Basic
Mathlib.RingTheory.Smooth.Fiber
Mathlib.RingTheory.Smooth.StandardSmooth
Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Mathlib.RingTheory.Etale.Descent
Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Mathlib.RingTheory.RingHom.Smooth
Mathlib.RingTheory.RingHom.Flat
Mathlib.RingTheory.FinitePresentation
Mathlib.RingTheory.RingHom.StandardSmooth
Mathlib.RingTheory.RingHom.Locally
Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Mathlib.RingTheory.Ideal.Over
Mathlib.RingTheory.Localization.Ideal
Mathlib.RingTheory.Unramified.Basic
Mathlib.Tactic.Set
Mathlib.Tactic.Push
Batteries.Tactic.Init

Imported by2

abbrev

AlgebraicCurves.Geometry.Schemes.Proofs.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd.AlgebraicGeometry.Scheme.TwoAffineOpenCover.AffineBaseChange.specMap_algebraMap_eq

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (A : Type u) [CommRing A] [Algebra R A]
variable (U : X.Opens) (hU : IsAffineOpen U)

Lean source · full declaration

theorem specMap_algebraMap_eq :
    letI := algebraOfHom c U
    Spec.map (CommRingCat.ofHom (algebraMap R Γ(X, U))) = hU.fromSpec ≫ c := by
  let := algebraOfHom c U
  have halg : (algebraMap R Γ(X, U)) = ((Scheme.ΓSpecIso (.of R)).inv ≫ c.appLE ⊤ U le_top).hom :=
    rfl
  rw [halg, CommRingCat.ofHom_hom, Spec.map_comp, ← Scheme.isoSpec_Spec_inv, ←
    IsAffineOpen.fromSpec_top,
    IsAffineOpen.SpecMap_appLE_fromSpec c (isAffineOpen_top (Spec (.of R))) hU (le_top : U ≤ c ⁻¹ᵁ
      ⊤)]

def

pullbackAffineOpenIsoSpecTensor

L99 ↗

Documentation

Identify a base-changed affine open with the spectrum of its tensor-product ring.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (A : Type u) [CommRing A] [Algebra R A]
variable (U : X.Opens) (hU : IsAffineOpen U)

Lean source · full declaration

def pullbackAffineOpenIsoSpecTensor :
    letI := algebraOfHom c U
    ((fst c A) ⁻¹ᵁ U).toScheme ≅ Spec (.of (Γ(X, U) ⊗[R] A)) :=
  letI := algebraOfHom c U
  (pullbackRestrictIsoRestrict (fst c A) U).symm
    ≪≫ pullbackSymmetry _ _
    ≪≫ pullbackRightPullbackFstIso c (specMap R A) U.ι
    ≪≫ asIso (pullback.map (U.ι ≫ c) (specMap R A)
        (Spec.map (CommRingCat.ofHom (algebraMap R Γ(X, U)))) (specMap R A)
        hU.isoSpec.hom (𝟙 _) (𝟙 _)
        (by rw [Category.comp_id, specMap_algebraMap_eq c U hU,
          ← hU.isoSpec_inv_ι_assoc, Iso.hom_inv_id_assoc])
        (by rw [Category.id_comp, Category.comp_id]))
    ≪≫ pullbackSpecIso R Γ(X, U) A

def

sigma

L115 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd.AlgebraicGeometry.Scheme.TwoAffineOpenCover.AffineBaseChange.sigma

Documentation

The ring equivalence on sections induced by the affine tensor-product chart.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (A : Type u) [CommRing A] [Algebra R A]
variable (U : X.Opens) (hU : IsAffineOpen U)

Lean source · full declaration

def sigma :
    letI := algebraOfHom c U
    (Γ(X, U) ⊗[R] A) ≃+* Γ(XA c A, (fst c A) ⁻¹ᵁ U) :=
  letI := algebraOfHom c U
  ((Scheme.ΓSpecIso (.of (Γ(X, U) ⊗[R] A))).symm
    ≪≫ Scheme.Γ.mapIso (pullbackAffineOpenIsoSpecTensor c A U hU).op
    ≪≫ ((fst c A) ⁻¹ᵁ U).topIso).commRingCatIsoToRingEquiv

theorem

sigma_apply

L123 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd.AlgebraicGeometry.Scheme.TwoAffineOpenCover.AffineBaseChange.sigma_apply

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (A : Type u) [CommRing A] [Algebra R A]
variable (U : X.Opens) (hU : IsAffineOpen U)

Lean source · full declaration

theorem sigma_apply (x : letI := algebraOfHom c U; Γ(X, U) ⊗[R] A) :
    letI := algebraOfHom c U
    sigma c A U hU x = ((Scheme.ΓSpecIso (.of (Γ(X, U) ⊗[R] A))).inv
      ≫ (pullbackAffineOpenIsoSpecTensor c A U hU).hom.appTop ≫ ((fst c A) ⁻¹ᵁ U).topIso.hom).hom x
        :=
  rfl

theorem

iso_hom_comp_sndLeg

L130 ↗

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (A : Type u) [CommRing A] [Algebra R A]
variable (U : X.Opens) (hU : IsAffineOpen U)

Lean source · full declaration

theorem iso_hom_comp_sndLeg :
    letI := algebraOfHom c U
    ((fst c A) ⁻¹ᵁ U).ι ≫ snd c A
      = (pullbackAffineOpenIsoSpecTensor c A U hU).hom
        ≫ Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.includeRight : A →ₐ[R] Γ(X, U) ⊗[R]
          A)) := by
  let := algebraOfHom c U
  rw [pullbackAffineOpenIsoSpecTensor, ← pullbackSpecIso_inv_snd R Γ(X, U) A]
  simp only [Iso.trans_hom, Iso.symm_hom, asIso_hom, Category.assoc, Iso.hom_inv_id_assoc,
    pullback.lift_snd, Category.comp_id, pullbackRightPullbackFstIso_hom_snd,
    pullbackSymmetry_hom_comp_snd_assoc, pullbackRestrictIsoRestrict_inv_fst_assoc]

theorem

iso_hom_comp_fstLeg

L142 ↗

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (A : Type u) [CommRing A] [Algebra R A]
variable (U : X.Opens) (hU : IsAffineOpen U)

Lean source · full declaration

theorem iso_hom_comp_fstLeg :
    letI := algebraOfHom c U
    (pullbackAffineOpenIsoSpecTensor c A U hU).hom
        ≫ Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.includeLeftRingHom : Γ(X, U) →+* Γ(X,
          U) ⊗[R] A))
      = ((fst c A) ∣_ U) ≫ hU.isoSpec.hom := by
  let := algebraOfHom c U
  rw [pullbackAffineOpenIsoSpecTensor, ← pullbackSpecIso_inv_fst R Γ(X, U) A]
  simp only [Iso.trans_hom, Iso.symm_hom, asIso_hom, Category.assoc, Iso.hom_inv_id_assoc,
    pullback.lift_fst, pullbackRightPullbackFstIso_hom_fst_assoc,
      pullbackSymmetry_hom_comp_fst_assoc]
  rfl

theorem

opens_ι_appTop_topIso_hom

L155 ↗

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (A : Type u) [CommRing A] [Algebra R A]
variable (U : X.Opens) (hU : IsAffineOpen U)
omit [CommRing R] in

Lean source · statement

theorem opens_ι_appTop_topIso_hom {Y : Scheme.{u}} (V : Y.Opens) :
    V.ι.appTop ≫ V.topIso.hom = Y.presheaf.map (homOfLE (le_top : V ≤ ⊤)).op

theorem

topIso_morphismRestrict_appTop_topIso

L160 ↗

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (A : Type u) [CommRing A] [Algebra R A]
variable (U : X.Opens) (hU : IsAffineOpen U)
omit [CommRing R] in

Lean source · statement

theorem topIso_morphismRestrict_appTop_topIso {Y Z : Scheme.{u}} (g : Y ⟶ Z) (W : Z.Opens) :
    W.topIso.inv ≫ (g ∣_ W).appTop ≫ (g ⁻¹ᵁ W).topIso.hom = g.app W

theorem

sigma_tmul_one

L170 ↗

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (A : Type u) [CommRing A] [Algebra R A]
variable (U : X.Opens) (hU : IsAffineOpen U)

Lean source · full declaration

theorem sigma_tmul_one (s : Γ(X, U)) :
    letI := algebraOfHom c U
    sigma c A U hU (s ⊗ₜ[R] (1 : A)) = ((fst c A).app U).hom s := by
  let := algebraOfHom c U
  rw [sigma_apply]
  have hiL : s ⊗ₜ[R] (1 : A)
      = (CommRingCat.ofHom (Algebra.TensorProduct.includeLeftRingHom : Γ(X, U) →+* Γ(X, U) ⊗[R]
        A)).hom s := rfl
  rw [hiL, ← CommRingCat.comp_apply, ← Category.assoc, Scheme.ΓSpecIso_inv_naturality,
    Category.assoc,
    ← Category.assoc _ _ (((fst c A) ⁻¹ᵁ U).topIso.hom), ← Scheme.Hom.comp_appTop,
    iso_hom_comp_fstLeg c A U hU, Scheme.Hom.comp_appTop, IsAffineOpen.isoSpec_hom_appTop]
  have hΓ : (Scheme.ΓSpecIso (CommRingCat.of Γ(X, U))).inv ≫ (Scheme.ΓSpecIso Γ(X, U)).hom = 𝟙 _ :=
    Iso.inv_hom_id _
  simp only [← Category.assoc]
  rw [hΓ, Category.id_comp, Category.assoc, topIso_morphismRestrict_appTop_topIso]

theorem

sigma_one_tmul

L187 ↗

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (A : Type u) [CommRing A] [Algebra R A]
variable (U : X.Opens) (hU : IsAffineOpen U)

Lean source · full declaration

theorem sigma_one_tmul (a : A) :
    letI := algebraOfHom c U
    sigma c A U hU ((1 : Γ(X, U)) ⊗ₜ[R] a)
      = ((XA c A).presheaf.map (homOfLE (le_top : (fst c A) ⁻¹ᵁ U ≤ ⊤)).op).hom
          (((Scheme.ΓSpecIso (.of A)).inv ≫ (snd c A).appTop).hom a) := by
  let := algebraOfHom c U
  rw [sigma_apply]
  have hiR : (1 : Γ(X, U)) ⊗ₜ[R] a
      = (CommRingCat.ofHom (R := A) (S := Γ(X, U) ⊗[R] A)
          (Algebra.TensorProduct.includeRight : A →ₐ[R] Γ(X, U) ⊗[R] A)).hom a := rfl
  rw [hiR, ← CommRingCat.comp_apply, ← Category.assoc, Scheme.ΓSpecIso_inv_naturality,
    Category.assoc,
    ← Category.assoc _ _ (((fst c A) ⁻¹ᵁ U).topIso.hom), ← Scheme.Hom.comp_appTop,
    ← iso_hom_comp_sndLeg c A U hU, Scheme.Hom.comp_appTop, Category.assoc,
    opens_ι_appTop_topIso_hom ((fst c A) ⁻¹ᵁ U)]
  rfl

theorem

algebraMap_sndAlgebra

L204 ↗

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (A : Type u) [CommRing A] [Algebra R A]
variable (U : X.Opens) (hU : IsAffineOpen U)

Lean source · statement

theorem algebraMap_sndAlgebra (a : A) :
    (algebraOfHom (snd c A) ((fst c A) ⁻¹ᵁ U)).algebraMap a
      = ((XA c A).presheaf.map (homOfLE (le_top : (fst c A) ⁻¹ᵁ U ≤ ⊤)).op).hom
          (((Scheme.ΓSpecIso (.of A)).inv ≫ (snd c A).appTop).hom a)

def

algEquiv

L213 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd.AlgebraicGeometry.Scheme.TwoAffineOpenCover.AffineBaseChange.algEquiv

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (A : Type u) [CommRing A] [Algebra R A]
variable (U : X.Opens) (hU : IsAffineOpen U)

Lean source · full declaration

def algEquiv :
    letI := algebraOfHom c U; letI := algebraOfHom (snd c A) ((fst c A) ⁻¹ᵁ U)
    (A ⊗[R] Γ(X, U)) ≃ₐ[A] Γ(XA c A, (fst c A) ⁻¹ᵁ U) :=
  letI := algebraOfHom c U; letI := algebraOfHom (snd c A) ((fst c A) ⁻¹ᵁ U)
  AlgEquiv.ofRingEquiv (f := (Algebra.TensorProduct.comm R A Γ(X, U)).toRingEquiv.trans (sigma c A
    U hU))
    (fun a => by
      change sigma c A U hU ((Algebra.TensorProduct.comm R A Γ(X, U)) (algebraMap A (A ⊗[R] Γ(X,
        U)) a)) = _
      rw [Algebra.TensorProduct.algebraMap_apply, show algebraMap A A a = a from rfl,
        Algebra.TensorProduct.comm_tmul, sigma_one_tmul, algebraMap_sndAlgebra])

theorem

algEquiv_one_tmul

L225 ↗

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (A : Type u) [CommRing A] [Algebra R A]
variable (U : X.Opens) (hU : IsAffineOpen U)

Lean source · full declaration

theorem algEquiv_one_tmul (s : Γ(X, U)) :
    letI := algebraOfHom c U; letI := algebraOfHom (snd c A) ((fst c A) ⁻¹ᵁ U)
    algEquiv c A U hU ((1 : A) ⊗ₜ[R] s) = ((fst c A).app U).hom s := by
  let := algebraOfHom c U; let := algebraOfHom (snd c A) ((fst c A) ⁻¹ᵁ U)
  change sigma c A U hU ((Algebra.TensorProduct.comm R A Γ(X, U)) ((1 : A) ⊗ₜ[R] s)) = _
  rw [Algebra.TensorProduct.comm_tmul, sigma_tmul_one]

instance

(anonymous instance)

L251 ↗

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (k : Type u) [Field k] [Algebra R k]

Lean source · statement

instance : IsAffineHom (specMap R k)

instance

(anonymous instance)

L253 ↗

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (k : Type u) [Field k] [Algebra R k]

Lean source · statement

instance : IsAffineHom (fst c k)

theorem

isAffineOpen_preimage_fst

L259 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd.AlgebraicGeometry.SmoothFibre.isAffineOpen_preimage_fst

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (k : Type u) [Field k] [Algebra R k]

Lean source · statement

theorem isAffineOpen_preimage_fst (U : X.Opens) (hU : IsAffineOpen U) : IsAffineOpen ((fst c k) ⁻¹ᵁ
  U)

theorem

smooth_tensor_of_smooth_snd

L263 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd.AlgebraicGeometry.SmoothFibre.smooth_tensor_of_smooth_snd

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (k : Type u) [Field k] [Algebra R k]

Lean source · full declaration

theorem smooth_tensor_of_smooth_snd (U : X.Opens) (hU : IsAffineOpen U) (hsm : Smooth (snd c k)) :
    letI := algebraOfHom c U
    Algebra.Smooth k (k ⊗[R] Γ(X, U)) := by
  let := algebraOfHom c U
  let := algebraOfHom (snd c k) ((fst c k) ⁻¹ᵁ U)
  have h1 : (Scheme.Hom.appLE (snd c k) ⊤ ((fst c k) ⁻¹ᵁ U) le_top).hom.Smooth :=
    Smooth.smooth_appLE (snd c k) (isAffineOpen_top _) (isAffineOpen_preimage_fst c k U hU) le_top
  have h2 : ((Scheme.ΓSpecIso (.of k)).inv ≫ Scheme.Hom.appLE (snd c k) ⊤ ((fst c k) ⁻¹ᵁ U)
    le_top).hom.Smooth := by
    rw [CommRingCat.hom_comp]
    exact RingHom.Smooth.comp (RingHom.Smooth.of_bijective (Scheme.ΓSpecIso (.of
      k)).commRingCatIsoToRingEquiv.symm.bijective) h1
  have h3 : Algebra.Smooth k Γ(XA c k, (fst c k) ⁻¹ᵁ U) := h2
  exact Algebra.Smooth.of_equiv (algEquiv c k U hU).symm

theorem

isSmoothAt_of_smooth_tensorProduct_field

L283 ↗

Algebra.isSmoothAt_of_smooth_tensorProduct_field

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
open _root_.Algebra
open scoped Algebra in

Lean source · statement

theorem _root_.Algebra.isSmoothAt_of_smooth_tensorProduct_field
    {R S k : Type u} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S]
      [Algebra.FinitePresentation R S]
    [Field k] [Algebra R k] [Algebra.Smooth k (k ⊗[R] S)]
    (q : Ideal S) [q.IsPrime] (hq : q.under R = RingHom.ker (algebraMap R k)) : Algebra.IsSmoothAt
      R q

theorem

base_fst_asIdeal

L323 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd.AlgebraicGeometry.SmoothFibre.base_fst_asIdeal

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
open _root_.Algebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (k : Type u) [Field k] [Algebra R k]

Lean source · statement

theorem base_fst_asIdeal (z : ↥(XA c k)) :
    (c.base ((fst c k).base z)).asIdeal = RingHom.ker (algebraMap R k)

theorem

comap_ΓSpecIso_inv_primeIdealOf_top

L335 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd.AlgebraicGeometry.SmoothFibre.comap_ΓSpecIso_inv_primeIdealOf_top

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
open _root_.Algebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (k : Type u) [Field k] [Algebra R k]

Lean source · statement

theorem comap_ΓSpecIso_inv_primeIdealOf_top (p : ↥(Spec (CommRingCat.of R))) :
    Ideal.comap (Scheme.ΓSpecIso (.of R)).inv.hom ((isAffineOpen_top (Spec (.of R))).primeIdealOf
      ⟨p, trivial⟩).asIdeal =
      p.asIdeal

theorem

mem_smoothLocus_of_smooth_snd

L347 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd.AlgebraicGeometry.SmoothFibre.mem_smoothLocus_of_smooth_snd

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
open _root_.Algebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (k : Type u) [Field k] [Algebra R k]
variable [Flat c] [LocallyOfFinitePresentation c]

Lean source · statement

theorem mem_smoothLocus_of_smooth_snd (hsm : Smooth (snd c k)) (z : ↥(XA c k)) :
    (fst c k).base z ∈ c.smoothLocus

theorem

exists_mem_and_smooth_of_smooth_pullback_snd

L402 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd.AlgebraicGeometry.SmoothFibre.exists_mem_and_smooth_of_smooth_pullback_snd

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
open _root_.Algebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.AffineBaseChange

Lean source · statement

theorem exists_mem_and_smooth_of_smooth_pullback_snd
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    [Flat c] [LocallyOfFinitePresentation c]
    {k : Type u} [Field k] (x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    (hsm : Smooth (pullback.snd c x)) :
    ∀ y ∈ Set.range (pullback.fst c x).base, ∃ W : C.Opens, y ∈ W ∧ Smooth (W.ι ≫ c)

theorem

mem_smoothLocus_of_smooth_pullback_snd

L415 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd.AlgebraicGeometry.SmoothFibre.mem_smoothLocus_of_smooth_pullback_snd

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
open _root_.Algebra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.AffineBaseChange

Lean source · statement

theorem mem_smoothLocus_of_smooth_pullback_snd
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    [Flat c] [LocallyOfFinitePresentation c]
    {k : Type u} [Field k] (x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    (hsm : Smooth (pullback.snd c x)) :
    ∀ y ∈ Set.range (pullback.fst c x).base, y ∈ c.smoothLocus

theorem

exists_isStandardSmoothOfRelativeDimension

L432 ↗

Algebra.IsStandardSmooth.exists_isStandardSmoothOfRelativeDimension

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
open _root_.Algebra
open _root_.Algebra
open _root_.Algebra.IsStandardSmooth
open scoped Algebra Algebra.IsStandardSmooth in

Lean source · statement

theorem _root_.Algebra.IsStandardSmooth.exists_isStandardSmoothOfRelativeDimension
    (R A : Type u) [CommRing R] [CommRing A] [Algebra R A] [Algebra.IsStandardSmooth R A] :
    ∃ d : ℕ, Algebra.IsStandardSmoothOfRelativeDimension d R A

theorem

isStandardSmoothOfRelativeDimension_of_baseChange_localization

L439 ↗

Algebra.isStandardSmoothOfRelativeDimension_of_baseChange_localization

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
open _root_.Algebra
open _root_.Algebra
open _root_.Algebra.IsStandardSmooth
open scoped Algebra in

Lean source · statement

theorem _root_.Algebra.isStandardSmoothOfRelativeDimension_of_baseChange_localization
    {R A k : Type u} [CommRing R] [CommRing A] [Algebra R A] [Algebra.IsStandardSmooth R A]
    [Field k] [Algebra R k] (h : k ⊗[R] A) [Nontrivial (Localization.Away h)] (n : ℕ)
    [Algebra.IsStandardSmoothOfRelativeDimension n k (Localization.Away h)] :
    Algebra.IsStandardSmoothOfRelativeDimension n R A

theorem

isStandardSmoothOfRelativeDimension_of_baseChange_localization'

L462 ↗

Algebra.isStandardSmoothOfRelativeDimension_of_baseChange_localization'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
open _root_.Algebra
open _root_.Algebra
open _root_.Algebra.IsStandardSmooth
open scoped Algebra in

Lean source · statement

theorem _root_.Algebra.isStandardSmoothOfRelativeDimension_of_baseChange_localization'
    {R A k B : Type u} [CommRing R] [CommRing A] [Algebra R A] [Algebra.IsStandardSmooth R A]
    [Field k] [Algebra R k] [CommRing B] [Algebra k B] (e : k ⊗[R] A ≃ₐ[k] B) (h : B) [Nontrivial
      (Localization.Away h)]
    (n : ℕ) [Algebra.IsStandardSmoothOfRelativeDimension n k (Localization.Away h)] :
    Algebra.IsStandardSmoothOfRelativeDimension n R A

theorem

exists_mem_and_smoothOfRelativeDimension_one_of_snd

L500 ↗

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
open _root_.Algebra
open _root_.Algebra
open _root_.Algebra.IsStandardSmooth
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (k : Type u) [Field k] [Algebra R k]

Lean source · statement

theorem exists_mem_and_smoothOfRelativeDimension_one_of_snd [Flat c] [LocallyOfFinitePresentation c]
    (hsm : SmoothOfRelativeDimension 1 (snd c k)) (z : ↥(XA c k)) :
    ∃ W : X.Opens, (fst c k).base z ∈ W ∧ SmoothOfRelativeDimension 1 (W.ι ≫ c)

theorem

exists_mem_and_smoothOfRelativeDimension_one_of_pullback_snd

L612 ↗

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
open _root_.Algebra
open _root_.Algebra
open _root_.Algebra.IsStandardSmooth
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs
open exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.AffineBaseChange
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (.of R))
variable (k : Type u) [Field k] [Algebra R k]

Lean source · statement

theorem exists_mem_and_smoothOfRelativeDimension_one_of_pullback_snd
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    [Flat c] [LocallyOfFinitePresentation c]
    {k : Type u} [Field k] (x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    (hsm : SmoothOfRelativeDimension 1 (pullback.snd c x)) :
    ∀ y ∈ Set.range (pullback.fst c x).base, ∃ W : C.Opens, y ∈ W ∧ SmoothOfRelativeDimension 1
      (W.ι ≫ c)

theorem

exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd

L640 ↗

AlgebraicGeometry.exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicGeometry
universe u
open CategoryTheory CategoryTheory.Limits
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd in
open AlgebraicGeometry.SmoothFibre in

Lean source · statement

theorem exists_mem_and_smoothOfRelativeDimension_one_of_smoothOfRelativeDimension_pullback_snd
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    [Flat c] [LocallyOfFinitePresentation c]
    {k : Type u} [Field k] (x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    (hsm : SmoothOfRelativeDimension 1 (pullback.snd c x)) :
    ∀ y ∈ Set.range (pullback.fst c x).base, ∃ W : C.Opens, y ∈ W ∧ SmoothOfRelativeDimension 1
      (W.ι ≫ c)

Module documentation

exists mem and smooth Of Relative Dimension one of smooth Of Relative Dimension pullback

Declarations