NYLL
Module

Smooth_exists_fg_subalgebra_of_smooth_pullback_snd.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
14 declarations indexed from sourceView source ↗

Module documentation

Smooth exists fg subalgebra of smooth pullback snd

Imports17
Imported by2

Declarations

abbrev

Stage

L53 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd.SmoothDescGC7.Stage
Documentation

The finitely generated stages containing an intermediate algebra and a prescribed finite subset.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace SmoothDescGC7
section Stages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
Lean source · statement
abbrev Stage (A₁ : Subalgebra A₀ A) (s : Finset A) : Type u
instance

isDirectedOrder

L60 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd.SmoothDescGC7.Stage.isDirectedOrder
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace SmoothDescGC7
section Stages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
namespace Stage
variable (A₁ : Subalgebra A₀ A) (s : Finset A)
Lean source · statement
instance isDirectedOrder : IsDirectedOrder (Stage A₁ s)
theorem

nonempty

L65 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd.SmoothDescGC7.Stage.nonempty
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace SmoothDescGC7
section Stages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
namespace Stage
variable (A₁ : Subalgebra A₀ A) (s : Finset A)
Lean source · statement
theorem nonempty (hA₁ : A₁.FG) : Nonempty (Stage A₁ s)
instance

algebra

L69 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd.SmoothDescGC7.Stage.algebra
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace SmoothDescGC7
section Stages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
namespace Stage
variable (A₁ : Subalgebra A₀ A) (s : Finset A)
Lean source · statement
instance algebra (i : Stage A₁ s) : Algebra A₁ i.1
instance

isScalarTower_top

L72 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd.SmoothDescGC7.Stage.isScalarTower_top
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace SmoothDescGC7
section Stages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
namespace Stage
variable (A₁ : Subalgebra A₀ A) (s : Finset A)
Lean source · statement
instance isScalarTower_top (i : Stage A₁ s) : IsScalarTower A₁ i.1 A
instance

isScalarTower_bot

L75 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd.SmoothDescGC7.Stage.isScalarTower_bot
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace SmoothDescGC7
section Stages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
namespace Stage
variable (A₁ : Subalgebra A₀ A) (s : Finset A)
Lean source · statement
instance isScalarTower_bot (i : Stage A₁ s) : IsScalarTower A₀ A₁ i.1
def

incl

L79 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd.SmoothDescGC7.Stage.incl
Documentation

The algebra inclusion between finitely generated stages over the fixed intermediate algebra.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace SmoothDescGC7
section Stages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
namespace Stage
variable (A₁ : Subalgebra A₀ A) (s : Finset A)
Lean source · statement
def incl (i j : Stage A₁ s) (h : i ≤ j) : i.1 →ₐ[A₁] j.1
theorem

incl_apply

L82 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd.SmoothDescGC7.Stage.incl_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace SmoothDescGC7
section Stages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
namespace Stage
variable (A₁ : Subalgebra A₀ A) (s : Finset A)
Lean source · statement
theorem incl_apply (i j : Stage A₁ s) (h : i ≤ j) (x : i.1) : (incl A₁ s i j h x :
  A) = x
instance

directedSystem

L85 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd.SmoothDescGC7.Stage.directedSystem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace SmoothDescGC7
section Stages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
namespace Stage
variable (A₁ : Subalgebra A₀ A) (s : Finset A)
Lean source · full declaration
instance directedSystem :
    DirectedSystem (fun i : Stage A₁ s => ↥i.1) (fun i j h => ⇑(incl A₁ s i j h)) where
  map_self := by intros; rfl
  map_map := by intros; rfl
theorem

isDirectLimit

L90 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd.SmoothDescGC7.Stage.isDirectLimit
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace SmoothDescGC7
section Stages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
namespace Stage
variable (A₁ : Subalgebra A₀ A) (s : Finset A)
Lean source · full declaration
theorem isDirectLimit (hA₁ : A₁.FG) :
    IsDirectLimit (fun i j h => ⇑(incl A₁ s i j h)) (fun i : Stage A₁ s => ⇑(algebraMap i.1 A))
      where
  surj := fun m => by
    classical
    let T : Subalgebra A₀ A := A₁ ⊔ Algebra.adjoin A₀ (↑(insert m s) : Set A)
    have hle : Algebra.adjoin A₀ (↑(insert m s) : Set A) ≤ T := le_sup_right
    have hT : T.FG ∧ A₁ ≤ T ∧ (↑s : Set A) ⊆ T :=
      ⟨hA₁.sup (Subalgebra.fg_adjoin_finset (insert m s)), le_sup_left,
        fun x hx => hle (Algebra.subset_adjoin (Finset.mem_coe.mpr (Finset.mem_insert_of_mem hx)))⟩
    have hm : m ∈ T := hle (Algebra.subset_adjoin (Finset.mem_coe.mpr (Finset.mem_insert_self m s)))
    exact ⟨⟨T, hT⟩, ⟨m, hm⟩, rfl⟩
  inj := fun i j mi mj h => by
    obtain ⟨k, hik, hjk⟩ := exists_ge_ge i j
    exact ⟨k, hik, hjk, Subtype.ext h⟩
  compatibility := fun _ _ _ _ => rfl
theorem

exists_fg_subalgebra_smooth_tensorProduct

L117 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd.SmoothDescGC7.exists_fg_subalgebra_smooth_tensorProduct
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace SmoothDescGC7
section Stages
variable {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
attribute [local instance] Stage.isDirectedOrder
attribute [local instance] Stage.algebra
attribute [local instance] Stage.isScalarTower_top
attribute [local instance] Stage.isScalarTower_bot
attribute [local simp] Stage.incl_apply
attribute [local instance] Stage.directedSystem
Lean source · statement
theorem exists_fg_subalgebra_smooth_tensorProduct
    {B₀ : Type u} [CommRing B₀] [Algebra A₀ B₀]
    [Algebra.FinitePresentation A₀ B₀] [Algebra.Smooth A (A ⊗[A₀] B₀)] (s : Finset A) :
    ∃ T : Subalgebra A₀ A, T.FG ∧ (↑s : Set A) ⊆ T ∧ Algebra.Smooth T (T ⊗[A₀] B₀)
theorem

smooth_pullback_snd_Spec_iff

L145 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd.SmoothDescGC7.smooth_pullback_snd_Spec_iff
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace SmoothDescGC7
attribute [local instance] Stage.isDirectedOrder
attribute [local instance] Stage.algebra
attribute [local instance] Stage.isScalarTower_top
attribute [local instance] Stage.isScalarTower_bot
attribute [local simp] Stage.incl_apply
attribute [local instance] Stage.directedSystem
Lean source · statement
theorem smooth_pullback_snd_Spec_iff {A₀ B R : Type u} [CommRing A₀] [CommRing B] [CommRing R]
    [Algebra A₀ B] [Algebra A₀ R] :
    Smooth (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap A₀ B)))
      (Spec.map (CommRingCat.ofHom (algebraMap A₀ R)))) ↔ Algebra.Smooth R (R ⊗[A₀] B)
theorem

smooth_tensor_of_le

L157 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd.SmoothDescGC7.smooth_tensor_of_le
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace SmoothDescGC7
attribute [local instance] Stage.isDirectedOrder
attribute [local instance] Stage.algebra
attribute [local instance] Stage.isScalarTower_top
attribute [local instance] Stage.isScalarTower_bot
attribute [local simp] Stage.incl_apply
attribute [local instance] Stage.directedSystem
Lean source · statement
theorem smooth_tensor_of_le {A₀ A B : Type u} [CommRing A₀] [CommRing A] [CommRing B]
    [Algebra A₀ A] [Algebra A₀ B] (T' T : Subalgebra A₀ A) (h : T' ≤ T)
    [Algebra.Smooth T' (T' ⊗[A₀] B)] : Algebra.Smooth T (T ⊗[A₀] B)
theorem

exists_fg_subalgebra_of_smooth_pullback_snd

L176 ↗
AlgebraicGeometry.Smooth.exists_fg_subalgebra_of_smooth_pullback_snd
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_fg_subalgebra_of_smooth_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
attribute [local instance] SmoothDescGC7.Stage.isDirectedOrder
attribute [local instance] SmoothDescGC7.Stage.algebra
attribute [local instance] SmoothDescGC7.Stage.isScalarTower_top
attribute [local instance] SmoothDescGC7.Stage.isScalarTower_bot
attribute [local simp] SmoothDescGC7.Stage.incl_apply
attribute [local instance] SmoothDescGC7.Stage.directedSystem
open SmoothDescGC7 in
Lean source · statement
theorem _root_.AlgebraicGeometry.Smooth.exists_fg_subalgebra_of_smooth_pullback_snd
    {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀)) [QuasiCompact f]
      [LocallyOfFinitePresentation f]
    [Smooth (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap A₀ A))))] (s : Finset A) :
    ∃ (T : Subalgebra A₀ A), T.FG ∧ (↑s : Set A) ⊆ T ∧
      Smooth (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T))))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.