Algebra instances

This file contains several Algebra and IsScalarTower instances related to extensions of a field with a valuation, as well as their unit balls.

Main Definitions

• ValuationSubring.algebra : Given an algebra between two field extensions L and E of a field K with a valuation, create an algebra between their two rings of integers.

Main Results

• integralClosure_algebraMap_injective : the unit ball of a field K with respect to a valuation injects into its integral closure in a field extension L of K.

instance ValuationSubring.instAlgebraSubtypeMemValuationSubringWithZeroMultiplicativeInt {K : Type u_1} [Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) (L : Type u_2) [Field L] [Algebra K L] : Algebra { x : K // x ∈ v.valuationSubring } L

Equations

• ValuationSubring.instAlgebraSubtypeMemValuationSubringWithZeroMultiplicativeInt v L = Algebra.ofSubring v.valuationSubring.toSubring

theorem ValuationSubring.algebraMap_injective {K : Type u_1} [Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) (L : Type u_2) [Field L] [Algebra K L] : Function.Injective ⇑(algebraMap { x : K // x ∈ v.valuationSubring } L)

theorem ValuationSubring.isIntegral_of_mem_ringOfIntegers {K : Type u_1} [Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) (L : Type u_2) [Field L] [Algebra K L] {x : L} (hx : x ∈ integralClosure { x : K // x ∈ v.valuationSubring } L) : IsIntegral { x : K // x ∈ v.valuationSubring } ⟨x, hx⟩

theorem ValuationSubring.isIntegral_of_mem_ringOfIntegers' {K : Type u_1} [Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) (L : Type u_2) [Field L] [Algebra K L] {x : { x : L // x ∈ integralClosure { x : K // x ∈ v.valuationSubring } L }} : IsIntegral { x : K // x ∈ v.valuationSubring } x

instance ValuationSubring.instIsScalarTowerSubtypeMemValuationSubringWithZeroMultiplicativeInt {K : Type u_1} [Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) (L : Type u_2) [Field L] [Algebra K L] (E : Type u_3) [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] : IsScalarTower { x : K // x ∈ v.valuationSubring } L E

Equations

• ⋯ = ⋯

instance ValuationSubring.algebra {K : Type u_1} [Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) (L : Type u_2) [Field L] [Algebra K L] (E : Type u_3) [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] : Algebra { x : L // x ∈ integralClosure { x : K // x ∈ v.valuationSubring } L } { x : E // x ∈ integralClosure { x : K // x ∈ v.valuationSubring } E }

Given an algebra between two field extensions L and E of a field K with a valuation v, create an algebra between their two rings of integers.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ValuationSubring.equiv {K : Type u_1} [Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) (L : Type u_2) [Field L] [Algebra K L] (R : Type u_3) [CommRing R] [Algebra { x : K // x ∈ v.valuationSubring } R] [Algebra R L] [IsScalarTower { x : K // x ∈ v.valuationSubring } R L] [IsIntegralClosure R { x : K // x ∈ v.valuationSubring } L] : { x : L // x ∈ integralClosure { x : K // x ∈ v.valuationSubring } L } ≃+* R

A ring equivalence between the integral closure of the valuation subring of K in L and a ring R satisfying isIntegralClosure R v.valuationSubring L.

Equations

• ValuationSubring.equiv v L R = (IsIntegralClosure.equiv { x : K // x ∈ v.valuationSubring } R L { x : L // x ∈ integralClosure { x : K // x ∈ v.valuationSubring } L }).symm.toRingEquiv

theorem ValuationSubring.integralClosure_algebraMap_injective {K : Type u_1} [Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) (L : Type u_2) [Field L] [Algebra K L] : Function.Injective ⇑(algebraMap { x : K // x ∈ v.valuationSubring } { x : L // x ∈ integralClosure { x : K // x ∈ v.valuationSubring } L })