AlgebraicCurve.Place.exists_integralClosureAt_of_ord_fiber_nonneg
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_integralClosureAt_of_ord_fiber_nonneg
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid AlgebraicCurve
AlgebraicCurve.PlaceLean source · statement
theorem _root_.AlgebraicCurve.Place.exists_integralClosureAt_of_ord_fiber_nonneg {K F F' : Type*}
[Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
[FiniteDimensional F F'] [Algebra.IsSeparable F F'] {v : Place K F} [HasPrincipalDivisors K F']
{f : F'} (hf : f ≠ 0)
(hord : ∀ w ∈ v.fiber F', 0 ≤ w.ord f) :
∃ c : integralClosureAt F' v, algebraMap (integralClosureAt F' v) F' c = f