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 statements

• 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.

@[implicit_reducible]

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

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 (↥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 (↥v.valuationSubring) L) : IsIntegral ↥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 : ↥(integralClosure (↥v.valuationSubring) L)} : IsIntegral (↥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 (↥v.valuationSubring) L E

@[implicit_reducible]

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 ↥(integralClosure (↥v.valuationSubring) L) ↥(integralClosure (↥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.

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 (↥v.valuationSubring) R] [Algebra R L] [IsScalarTower (↥v.valuationSubring) R L] [IsIntegralClosure R (↥v.valuationSubring) L] : ↥(integralClosure (↥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.

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 ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L))