Module

FractionFieldTensorDomain.lean

Nyll.SchemeTheory.RingTheory.FractionFieldTensorDomain

2 declarations indexed from sourceView source ↗

Module documentation

Tensor domains after passage to a fraction field

A flat algebra over an arbitrary base embeds in its tensor product with a faithful algebra. If that tensor product is a domain, localizing the original algebra to its fraction field preserves this property. Over the integers this also compares the integral and rational tensor products of fraction fields.

Imports4

Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.Localization.BaseChange
Mathlib.RingTheory.Localization.FractionRing
Mathlib.Algebra.Algebra.Rat

Imported by2

theorem

isDomain_of_isFractionRing_left_of_flat

L28 ↗

Algebra.TensorProduct.isDomain_of_isFractionRing_left_of_flat

Documentation

A domain tensor product remains a domain after localizing its flat left factor to a fraction field. Injectivity of the right structure map ensures that the denominators remain nonzero in the tensor product.

Source context 2 commands

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

open scoped TensorProduct
namespace Algebra.TensorProduct

Lean source · statement

theorem isDomain_of_isFractionRing_left_of_flat
    {R B F K : Type*} [CommRing R] [CommRing B] [IsDomain B] [Algebra R B]
    [CommRing F] [Algebra R F] [Algebra B F] [IsScalarTower R B F]
    [IsFractionRing B F] [CommRing K] [Algebra R K]
    [Module.Flat R B] [IsDomain (B ⊗[R] K)]
    (hK : Function.Injective (algebraMap R K)) :
    IsDomain (F ⊗[R] K)

theorem

isDomain_ratTensor_of_isFractionRing_intTensor

L65 ↗

Algebra.TensorProduct.isDomain_ratTensor_of_isFractionRing_intTensor