Module

TensorFractionGeneration.lean

Nyll.AlgebraicCurves.Foundations.FieldTheory.TensorFractionGeneration

1 declaration indexed from sourceView source ↗

Module documentation

Generators of the fraction field of a scalar extension

The fraction field of a scalar-extended affine coordinate ring is generated by the new constants and the image of the old function field. This lemma uses the tensor-product description of the coordinate ring, rather than assuming generation of the function field.

Imports3

Mathlib.RingTheory.TensorProduct.Basic
Mathlib.RingTheory.Localization.FractionRing
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Imported by2

theorem

adjoin_range_eq_top_of_tensor_fraction

L26 ↗

IntermediateField.adjoin_range_eq_top_of_tensor_fraction

Documentation

An affine tensor-product presentation supplies the field-generation condition for constant extension.

Source context 2 commands

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

open scoped TensorProduct
namespace IntermediateField

Lean source · statement

theorem adjoin_range_eq_top_of_tensor_fraction
    {K K' F L A B : Type*}
    [Field K] [Field K'] [Field F] [Field L]
    [CommRing A] [CommRing B] [Algebra K K'] [Algebra K A]
    [Algebra K' B] [Algebra B L] [Algebra K' L] [IsScalarTower K' B L]
    [IsFractionRing B L]
    (e : K' ⊗[K] A ≃ₐ[K'] B)
    (a : A →+* F) (φ : F →+* L)
    (h : ∀ x : A, algebraMap B L (e (1 ⊗ₜ[K] x)) = φ (a x)) :
    IntermediateField.adjoin K' (Set.range φ) = ⊤

Module documentation

Generators of the fraction field of a scalar extension

Declarations

adjoin_range_eq_top_of_tensor_fraction