Module

FlatTensorNilpotentKernel.lean

Nyll.SchemeTheory.RingTheory.FlatTensorNilpotentKernel

1 declaration indexed from sourceView source ↗

Module documentation

Flat base change of a ring map with nilpotent kernel elements

Exactness of tensoring with a flat algebra represents every element killed by base change using elements of the original kernel. Their images are nilpotent, so the resulting finite sum is nilpotent as well.

Imports2

Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.Nilpotent.Lemmas

Imported by2

theorem

ker_includeLeft_le_nilradical_of_flat

L28 ↗

SchemeTheory.ker_includeLeft_le_nilradical_of_flat

Documentation

Flat base change preserves the condition that every kernel element is nilpotent. No uniform nilpotence exponent is required.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace SchemeTheory
universe u v w

Lean source · statement

theorem ker_includeLeft_le_nilradical_of_flat
    (R : Type u) (N : Type v) (T : Type w)
    [CommRing R] [CommRing N] [CommRing T]
    [Algebra R N] [Algebra R T] [Module.Flat R T]
    (hker : RingHom.ker (algebraMap R N) ≤ nilradical R) :
    RingHom.ker (algebraMap T (T ⊗[R] N)) ≤ nilradical T

Module documentation

Flat base change of a ring map with nilpotent kernel elements

Declarations

ker_includeLeft_le_nilradical_of_flat