AlgebraicCurve.Place.exists_comap_toValuationSubring_eq_of_ne_top_of_isAlgebraic
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_comap_toValuationSubring_eq_of_ne_top_of_isAlgebraic
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.exists_comap_toValuationSubring_eq_of_ne_top_of_isAlgebraic
{κ : Type*} [Field κ] {k : Type*} [Field k] {E : Type*} [Field E]
[Algebra κ k] [Algebra k E] [Algebra κ E] [IsScalarTower κ k E] [Algebra.IsAlgebraic k E]
(x : E) [FiniteDimensional ↥(IntermediateField.adjoin κ ({x} : Set E)) E]
(W : ValuationSubring k) (hW : W ≠ ⊤) (hκ : ∀ a : κ, algebraMap κ k a ∈ W) :
∃ w : AlgebraicCurve.Place κ E, w.toValuationSubring.comap (algebraMap k E) = W