Module

Flat_exists_fg_subalgebra_of_flat_pullback_snd.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Flat_exists_fg_subalgebra_of_flat_pullback_snd

3 declarations indexed from sourceView source ↗

Module documentation

Descent of flatness to a finite stage.

Flatness on a finite affine cover descends to finitely generated subalgebras and is combined at a common stage.

Imports4

Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.Tactic.Choose
Nyll.SchemeTheory.RingTheory.Flat.FiniteSubalgebra

Imported by2

theorem

flat_pullback_snd_Spec_iff

L36 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Flat_exists_fg_subalgebra_of_flat_pullback_snd.FlatDesc21.flat_pullback_snd_Spec_iff

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Flat_exists_fg_subalgebra_of_flat_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace FlatDesc21

Lean source · statement

theorem flat_pullback_snd_Spec_iff {A₀ B R : Type u} [CommRing A₀] [CommRing B] [CommRing R]
    [Algebra A₀ B] [Algebra A₀ R] :
    Flat (pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap A₀ B))) (Spec.map (CommRingCat.ofHom
        (algebraMap A₀ R)))) ↔
      Module.Flat R (R ⊗[A₀] B)

theorem

flat_tensor_of_le

L50 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Flat_exists_fg_subalgebra_of_flat_pullback_snd.FlatDesc21.flat_tensor_of_le

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Flat_exists_fg_subalgebra_of_flat_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace FlatDesc21

Lean source · statement

theorem flat_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) [Module.Flat T' (T' ⊗[A₀] B)] : Module.Flat T (T ⊗[A₀]
        B)

theorem

exists_fg_subalgebra_of_flat_pullback_snd

L63 ↗

AlgebraicGeometry.Flat.exists_fg_subalgebra_of_flat_pullback_snd

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Flat_exists_fg_subalgebra_of_flat_pullback_snd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
open FlatDesc21 in

Lean source · statement

theorem _root_.AlgebraicGeometry.Flat.exists_fg_subalgebra_of_flat_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]
    [Flat (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap A₀ A))))] (s : Finset A) :
    ∃ (T : Subalgebra A₀ A), T.FG ∧ (↑s : Set A) ⊆ T ∧
      Flat (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T))))

Module documentation

Descent of flatness to a finite stage.

Declarations

flat_pullback_snd_Spec_iff

flat_tensor_of_le

exists_fg_subalgebra_of_flat_pullback_snd