TameAbhyankar.SGA1.primeLocalizationEquivValuation_field_square
The native prime-localization automorphism has the prescribed original field action. Equality is proved on actual B-coefficients and then extended through localization; no localized action comparison is an input.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace TameAbhyankar.SGA1
universe u vLean source · statement
theorem primeLocalizationEquivValuation_field_square
(B : Type u) (L : Type v) [CommRing B] [IsDedekindDomain B]
[Field L] [Algebra B L] [IsFractionRing B L]
(Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
(σ : B ≃+* B) (hσ : Q = Q.comap σ.toRingHom)
(ρ : L →+* L)
(hcoeff : ρ.comp (algebraMap B L) = (algebraMap B L).comp σ.toRingHom) :
((idealLocalizationValuationSubring B L Q hQ).subtype.comp
(primeLocalizationEquivValuation B L Q hQ).toRingHom).comp
(Localization.localRingEquiv Q Q σ hσ).toRingHom =
ρ.comp ((idealLocalizationValuationSubring B L Q hQ).subtype.comp
(primeLocalizationEquivValuation B L Q hQ).toRingHom)