ModuleFractionFieldSubalgebraTrace.lean
Nyll.SchemeTheory.RingTheory.FractionFieldSubalgebraTrace
5 declarations indexed from sourceView source ↗ Module documentation
Traces after localizing a subalgebra of a fraction field
For any subalgebra B of the fraction field K of a domain R, the actual multiplication map K tensor B to K is an isomorphism. Flatness preserves the inclusion B to K, and each element of K is the image of k tensor 1. Consequently the trace of multiplication by b after base change is b itself. The result does not assume that R is integrally closed.
Imports4
- Mathlib.RingTheory.Localization.BaseChange
- Mathlib.RingTheory.Localization.FractionRing
- Mathlib.RingTheory.Flat.Localization
- Mathlib.RingTheory.Trace.Basic
Imported by2
Declarations
SchemeTheory.fractionFieldTensorSubalgebraHom
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped TensorProduct nonZeroDivisors
namespace SchemeTheory
universe u v
variable (R : Type u) [CommRing R]
variable (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K]
SchemeTheory.fractionFieldTensorSubalgebraHom_bijective
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped TensorProduct nonZeroDivisors
namespace SchemeTheory
universe u v
variable (R : Type u) [CommRing R]
variable (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K]
SchemeTheory.fractionFieldTensorSubalgebraEquiv
DocumentationMultiplication identifies the base change of any fraction-field subalgebra with that fraction field.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped TensorProduct nonZeroDivisors
namespace SchemeTheory
universe u v
variable (R : Type u) [CommRing R]
variable (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K]
SchemeTheory.fractionFieldTensorSubalgebraEquiv_tmul
DocumentationThe comparison is the actual multiplication map on pure tensors.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped TensorProduct nonZeroDivisors
namespace SchemeTheory
universe u v
variable (R : Type u) [CommRing R]
variable (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K]
SchemeTheory.trace_baseChange_lmul_subalgebra
DocumentationMultiplication by an element of a fraction-field subalgebra has that same element as its trace after base change to the fraction field.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped TensorProduct nonZeroDivisors
namespace SchemeTheory
universe u v
variable (R : Type u) [CommRing R]
variable (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K]