Module

FiniteSubalgebra.lean

Nyll.SchemeTheory.RingTheory.Flat.FiniteSubalgebra

27 declarations indexed from sourceView source ↗

Module documentation

Finite subalgebras with flat base change

Flatness descends to a finitely generated subalgebra containing any chosen finite set. The proof first treats the noetherian case and then descends a finite presentation model.

Imports4

Mathlib.RingTheory.Extension.Presentation.Basic
Mathlib.RingTheory.Extension.Presentation.Core
Nyll.SchemeTheory.RingTheory.Flat.OpenLocus
Nyll.SchemeTheory.RingTheory.Flat.FiniteSubalgebraLocalization

Imported by5

def

trans

L41 ↗

FlatDescentGlobal.trans

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section BCL
variable {R₀ E E' B₀ : Type*} [CommRing R₀] [CommRing E] [CommRing E'] [CommRing B₀]
  [Algebra R₀ E] [Algebra R₀ E'] [Algebra R₀ B₀] [Algebra E E'] [IsScalarTower R₀ E E']
variable (R₀ E E' B₀) in

Lean source · statement

def _root_.FlatDescentGlobal.trans : E ⊗[R₀] B₀ →ₐ[R₀] E' ⊗[R₀] B₀

lemma

trans_tmul

L47 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.trans_tmul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section BCL
variable {R₀ E E' B₀ : Type*} [CommRing R₀] [CommRing E] [CommRing E'] [CommRing B₀]
  [Algebra R₀ E] [Algebra R₀ E'] [Algebra R₀ B₀] [Algebra E E'] [IsScalarTower R₀ E E']
variable (R₀ E E' B₀) in

Lean source · statement

lemma trans_tmul (e : E) (b : B₀) :
    trans R₀ E E' B₀ (e ⊗ₜ b) = algebraMap E E' e ⊗ₜ b

lemma

trans_algebraMap

L51 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.trans_algebraMap

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section BCL
variable {R₀ E E' B₀ : Type*} [CommRing R₀] [CommRing E] [CommRing E'] [CommRing B₀]
  [Algebra R₀ E] [Algebra R₀ E'] [Algebra R₀ B₀] [Algebra E E'] [IsScalarTower R₀ E E']
variable (R₀ E E' B₀) in

Lean source · statement

lemma trans_algebraMap (e : E) :
    trans R₀ E E' B₀ (algebraMap E (E ⊗[R₀] B₀) e) =
      algebraMap E' (E' ⊗[R₀] B₀) (algebraMap E E' e)

theorem

flat_atPrime_baseChange

L57 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.flat_atPrime_baseChange

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section BCL
variable {R₀ E E' B₀ : Type*} [CommRing R₀] [CommRing E] [CommRing E'] [CommRing B₀]
  [Algebra R₀ E] [Algebra R₀ E'] [Algebra R₀ B₀] [Algebra E E'] [IsScalarTower R₀ E E']
variable (R₀ E E' B₀) in

Lean source · statement

theorem flat_atPrime_baseChange (Q' : Ideal (E' ⊗[R₀] B₀)) [Q'.IsPrime]
    (hflat : Module.Flat E (Localization.AtPrime (Q'.comap (trans R₀ E E' B₀).toRingHom))) :
    Module.Flat E' (Localization.AtPrime Q')

abbrev

lv

L146 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.lv

Documentation

The tensor-product map from a subalgebra stage to the ambient algebra.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

abbrev lv (E : Subalgebra R₀ R) : ↥E ⊗[R₀] B₀ →ₐ[R₀] R ⊗[R₀] B₀

abbrev

tr

L150 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.tr

Documentation

The transition map on tensor products induced by inclusion of subalgebras.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

abbrev tr {E E' : Subalgebra R₀ R} (h : E ≤ E') : ↥E ⊗[R₀] B₀ →ₐ[R₀] ↥E' ⊗[R₀] B₀

lemma

lv_comp_tr

L153 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.lv_comp_tr

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

lemma lv_comp_tr {E E' : Subalgebra R₀ R} (h : E ≤ E') :
    (lv (B₀ := B₀) E').comp (tr h) = lv E

lemma

lv_tr

L158 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.lv_tr

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

lemma lv_tr {E E' : Subalgebra R₀ R} (h : E ≤ E') (x : ↥E ⊗[R₀] B₀) :
    lv E' (tr h x) = lv E x

lemma

tr_comp_tr

L162 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.tr_comp_tr

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

lemma tr_comp_tr {E E' E'' : Subalgebra R₀ R} (h : E ≤ E') (h' : E' ≤ E'') :
    (tr (B₀ := B₀) h').comp (tr h) = tr (h.trans h')

lemma

tr_tr

L167 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.tr_tr

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

lemma tr_tr {E E' E'' : Subalgebra R₀ R} (h : E ≤ E') (h' : E' ≤ E'') (x : ↥E ⊗[R₀] B₀) :
    tr h' (tr h x) = tr (h.trans h') x

lemma

tr_refl

L171 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.tr_refl

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

lemma tr_refl (E : Subalgebra R₀ R) (x : ↥E ⊗[R₀] B₀) : tr (le_refl E) x = x

def

U

L178 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.U

Documentation

The primes of the tensor-product stage where the local ring is flat over E.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

def U (E : Subalgebra R₀ R) : Set (PrimeSpectrum (↥E ⊗[R₀] B₀))

def

V

L182 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.V

Documentation

The inverse image in the ambient tensor product of the flat locus at stage E.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

def V (E : Subalgebra R₀ R) : Set (PrimeSpectrum (R ⊗[R₀] B₀))

theorem

U_mono

L185 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.U_mono

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

theorem U_mono {E E' : Subalgebra R₀ R} (h : E ≤ E') (Q' : PrimeSpectrum (↥E' ⊗[R₀] B₀))
    (hQ : PrimeSpectrum.comap (tr h).toRingHom Q' ∈ U (B₀ := B₀) E) : Q' ∈ U E'

lemma

comap_lv_eq

L199 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.comap_lv_eq

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

lemma comap_lv_eq {E E' : Subalgebra R₀ R} (h : E ≤ E') (P : PrimeSpectrum (R ⊗[R₀] B₀)) :
    PrimeSpectrum.comap (tr (B₀ := B₀) h).toRingHom (PrimeSpectrum.comap (lv E').toRingHom P) =
      PrimeSpectrum.comap (lv E).toRingHom P

theorem

V_mono

L207 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.V_mono

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

theorem V_mono {E E' : Subalgebra R₀ R} (h : E ≤ E') : V (B₀ := B₀) E ⊆ V E'

theorem

exists_fg_mem_range_lv

L214 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.exists_fg_mem_range_lv

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

theorem exists_fg_mem_range_lv (b : R ⊗[R₀] B₀) :
    ∃ E : Subalgebra R₀ R, E.FG ∧ b ∈ Set.range (lv (B₀ := B₀) E)

lemma

lv_eq_rTensor

L228 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.lv_eq_rTensor

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

lemma lv_eq_rTensor (E : Subalgebra R₀ R) (x : ↥E ⊗[R₀] B₀) :
    lv E x = LinearMap.rTensor B₀ E.val.toLinearMap x

lemma

tr_eq_rTensor

L234 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.tr_eq_rTensor

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

lemma tr_eq_rTensor {E E' : Subalgebra R₀ R} (h : E ≤ E') (x : ↥E ⊗[R₀] B₀) :
    tr h x = LinearMap.rTensor B₀ (Subalgebra.inclusion h).toLinearMap x

theorem

exists_fg_tr_eq_zero

L240 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.exists_fg_tr_eq_zero

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Levels
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

theorem exists_fg_tr_eq_zero {E : Subalgebra R₀ R} (hE : E.FG) (x : ↥E ⊗[R₀] B₀)
    (hx : lv E x = 0) : ∃ E' : Subalgebra R₀ R, ∃ h : E ≤ E', E'.FG ∧ tr h x = 0

theorem

isOpen_V

L293 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.isOpen_V

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Noetherian
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

theorem isOpen_V [IsNoetherianRing R₀] [Algebra.FiniteType R₀ B₀] {E : Subalgebra R₀ R}
    (hE : E.FG) : IsOpen (V (B₀ := B₀) E)

theorem

exists_fg_mem_V

L300 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.exists_fg_mem_V

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Noetherian
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

theorem exists_fg_mem_V [IsNoetherianRing R₀] [Algebra.FiniteType R₀ B₀]
    [Module.Flat R (R ⊗[R₀] B₀)] (P : PrimeSpectrum (R ⊗[R₀] B₀)) :
    ∃ E : Subalgebra R₀ R, E.FG ∧ P ∈ V (B₀ := B₀) E

theorem

exists_fg_V_eq_univ

L314 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.exists_fg_V_eq_univ

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Noetherian
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

theorem exists_fg_V_eq_univ [IsNoetherianRing R₀] [Algebra.FiniteType R₀ B₀]
    [Module.Flat R (R ⊗[R₀] B₀)] (s : Finset R) :
    ∃ E : Subalgebra R₀ R, E.FG ∧ (↑s : Set R) ⊆ E ∧ V (B₀ := B₀) E = Set.univ

theorem

noetherian_case

L334 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.noetherian_case

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section Noetherian
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

theorem noetherian_case [IsNoetherianRing R₀] [Algebra.FiniteType R₀ B₀]
    [Module.Flat R (R ⊗[R₀] B₀)] (s : Finset R) :
    ∃ R₁ : Subalgebra R₀ R, R₁.FG ∧ (↑s : Set R) ⊆ R₁ ∧ Module.Flat R₁ (R₁ ⊗[R₀] B₀)

theorem

flat_iff_of_model

L411 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.flat_iff_of_model

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section General
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

theorem flat_iff_of_model {A₀ B₀₀ : Type*} [CommRing A₀] [CommRing B₀₀] [Algebra A₀ R₀]
    [Algebra A₀ B₀₀] (e₀ : R₀ ⊗[A₀] B₀₀ ≃ₐ[R₀] B₀)
    (T : Type*) [CommRing T] [Algebra R₀ T] [Algebra A₀ T] [IsScalarTower A₀ R₀ T] :
    Module.Flat T (T ⊗[R₀] B₀) ↔ Module.Flat T (T ⊗[A₀] B₀₀)

theorem

general_case

L420 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_Flat_exists_fg_subalgebra_flat_tensorProduct.FlatDescentGlobal.general_case

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
noncomputable section
namespace FlatDescentGlobal
section General
variable {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀] [Algebra R₀ R] [Algebra R₀ B₀]

Lean source · statement

theorem general_case [Algebra.FinitePresentation R₀ B₀] [Module.Flat R (R ⊗[R₀] B₀)]
    (s : Finset R) :
    ∃ R₁ : Subalgebra R₀ R, R₁.FG ∧ (↑s : Set R) ⊆ R₁ ∧ Module.Flat R₁ (R₁ ⊗[R₀] B₀)

theorem

exists_fg_subalgebra_flat_tensorProduct

L482 ↗

Module.Flat.exists_fg_subalgebra_flat_tensorProduct

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_Flat_exists_fg_subalgebra_flat_tensorProduct
open TensorProduct
attribute [local simp] trans_tmul

Lean source · statement

theorem _root_.Module.Flat.exists_fg_subalgebra_flat_tensorProduct
    {R₀ R B₀ : Type*} [CommRing R₀] [CommRing R] [CommRing B₀]
    [Algebra R₀ R] [Algebra R₀ B₀] [Algebra.FinitePresentation R₀ B₀]
    [Module.Flat R (R ⊗[R₀] B₀)] (s : Finset R) :
    ∃ R₁ : Subalgebra R₀ R, R₁.FG ∧ (↑s : Set R) ⊆ R₁ ∧ Module.Flat R₁ (R₁ ⊗[R₀] B₀)

Module documentation

Finite subalgebras with flat base change

Declarations