instIsLocalHomValuationInteger — Mathlib

English

For any S with a valuation vS extending vR, the induced map between the integer subrings is a local homomorphism.

Русский

Для любого S с вальвацией vS, продолжающей vR, индуцированное отображение между целочисленными подкольцами является локальным гомоморфизмом.

LaTeX

$$$\\IsLocalHom\\bigl(\\operatorname{algebraMap}_{v_R^{\\mathrm{integer}}, v_S^{\\mathrm{integer}}}\\bigr)$$$

Lean4

@[instance]
theorem instIsLocalHomValuationInteger {S ΓS : Type*} [CommRing S] [LinearOrderedCommGroupWithZero ΓS] [Algebra R S]
    [IsLocalHom (algebraMap R S)] {vS : Valuation S ΓS} [vR.HasExtension vS] :
    IsLocalHom (algebraMap vR.integer vS.integer) where
  map_nonunit r
    hr := by
    apply (Valuation.integer.integers (v := vR)).isUnit_of_one
    · exact (isUnit_map_iff (algebraMap R S) _).mp (hr.map (algebraMap _ S))
    · apply(Valuation.integer.integers (v := vS)).one_of_isUnit at hr
      exact (val_map_eq_one_iff vR vS _).mp hr

Похожие утверждения