NYLL
Module

PrimeRigidity.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.PrimeRigidity
2 declarations indexed from sourceView source ↗

Module documentation

Rigidity at a prime of an unramified domain

Maps out of an essentially finite type unramified algebra into a local ring are determined by congruence modulo its maximal ideal. Localizing a domain at a prime applies that criterion to endomorphisms agreeing modulo the prime. Injectivity of the actual localization map then proves equality in the original domain.

Imports4
Imported by2

Declarations

theorem

algHom_ext_of_sub_mem_maximalIdeal

L30 ↗
Algebra.FormallyUnramified.algHom_ext_of_sub_mem_maximalIdeal
Documentation

Maps from an unramified algebra into a local ring are determined by reduction modulo its maximal ideal. The Jacobson equality and the actual quotient-map comparison are proved in this local-ring owner.

Source context 3 commands

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

noncomputable section
namespace Algebra.FormallyUnramified
universe u v w
Lean source · statement
theorem algHom_ext_of_sub_mem_maximalIdeal
    {R : Type u} {A : Type v} {B : Type w}
    [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    [FormallyUnramified R A] [EssFiniteType R A] [IsLocalRing B]
    {f g : A →ₐ[R] B}
    (hfg : ∀ a : A, f a - g a ∈ IsLocalRing.maximalIdeal B) : f = g
theorem

algHom_ext_of_sub_mem_prime

L48 ↗
Algebra.FormallyUnramified.algHom_ext_of_sub_mem_prime
Documentation

An endomorphism of an unramified domain is determined by its reduction at any prime. No finiteness or normality condition on the base is needed.

Source context 3 commands

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

noncomputable section
namespace Algebra.FormallyUnramified
universe u v w
Lean source · statement
theorem algHom_ext_of_sub_mem_prime
    {R : Type u} {S : Type v}
    [CommRing R] [CommRing S] [Algebra R S] [IsDomain S]
    [FormallyUnramified R S] [EssFiniteType R S]
    (q : Ideal S) [q.IsPrime]
    {f g : S →ₐ[R] S} (hfg : ∀ a : S, f a - g a ∈ q) : f = g

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.