Valuation extensions from valuative relations

Mathlib has two compatible notions of one valuation extending another. ValuativeExtension A B states the relation intrinsically, without choosing value groups, while Valuation.HasExtension vA vB states that the pullback of vB is equivalent to vA.

This file supplies the canonical bridge for the valuations attached to valuative relations. It allows Mathlib's valuation-extension API, including its algebra maps between valuation rings and residue fields, to be used directly from a ValuativeExtension hypothesis.

Main results

• TauCeti.ValuativeExtension.trans: compatibility of valuative relations in an algebra tower.
• ValuativeExtension.valuationHasExtension: the canonical valuation on B extends the canonical valuation on A.
• TauCeti.integerRingAlgebra: the induced algebra structure on the valuation rings.
• TauCeti.residueFieldAlgebra: the induced algebra structure on the residue fields.

instance ValuativeExtension.valuationHasExtension {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] : (ValuativeRel.valuation A).HasExtension (ValuativeRel.valuation B)

A compatible extension of valuative relations makes the canonical valuation on the larger ring an extension, in Mathlib's valuation-level sense, of the canonical valuation on the base.

theorem TauCeti.ValuativeExtension.trans (A : Type u_1) (B : Type u_2) (C : Type u_3) [CommSemiring A] [CommSemiring B] [Semiring C] [ValuativeRel A] [ValuativeRel B] [ValuativeRel C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] [ValuativeExtension A B] [ValuativeExtension B C] : ValuativeExtension A C

Compatibility of valuative relations composes along an algebra tower.

@[instance_reducible]

noncomputable instance TauCeti.integerRingAlgebra {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] : Algebra ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer

The structure map of a compatible extension restricts to its rings of integers.

Equations

• TauCeti.integerRingAlgebra = Valuation.HasExtension.instAlgebra_valuationSubring (ValuativeRel.valuation K) (ValuativeRel.valuation L)

@[instance_reducible]

noncomputable instance TauCeti.residueFieldAlgebra {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] : Algebra (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer)

The local map on rings of integers induces the residue-field extension.

Equations

• TauCeti.residueFieldAlgebra = IsLocalRing.ResidueField.instAlgebra

theorem TauCeti.coe_algebraMap_integerRing {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L] [ValuativeExtension K L] (x : ↥(ValuativeRel.valuation K).integer) : ↑((algebraMap ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer) x) = (algebraMap K L) ↑x

Coercing the integer-ring structure map to L gives the field structure map.