Module

Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField

33 declarations indexed from sourceView source ↗

Module documentation

Scheme Hom fiber Inclusion mem smooth Locus of mem smooth Locus fiber To Spec Residue

Field

Imports35

Lean.Elab.Command
Mathlib.AlgebraicGeometry.Fiber
Mathlib.AlgebraicGeometry.ResidueField
Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Smooth.Locus
Mathlib.Topology.Sets.Opens
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.Etale.Descent
Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Mathlib.RingTheory.RingHom.Smooth
Mathlib.RingTheory.RingHom.Flat
Mathlib.RingTheory.FinitePresentation
Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Mathlib.RingTheory.Ideal.Over
Mathlib.RingTheory.Unramified.Basic
Mathlib.Tactic.Set
Nyll.SchemeTheory.Cohomology.Cech.TwoAffineOpenCover
Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCechSectionsOf
Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_isSmoothAt_of_isSmoothAt_fiber

Imported by2

abbrev

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

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace 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

L135 ↗

Documentation

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

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace 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

L153 ↗

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

Documentation

The ring equivalence between the tensor-product ring and sections of the base-changed affine open.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace 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

L161 ↗

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

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace 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

L168 ↗

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace 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

L180 ↗

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace 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

L193 ↗

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace 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

L198 ↗

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace 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

L208 ↗

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace 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

L225 ↗

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace 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

L242 ↗

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace 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

L251 ↗

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

Documentation

The algebra equivalence identifying sections of the base-changed affine open with a tensor product.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace 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

L263 ↗

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace Scheme
namespace 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)

L306 ↗

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
open 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)

L308 ↗

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
open 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

L311 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
open 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

L315 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
open 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

L380 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField.Algebra.isSmoothAt_of_smooth_tensorProduct_field

Source context 7 commands

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

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

Lean source · statement

theorem 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

L439 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
open 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

L451 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
open 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

comap_algEquiv

L463 ↗

Algebra.IsSmoothAt.comap_algEquiv

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
open 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 _root_.Algebra.IsSmoothAt.comap_algEquiv {K A B : Type*} [CommRing K] [CommRing A]
  [CommRing B]
    [Algebra K A] [Algebra K B] (e : A ≃ₐ[K] B) (Q : Ideal B) [Q.IsPrime] [Algebra.IsSmoothAt K Q] :
    Algebra.IsSmoothAt K (Q.comap e.toRingHom)

theorem

of_algEquiv_of_comap_eq

L511 ↗

Algebra.IsSmoothAt.of_algEquiv_of_comap_eq

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
open 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 _root_.Algebra.IsSmoothAt.of_algEquiv_of_comap_eq {K A B : Type*} [CommRing K]
  [CommRing A] [CommRing B]
    [Algebra K A] [Algebra K B] (e : A ≃ₐ[K] B) (P : Ideal A) (Q : Ideal B) [P.IsPrime] [Q.IsPrime]
    (h : Q.comap e.toRingHom = P) [Algebra.IsSmoothAt K Q] : Algebra.IsSmoothAt K P

theorem

mem_smoothLocus_of_mem_smoothLocus_snd_residueField

L535 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField.AlgebraicGeometry.SmoothFibre.mem_smoothLocus_of_mem_smoothLocus_snd_residueField

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
open 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_mem_smoothLocus_snd_residueField (p : Ideal R) [p.IsPrime]
    (z : ↥(XA c p.ResidueField)) (hz : z ∈ (snd c p.ResidueField).smoothLocus) :
    (fst c p.ResidueField).base z ∈ c.smoothLocus

theorem

smoothLocus_comp_of_isOpenImmersion

L617 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField.AlgebraicGeometry.SmoothFibre.smoothLocus_comp_of_isOpenImmersion

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
open 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 smoothLocus_comp_of_isOpenImmersion {X' Y Z : Scheme.{u}} (f : X' ⟶ Y) (g : Y ⟶ Z)
    [LocallyOfFinitePresentation f] [LocallyOfFinitePresentation (f ≫ g)] [IsOpenImmersion g] :
    (f ≫ g).smoothLocus = f.smoothLocus

theorem

smoothLocus_congr

L629 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField.AlgebraicGeometry.SmoothFibre.smoothLocus_congr

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
open 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 smoothLocus_congr {X' Y : Scheme.{u}} {f g : X' ⟶ Y}
    [LocallyOfFinitePresentation f] [LocallyOfFinitePresentation g] (h : f = g) :
    f.smoothLocus = g.smoothLocus

theorem

H1_affine

L639 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField.AlgebraicGeometry.SmoothFibre.H1_affine

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace AlgebraicGeometry
namespace SmoothFibre
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
open 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 H1_affine {R : Type u} [CommRing R] {X : Scheme.{u}} (c : X ⟶ Spec (CommRingCat.of R))
    [LocallyOfFinitePresentation c] [Flat c] (y : ↥(Spec (CommRingCat.of R)))
    [LocallyOfFinitePresentation (c.fiberToSpecResidueField y)]
    (z : ↥(c.fiber y)) (hz : z ∈ (c.fiberToSpecResidueField y).smoothLocus) :
    (c.fiberι y).base z ∈ c.smoothLocus

theorem

smoothLocus_congr

L782 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField.AlgebraicGeometry.Scheme.Hom.smoothLocus_congr

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open scoped _root_.AlgebraicGeometry.Scheme in
open scoped _root_.AlgebraicGeometry.Scheme.Hom in

Lean source · statement

theorem Scheme.Hom.smoothLocus_congr {X Y : Scheme.{u}} {f g : X ⟶ Y} (h : f = g)
    [LocallyOfFinitePresentation f] [LocallyOfFinitePresentation g] : f.smoothLocus = g.smoothLocus

theorem

smoothLocus_comp_of_isOpenImmersion

L790 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField.AlgebraicGeometry.Scheme.Hom.smoothLocus_comp_of_isOpenImmersion

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open scoped _root_.AlgebraicGeometry.Scheme in
open scoped _root_.AlgebraicGeometry.Scheme.Hom in

Lean source · statement

theorem Scheme.Hom.smoothLocus_comp_of_isOpenImmersion {X Y Z : Scheme.{u}} (φ : X ⟶ Y) (e : Y ⟶ Z)
    [LocallyOfFinitePresentation φ] [IsOpenImmersion e] :
    (φ ≫ e).smoothLocus = φ.smoothLocus

theorem

fiberInclusion_mem_smoothLocus_general

L798 ↗

H1GenY.fiberInclusion_mem_smoothLocus_general

Source context 9 commands

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

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

Lean source · statement

theorem _root_.H1GenY.fiberInclusion_mem_smoothLocus_general
    {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f] (y : ↥Y)
    [LocallyOfFinitePresentation (f.fiberToSpecResidueField y)] (z : ↥(f.fiber y))
    (hz : z ∈ (f.fiberToSpecResidueField y).smoothLocus) :
    (f.fiberι y).base z ∈ f.smoothLocus

theorem

fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField

L902 ↗

AlgebraicGeometry.Scheme.Hom.fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicGeometry.Scheme.Hom
universe u
open CategoryTheory CategoryTheory.Limits
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open Scheme_Hom_fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField in

Lean source · statement

theorem fiberInclusion_mem_smoothLocus_of_mem_smoothLocus_fiberToSpecResidueField
    {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f] (y : ↥Y)
    [LocallyOfFinitePresentation (f.fiberToSpecResidueField y)] (z : ↥(f.fiber y))
    (hz : z ∈ (f.fiberToSpecResidueField y).smoothLocus) :
    (f.fiberι y).base z ∈ f.smoothLocus

Module documentation

Scheme Hom fiber Inclusion mem smooth Locus of mem smooth Locus fiber To Spec Residue

Declarations