NYLL
Module

ComapResidueCharacteristic.lean

Nyll.ValuedFieldTheory.Valuation.ComapResidueCharacteristic
2 declarations indexed from sourceView source ↗

Module documentation

Residue characteristic under pullback of a valuation subring

A field embedding preserves the nonunit condition for the pulled-back valuation subring. Consequently equality of integer residues downstairs implies equality upstairs, so residue characteristic zero descends. No algebraicity, Henselianity, or rank assumption is used.

Imports2
Imported by6

Declarations

theorem

mem_nonunits_comap_iff

L27 ↗
ValuationSubring.mem_nonunits_comap_iff
Documentation

The actual field embedding preserves and reflects nonunits of a pulled-back valuation subring.

Source context 3 commands

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

namespace ValuationSubring
universe u v
variable {K : Type u} {L : Type v} [Field K] [Field L]
Lean source · statement
theorem mem_nonunits_comap_iff (A : ValuationSubring L) (f : K →+* L) (x : K) :
    x ∈ (A.comap f).nonunits ↔ f x ∈ A.nonunits
theorem

charZero_residueField_comap

L40 ↗
ValuationSubring.charZero_residueField_comap
Documentation

Residue characteristic zero descends along any field embedding by pulling back the specified valuation subring.

Source context 3 commands

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

namespace ValuationSubring
universe u v
variable {K : Type u} {L : Type v} [Field K] [Field L]
Lean source · statement
theorem charZero_residueField_comap (A : ValuationSubring L) (f : K →+* L)
    [CharZero (IsLocalRing.ResidueField A)] :
    CharZero (IsLocalRing.ResidueField (A.comap f))

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