NYLL
Module

FinitelyGeneratedModel.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.FinitelyGeneratedModel
1 declaration indexed from sourceView source ↗

Module documentation

Finite étale models over finitely generated coefficient subalgebras

An actual étale model is supplied by Mathlib's Noetherian descent theorem. Its coefficient ring is enlarged by the monic equations needed for module finiteness. Both properties therefore hold on the same model, with the original algebra recovered by the canonical tensor-product associativity equivalence. The ambient base ring is completely arbitrary.

This supplies the affine coefficient model used in Stacks Project, tag 0BTV.

Imports7
Imported by2

Declarations

theorem

exists_fg_subalgebra_model

L39 ↗
Algebra.FiniteEtale.exists_fg_subalgebra_model
Documentation

A finite étale algebra over any scalar extension has a finite étale model over an actual finitely generated coefficient subalgebra.

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_model
    (R : Type u) (A : Type v) (B : Type w)
    [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra A B] [Module.Finite A B] [Algebra.Etale A B] :
    ∃ (A₁ : Subalgebra R A) (B₁ : Type v) (_ : CommRing B₁) (_ : Algebra A₁ B₁),
      A₁.FG ∧ Module.Finite A₁ B₁ ∧ Algebra.Etale A₁ B₁ ∧
        Nonempty (B ≃ₐ[A] A ⊗[A₁] B₁)

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