Module

Place_exists_restrictAlong_eq_of_finiteDimensional_fieldRange.lean

Nyll.AlgebraicCurves.Places.Place_exists_restrictAlong_eq_of_finiteDimensional_fieldRange

2 declarations indexed from sourceView source ↗

Module documentation

Place exists restrict Along eq of finite Dimensional field Range

Imports3

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

solution_impl

L32 ↗

AlgebraicCurves.Places.Proofs.Place_exists_restrictAlong_eq_of_finiteDimensional_fieldRange.AlgebraicCurve.Place.solution_impl

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_restrictAlong_eq_of_finiteDimensional_fieldRange
open scoped _root_.AlgebraicCurve _root_.AlgebraicCurve.Place in

Lean source · statement

theorem AlgebraicCurve.Place.solution_impl
    {K F F' : Type*} [Field K] [Field F] [Field F']
    [Algebra K F] [Algebra K F']
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    [FiniteDimensional φ.fieldRange F'] [Algebra.IsSeparable φ.fieldRange F']
    (v : AlgebraicCurve.Place K F) :
    ∃ w : AlgebraicCurve.Place K F', w.restrictAlong φ hφ = v

theorem

exists_restrictAlong_eq_of_finiteDimensional_fieldRange

L56 ↗

AlgebraicCurve.Place.exists_restrictAlong_eq_of_finiteDimensional_fieldRange

Source context 3 commands