Module

JacobsonRigidity.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.JacobsonRigidity

1 declaration indexed from sourceView source ↗

Module documentation

Rigidity of unramified maps modulo the Jacobson radical

The separability element of an essentially finite type unramified algebra annihilates the difference between two algebra maps. If the maps agree modulo an ideal in the Jacobson radical, the image of that element is a unit, forcing the maps to agree. This gives uniqueness for the morphism lifting problem over a general henselian pair.

Imports3

Mathlib.RingTheory.Jacobson.Ideal
Mathlib.RingTheory.TensorProduct.Maps
Mathlib.RingTheory.Unramified.Finite

Imported by5

theorem

comp_injective_of_le_jacobson

L37 ↗

Algebra.FormallyUnramified.comp_injective_of_le_jacobson

Documentation

Maps out of an essentially finite type unramified algebra are determined by reduction modulo any ideal contained in the Jacobson radical.

Source context 5 commands

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

@[expose] public section
open scoped TensorProduct
universe u v w
namespace Algebra.FormallyUnramified
variable {R : Type u} {A : Type v} {B : Type w}
  [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]

Lean source · statement

theorem comp_injective_of_le_jacobson [FormallyUnramified R A] [EssFiniteType R A]
    (J : Ideal B) (hJ : J ≤ Ideal.jacobson ⊥) :
    Function.Injective
      ((Ideal.Quotient.mkₐ R J).comp : (A →ₐ[R] B) → A →ₐ[R] B ⧸ J)

Module documentation

Rigidity of unramified maps modulo the Jacobson radical

Declarations

comp_injective_of_le_jacobson