Module

PrimeLocalizationInjection.lean

Nyll.SchemeTheory.RingTheory.Localization.PrimeLocalizationInjection

1 declaration indexed from sourceView source ↗

Module documentation

Injectivity of prime localization maps

Proves that an injective ring map into a domain induces an injective map on localizations at a prime and its contraction.

Imports2

Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Localization.Basic

Imported by2

theorem

localRingHom_injective

L23 ↗

SchemeTheory.localRingHom_injective

Documentation

An injective coefficient map into a domain remains injective after localization at a prime and its literal contraction.

Source context 2 commands

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

namespace SchemeTheory
universe u v

Lean source · statement

theorem localRingHom_injective
    {B : Type u} {C : Type v} [CommRing B] [CommRing C] [IsDomain C]
    (Q : Ideal B) (P : Ideal C) [Q.IsPrime] [P.IsPrime]
    (f : B →+* C) (hf : Q = P.comap f) (hinj : Function.Injective f.toFun) :
    Function.Injective (Localization.localRingHom Q P f hf).toFun

Module documentation

Injectivity of prime localization maps

Declarations

localRingHom_injective