ModuleIntegralPurelyInseparableLocalTensor.lean
Nyll.SchemeTheory.RingTheory.IntegralPurelyInseparableLocalTensor
2 declarations indexed from sourceView source ↗ Module documentation
Locality after base change of an integral local extension
If an integral map of local rings induces a purely inseparable residue field extension, its tensor product with any local algebra is local. The proof constructs the map to the tensor product of the two residue fields. Every maximal quotient factors through that map, and purely inseparability gives uniqueness of the resulting prime of the residue tensor product.
This is the local tensor product step of Stacks Project, Tag 092Y, used in the forward implication of Tag 06DM. It neither assumes nor encodes the irreducibility of a strict henselization.
Imports5
- Mathlib.RingTheory.Ideal.GoingUp
- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
- Mathlib.RingTheory.LocalRing.ResidueField.Basic
- Mathlib.RingTheory.Spectrum.Prime.Homeomorph
- Mathlib.RingTheory.TensorProduct.Nontrivial
Imported by3
Declarations
SchemeTheory.isLocalHom_of_ker_eq_maximalIdeal
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped TensorProduct
open IsLocalRing
namespace SchemeTheory
universe u v w
SchemeTheory.isLocalRing_tensorProduct_of_integral_of_purelyInseparable_residue
DocumentationAn integral local extension with purely inseparable residue field remains local after tensoring with a local algebra over the original local ring.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped TensorProduct
open IsLocalRing
namespace SchemeTheory
universe u v w