Module

LocalizationLocalMap.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.LocalizationLocalMap

1 declaration indexed from sourceView source ↗

Module documentation

The local map into a localization at a prime above the maximal ideal

For a local ring R, localizing an R-algebra at a prime above the maximal ideal gives a local map from R. This uses the actual localization and lying-over data, without integrality or finiteness assumptions.

Imports2

Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Ideal.Over

Imported by2

theorem

localizationAtPrime_algebraMap_isLocalHom

L22 ↗

ValuationTheory.DiscreteValuationField.localizationAtPrime_algebraMap_isLocalHom

Documentation

The map from a local base ring into a localization at a prime above its maximal ideal reflects units. The algebra structures form the given tower.

Source context 1 command

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

namespace ValuationTheory.DiscreteValuationField

Lean source · statement

theorem localizationAtPrime_algebraMap_isLocalHom
    (R : Type*) {B : Type*} (A : Type*)
    [CommRing R] [CommRing B] [CommRing A] [IsLocalRing R]
    [Algebra R B] [Algebra B A] [Algebra R A] [IsScalarTower R B A]
    (P : Ideal B) [P.IsPrime] [P.LiesOver (IsLocalRing.maximalIdeal R)]
    [IsLocalization.AtPrime A P] :
    IsLocalHom (algebraMap R A)

Module documentation

The local map into a localization at a prime above the maximal ideal

Declarations

localizationAtPrime_algebraMap_isLocalHom