AlgebraicCurve.Place.restrictAlong_surjective
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_restrictAlong_surjective
open AlgebraicCurveLean source · full declaration
theorem _root_.AlgebraicCurve.Place.restrictAlong_surjective
{K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
(φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
(hfin : AlgebraicCurve.FiniteAlong K φ) (hsep : AlgebraicCurve.SeparableAlong K φ) :
Function.Surjective (fun w : AlgebraicCurve.Place K F' => w.restrictAlong φ hφ) := by
intro v
let := algebraAlong φ
have := isScalarTower_along φ
have : Module.Finite F F' := hfin
have : Algebra.IsSeparable F F' := hsep
obtain ⟨W, hW⟩ := AlgebraicCurve.Place.exists_restrict_eq (K := K) (F' := F) (M := F') v
exact ⟨W, hW⟩