Module

PrincipalUnitRingTransport.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.PrincipalUnitRingTransport

2 declarations indexed from sourceView source ↗

Module documentation

Transport of principal-unit multipliers

Proves that the principal-unit multiplier condition is preserved, in both directions, by a local-ring equivalence intertwining the ring maps.

Imports3

Mathlib.RingTheory.LocalRing.RingHom.Basic
Mathlib.Algebra.Group.Units.Hom
Mathlib.Algebra.Ring.Equiv

Imported by2

theorem

principalUnitMultipliers_transport

L26 ↗

RamificationTheory.HilbertRamification.LocalRing.principalUnitMultipliers_transport

Documentation

Transport the actual principal-unit multiplier predicate using only the maximal ideals and the actual coefficient square; no residue field is opened.

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification.LocalRing
open IsLocalRing
universe u v

Lean source · statement

theorem principalUnitMultipliers_transport
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S]
    (e : R ≃+* S) (σ : R →+* R) (τ : S →+* S)
    (hcomm : e.toRingHom.comp σ = τ.comp e.toRingHom)
    (hσ : ∀ x : R, ∃ a : Rˣ, σ x = x * (a : R) ∧ (a : R) - 1 ∈ maximalIdeal R) :
    ∀ y : S, ∃ a : Sˣ, τ y = y * (a : S) ∧ (a : S) - 1 ∈ maximalIdeal S

theorem

principalUnitMultipliers_iff_of_ringEquiv

L49 ↗

RamificationTheory.HilbertRamification.LocalRing.principalUnitMultipliers_iff_of_ringEquiv