TameAbhyankar.SGA1.idealLocalization_exists_principal_valuation_action
Transport the actual native prime-localization action through its canonical valuation-ring equivalence. Both the target automorphism and its field square are constructed; no localized comparison is supplied.
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 idealLocalization_exists_principal_valuation_action
(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)
(hprincipal : ∀ x : Localization.AtPrime Q, ∃ a : (Localization.AtPrime Q)ˣ,
Localization.localRingEquiv Q Q σ hσ x = x * (a : Localization.AtPrime Q) ∧
(a : Localization.AtPrime Q) - 1 ∈ IsLocalRing.maximalIdeal (Localization.AtPrime Q)) :
∃ τ : idealLocalizationValuationSubring B L Q hQ ≃+*
idealLocalizationValuationSubring B L Q hQ,
(idealLocalizationValuationSubring B L Q hQ).subtype.comp τ.toRingHom =
ρ.comp (idealLocalizationValuationSubring B L Q hQ).subtype ∧
∀ x : idealLocalizationValuationSubring B L Q hQ,
∃ a : (idealLocalizationValuationSubring B L Q hQ)ˣ,
τ.toRingHom x = x * (a : idealLocalizationValuationSubring B L Q hQ) ∧
(a : idealLocalizationValuationSubring B L Q hQ) - 1 ∈
IsLocalRing.maximalIdeal (idealLocalizationValuationSubring B L Q hQ)