IsAlgClosed.exists_valuationSubring_ringHom_retraction_forall_valuation_eq_one
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsAlgClosed_exists_valuationSubring_ringHom_retraction_forall_valuation_eq_oneLean source · statement
theorem _root_.IsAlgClosed.exists_valuationSubring_ringHom_retraction_forall_valuation_eq_one
(K E : Type*) [Field K] [Field E] [Algebra K E] [IsAlgClosed K]
(S : Finset E) (hS : (0 : E) ∉ S) :
∃ (A : ValuationSubring E) (hK : ∀ c : K, algebraMap K E c ∈ A) (σ : A →+* K),
RingHom.ker σ = IsLocalRing.maximalIdeal A ∧
(∀ c : K, σ ⟨algebraMap K E c, hK c⟩ = c) ∧
∀ s ∈ S, A.valuation s = 1