Module

FiniteCoefficientModel.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.FiniteCoefficientModel

1 declaration indexed from sourceView source ↗

Module documentation

Finite coefficient models of flat algebras

Finitely many monic equations over an arbitrary scalar extension use only finitely many coefficients. Flatness ensures that those equations already hold after adjoining their coefficients. In particular, this construction requires neither an integral scalar extension nor injective transition maps.

This is the coefficient-enlargement step in the finite étale object descent of Stacks Project, tags 0BTV and 01ZO. The monic polynomial restriction uses Mathlib's Polynomial.toSubring API.

Imports6

Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.FiniteType
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Mathlib.RingTheory.Polynomial.Subring
Mathlib.RingTheory.TensorProduct.Maps

Imported by2

theorem

exists_fg_subalgebra_finite_tensorProduct

L40 ↗

Algebra.FiniteEtale.exists_fg_subalgebra_finite_tensorProduct

Documentation

If a flat finite-type algebra becomes module-finite after an arbitrary scalar extension, it is already module-finite after extending scalars to one finitely generated subalgebra of that extension.

Source context 4 commands

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

@[expose] public section
open scoped TensorProduct
universe u v w
namespace Algebra.FiniteEtale

Lean source · statement

theorem exists_fg_subalgebra_finite_tensorProduct
    (R : Type u) (A : Type v) (B : Type w)
    [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B] [Module.Flat R B]
    [Algebra.FiniteType R B] [Module.Finite A (A ⊗[R] B)] :
    ∃ (T : Subalgebra R A), T.FG ∧ Module.Finite T (T ⊗[R] B)

Module documentation

Finite coefficient models of flat algebras

Declarations

exists_fg_subalgebra_finite_tensorProduct