LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogOfMixedChar_equivOfPreserves
The principal-unit logarithm commutes with the actual induced automorphism.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u
variable {K : Type u} [Field K] [CharZero K]Lean source · full declaration
theorem principalUnitLogOfMixedChar_equivOfPreserves
(v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
[ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
(p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
(f : K ≃+* K) (hval : ∀ x : K, v (f x) = v x)
(u : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1) :
(principalUnitLogOfMixedChar v p
(CompleteDVF.higherPrincipalUnitGroup.equivOfPreserves
(completeDVFOfWithZeroValuation v) f
(fun x => by change v x ≤ 1 ↔ v (f x) ≤ 1; rw [hval x]) 1 u)).toAdd =
f (principalUnitLogOfMixedChar v p u).toAdd := by
rw [principalUnitLogOfMixedChar_apply_toAdd, principalUnitLogOfMixedChar_apply_toAdd]
simp only [principalUnitLogSeriesOfWithZeroValuation]
rw [map_logOnePlusSeriesField_of_preserves v f hval]
congr 1
simp only [principalUnitSubOneOfWithZeroValuation,
CompleteDVF.higherPrincipalUnitGroup.equivOfPreserves_apply_coe,
_root_.map_sub, _root_.map_one]