AlgebraicCurve.exists_isRational_forall_mem_and_evalAt_eq_of_algHom
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_isRational_forall_mem_and_evalAt_eq_of_algHom
attribute [-instance]
AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve IsLocalRingLean source · statement
theorem _root_.AlgebraicCurve.exists_isRational_forall_mem_and_evalAt_eq_of_algHom
{L : Type*} [Field L] [IsAlgClosed L]
{F : Type*} [Field F] [Algebra L F] [IsCurveOver L F] [Algebra.EssFiniteType L F]
(B : Subalgebra L F) (χ : B →ₐ[L] L)
(hB : ∃ z : B, (z : F) ∉ Set.range (algebraMap L F)) :
∃ P : Place L F, P.IsRational ∧
∀ z : B, (z : F) ∈ P.toValuationSubring ∧ P.evalAt (z : F) = χ z