NYLL
Module

exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation
9 declarations indexed from sourceView source ↗

Module documentation

exists fg subalgebra is Pullback of is Affine of locally Of Finite Presentation

Imports7
Imported by2

Declarations

abbrev

Idx

L44 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation.M1b3.Idx
Documentation

The finitely generated intermediate algebras containing the prescribed finite set and the base-ring image.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace M1b3
variable {A₀ R A : Type u} [CommRing A₀] [CommRing R] [CommRing A] [Algebra A₀ R] [Algebra R A]
  [Algebra A₀ A]
Lean source · statement
abbrev Idx (s : Finset A) : Type u
theorem

idx_directed

L47 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation.M1b3.idx_directed
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace M1b3
variable {A₀ R A : Type u} [CommRing A₀] [CommRing R] [CommRing A] [Algebra A₀ R] [Algebra R A]
  [Algebra A₀ A]
omit [Algebra A₀ R] in
Lean source · statement
theorem idx_directed (s : Finset A) (a b : Idx (A₀ := A₀) (R := R) s) : ∃ c : Idx (A₀ := A₀) (R :=
  R) s, a ≤ c ∧ b ≤ c
instance

(anonymous instance)

L53 ↗
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace M1b3
variable {A₀ R A : Type u} [CommRing A₀] [CommRing R] [CommRing A] [Algebra A₀ R] [Algebra R A]
  [Algebra A₀ A]
Lean source · statement
instance (s : Finset A) : IsDirected (Idx (A₀ := A₀) (R := R) s) (· ≤ ·)
instance

(anonymous instance)

L55 ↗
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace M1b3
variable {A₀ R A : Type u} [CommRing A₀] [CommRing R] [CommRing A] [Algebra A₀ R] [Algebra R A]
  [Algebra A₀ A]
Lean source · statement
instance (s : Finset A) : IsDirectedOrder (Idx (A₀ := A₀) (R := R) s)
def

stageMap

L58 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation.M1b3.stageMap
Documentation

The inclusion homomorphism between two finitely generated stages.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace M1b3
variable {A₀ R A : Type u} [CommRing A₀] [CommRing R] [CommRing A] [Algebra A₀ R] [Algebra R A]
  [Algebra A₀ A]
Lean source · statement
def stageMap (s : Finset A) (i j : Idx (A₀ := A₀) (R := R) s) (h : i ≤ j) : ↥i.1 →+* ↥j.1
instance

directedSystem

L61 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation.M1b3.directedSystem
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace M1b3
variable {A₀ R A : Type u} [CommRing A₀] [CommRing R] [CommRing A] [Algebra A₀ R] [Algebra R A]
  [Algebra A₀ A]
Lean source · full declaration
instance directedSystem (s : Finset A) :
    DirectedSystem (fun i : Idx (A₀ := A₀) (R := R) s => ↥i.1) (fun i j h => ⇑(stageMap s i j h))
      where
  map_self _ _ := rfl
  map_map _ _ _ _ _ _ := rfl
theorem

isDirectLimit

L68 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation.M1b3.isDirectLimit
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace M1b3
variable {A₀ R A : Type u} [CommRing A₀] [CommRing R] [CommRing A] [Algebra A₀ R] [Algebra R A]
  [Algebra A₀ A]
omit [Algebra A₀ R] in
Lean source · full declaration
theorem isDirectLimit (s : Finset A) [Nonempty (Idx (A₀ := A₀) (R := R) s)] :
    IsDirectLimit (fun (i j : Idx (A₀ := A₀) (R := R) s) h => ⇑(stageMap s i j h)) (fun i =>
      ⇑(algebraMap (↥i.1) A)) := by
  classical
  refine ⟨fun a => ?_, fun i j mi mj h => ?_, fun _ _ _ _ => rfl⟩
  · obtain ⟨i⟩ := (inferInstance : Nonempty (Idx (A₀ := A₀) (R := R) s))
    have hfg : (Algebra.adjoin A₀ ({a} : Set A)).FG :=
      by simpa using Subalgebra.fg_adjoin_finset (R := A₀) {a}
    refine ⟨⟨i.1 ⊔ Algebra.adjoin A₀ {a}, i.2.1.sup hfg, i.2.2.1.trans (SetLike.coe_subset_coe.mpr
      le_sup_left),
      i.2.2.2.trans (SetLike.coe_subset_coe.mpr le_sup_left)⟩, ⟨a, ?_⟩, rfl⟩
    exact (le_sup_right : Algebra.adjoin A₀ {a} ≤ i.1 ⊔ Algebra.adjoin A₀ {a})
      (Algebra.self_mem_adjoin_singleton A₀ a)
  · obtain ⟨k, hik, hjk⟩ := idx_directed s i j
    exact ⟨k, hik, hjk, Subtype.ext h⟩
theorem

m1_main

L105 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation.m1_main
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
open M1b3 in
Lean source · statement
theorem m1_main
    {A₀ R A : Type u} [CommRing A₀] [CommRing R] [CommRing A] [Algebra A₀ R] [Algebra R A] [Algebra
      A₀ A]
    [IsScalarTower A₀ R A] [Algebra.FiniteType A₀ R]
    {X : Scheme.{u}} [IsAffine X] (g : X ⟶ Spec (CommRingCat.of A)) [LocallyOfFinitePresentation g]
    (s : Finset A) :
    ∃ (T : Subalgebra A₀ A), T.FG ∧ (↑s : Set A) ⊆ T ∧ Set.range (algebraMap R A) ⊆ T ∧
      ∃ (X₀ : Scheme.{u}) (f₀ : X₀ ⟶ Spec (CommRingCat.of ↥T)) (π : X ⟶ X₀),
        IsAffine X₀ ∧ LocallyOfFinitePresentation f₀ ∧ QuasiCompact f₀ ∧ QuasiSeparated f₀ ∧
        IsPullback π g f₀ (Spec.map (CommRingCat.ofHom (algebraMap ↥T A)))
theorem

exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation

L207 ↗
AlgebraicGeometry.exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation
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 scoped TensorProduct
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation in
Lean source · statement
theorem exists_fg_subalgebra_isPullback_of_isAffine_of_locallyOfFinitePresentation
    {A₀ R A : Type u} [CommRing A₀] [CommRing R] [CommRing A] [Algebra A₀ R] [Algebra R A] [Algebra
      A₀ A]
    [IsScalarTower A₀ R A] [Algebra.FiniteType A₀ R]
    {X : Scheme.{u}} [IsAffine X] (g : X ⟶ Spec (CommRingCat.of A)) [LocallyOfFinitePresentation g]
    (s : Finset A) :
    ∃ (T : Subalgebra A₀ A), T.FG ∧ (↑s : Set A) ⊆ T ∧ Set.range (algebraMap R A) ⊆ T ∧
      ∃ (X₀ : Scheme.{u}) (f₀ : X₀ ⟶ Spec (CommRingCat.of ↥T)) (π : X ⟶ X₀),
        IsAffine X₀ ∧ LocallyOfFinitePresentation f₀ ∧ QuasiCompact f₀ ∧ QuasiSeparated f₀ ∧
        IsPullback π g f₀ (Spec.map (CommRingCat.ofHom (algebraMap ↥T A)))

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