Shared library for isogeny endomorphism data

Common declarations from the dual-endomorphism and pointwise-addition proofs, together with the supporting helpers needed to make those declarations independent of either proof file. Also contains general coordinate-ring pullbacks, scalar-extension constructions for function fields, and compatibility of point maps with geometric morphisms.

theorem WeierstrassCurve.Affine.CoordinateRing.algebraMap_eq_mk_C_C {F : Type u_1} [Field F] {W : Affine F} (a : F) : (algebraMap F W.CoordinateRing) a = (mk W) (Polynomial.C (Polynomial.C a))

theorem WeierstrassCurve.Affine.CoordinateRing.eq_of_XYIdeal_eq {F : Type u_1} [Field F] {W : Affine F} {x₁ y₁ x₂ y₂ : F} (h₂ : W.Equation x₂ y₂) (h : XYIdeal W x₁ (Polynomial.C y₁) = XYIdeal W x₂ (Polynomial.C y₂)) : x₁ = x₂ ∧ y₁ = y₂

noncomputable def WeierstrassCurve.Affine.CoordinateRing.heightOneSpectrumOfEquation {F : Type u_1} [Field F] {W : Affine F} {x y : F} (h : W.Equation x y) : IsDedekindDomain.HeightOneSpectrum W.CoordinateRing

The height-one prime of the coordinate ring defined by a pair of coordinates satisfying the curve equation.

Equations

• WeierstrassCurve.Affine.CoordinateRing.heightOneSpectrumOfEquation h = { asIdeal := WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (Polynomial.C y), isPrime := ⋯, ne_bot := ⋯ }

theorem WeierstrassCurve.Affine.CoordinateRing.heightOneSpectrumOfEquation_asIdeal {F : Type u_1} [Field F] {W : Affine F} {x y : F} (h : W.Equation x y) : (heightOneSpectrumOfEquation h).asIdeal = XYIdeal W x (Polynomial.C y)

def WeierstrassCurve.Affine.IsFinitePlace {F : Type u_1} [Field F] {W : Affine F} (v : AlgebraicCurve.Place F W.FunctionField) : Prop

Every element of the affine coordinate ring is integral at the place.

Equations

• WeierstrassCurve.Affine.IsFinitePlace v = ∀ (r : W.CoordinateRing), (algebraMap W.CoordinateRing W.FunctionField) r ∈ v.toValuationSubring

noncomputable def WeierstrassCurve.Affine.IsFinitePlace.ringHom {F : Type u_1} [Field F] {W : Affine F} {v : AlgebraicCurve.Place F W.FunctionField} (hv : IsFinitePlace v) : W.CoordinateRing →+* ↥v.toValuationSubring

The coordinate-ring homomorphism into the valuation ring of a finite place.

Equations

• hv.ringHom = { toFun := fun (r : W.CoordinateRing) => ⟨(algebraMap W.CoordinateRing W.FunctionField) r, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem WeierstrassCurve.Affine.IsFinitePlace.coe_ringHom_apply {F : Type u_1} [Field F] {W : Affine F} {v : AlgebraicCurve.Place F W.FunctionField} (hv : IsFinitePlace v) (r : W.CoordinateRing) : ↑(hv.ringHom r) = (algebraMap W.CoordinateRing W.FunctionField) r

noncomputable def WeierstrassCurve.Affine.IsFinitePlace.centre {F : Type u_1} [Field F] {W : Affine F} {v : AlgebraicCurve.Place F W.FunctionField} (hv : IsFinitePlace v) : Ideal W.CoordinateRing

The prime ideal of the coordinate ring obtained by pulling back the maximal ideal of the finite place's valuation ring.

Equations

• hv.centre = Ideal.comap hv.ringHom (IsLocalRing.maximalIdeal ↥v.toValuationSubring)

theorem WeierstrassCurve.Affine.IsFinitePlace.centre_isPrime {F : Type u_1} [Field F] {W : Affine F} {v : AlgebraicCurve.Place F W.FunctionField} (hv : IsFinitePlace v) : hv.centre.IsPrime

theorem WeierstrassCurve.Affine.IsFinitePlace.inv_mem {F : Type u_1} [Field F] {W : Affine F} {v : AlgebraicCurve.Place F W.FunctionField} (hv : IsFinitePlace v) {r : W.CoordinateRing} (hr : r ∉ hv.centre) : ((algebraMap W.CoordinateRing W.FunctionField) r)⁻¹ ∈ v.toValuationSubring

theorem WeierstrassCurve.Affine.IsFinitePlace.centre_ne_bot {F : Type u_1} [Field F] {W : Affine F} {v : AlgebraicCurve.Place F W.FunctionField} (hv : IsFinitePlace v) : hv.centre ≠ ⊥

noncomputable def WeierstrassCurve.Affine.placeOfEquation {F : Type u_1} [Field F] {W : Affine F} [IsDedekindDomain W.CoordinateRing] {x y : F} (h : W.Equation x y) : AlgebraicCurve.Place F W.FunctionField

The function-field place associated to coordinates satisfying the affine curve equation.

Equations

• WeierstrassCurve.Affine.placeOfEquation h = AlgebraicCurve.Place.ofHeightOneSpectrum (WeierstrassCurve.Affine.CoordinateRing.heightOneSpectrumOfEquation h)

theorem WeierstrassCurve.Affine.isFinitePlace_placeOfEquation {F : Type u_1} [Field F] {W : Affine F} [IsDedekindDomain W.CoordinateRing] {x y : F} (h : W.Equation x y) : IsFinitePlace (placeOfEquation h)

theorem WeierstrassCurve.Affine.isFinitePlace_iff_exists_placeOfEquation {F : Type u_1} [Field F] {W : Affine F} [IsDedekindDomain W.CoordinateRing] [IsAlgClosed F] (v : AlgebraicCurve.Place F W.FunctionField) : IsFinitePlace v ↔ ∃ (x : F) (y : F) (h : W.Equation x y), v = placeOfEquation h

theorem WeierstrassCurve.Affine.S13_instIsDedekindDomainCoordinateRing {F : Type u_1} [Field F] {W : Affine F} [IsAlgClosed F] [WeierstrassCurve.IsElliptic W] : IsDedekindDomain W.CoordinateRing

theorem WeierstrassCurve.Affine.placeOfPoint_some {F : Type u_1} [Field F] {W : Affine F} [IsDedekindDomain W.CoordinateRing] [W.GenusOnePlaceGate] [GenusOnePlaceGate.IsCentred W] {x y : F} (h : W.Nonsingular x y) : placeOfPoint (Point.some x y h) = placeOfEquation ⋯

def WeierstrassCurve.Affine.InfinitePlace.place {F : Type u_1} [Field F] {W : Affine F} [W.GenusOnePlaceGate] : AlgebraicCurve.Place F W.FunctionField

The function-field place associated to the identity point at infinity.

Equations

• WeierstrassCurve.Affine.InfinitePlace.place = WeierstrassCurve.Affine.placeOfPoint 0

theorem WeierstrassCurve.Affine.InfinitePlace.not_isFinitePlace {F : Type u_1} [Field F] {W : Affine F} [W.GenusOnePlaceGate] [GenusOnePlaceGate.IsCentred W] [IsAlgClosed F] [WeierstrassCurve.IsElliptic W] : ¬IsFinitePlace place

theorem WeierstrassCurve.Affine.InfinitePlace.eq_of_not_isFinitePlace {F : Type u_1} [Field F] {W : Affine F} [IsDedekindDomain W.CoordinateRing] [W.GenusOnePlaceGate] [GenusOnePlaceGate.IsCentred W] (v : AlgebraicCurve.Place F W.FunctionField) (hv : ¬IsFinitePlace v) : v = place

theorem WeierstrassCurve.Affine.placeOfPoint_zero {F : Type u_1} [Field F] {W : Affine F} [W.GenusOnePlaceGate] : placeOfPoint Point.zero = InfinitePlace.place

theorem WeierstrassCurve.Affine.placeOfPoint_injective {F : Type u_1} [Field F] {W : Affine F} [W.GenusOnePlaceGate] : Function.Injective placeOfPoint

theorem WeierstrassCurve.Affine.placeOfPoint_surjective {F : Type u_1} [Field F] {W : Affine F} [W.GenusOnePlaceGate] (_hΔ : Δ W ≠ 0) : Function.Surjective placeOfPoint

theorem WeierstrassCurve.Affine.normFormulaAlong_of_elliptic {F : Type u_1} [Field F] [CharZero F] {V W : Affine F} (ι : V.FunctionField →ₐ[F] W.FunctionField) (hfin : AlgebraicCurve.FiniteAlong F ι) : AlgebraicCurve.NormFormulaAlong F ι hfin

theorem WeierstrassCurve.Affine.IsogenyEndDatum.normFormulaAlong_auto {F : Type u_1} [Field F] [CharZero F] {W : Affine F} (D : W.IsogenyEndDatum) : AlgebraicCurve.NormFormulaAlong F D.ι ⋯

noncomputable def WeierstrassCurve.Affine.IsogenyEndDatum.pointEnd' {F : Type u_1} [Field F] [DecidableEq F] [CharZero F] {W : Affine F} [W.GenusOnePlaceGate] [W.AbelTheorem] (D : W.IsogenyEndDatum) : AddMonoid.End W.Point

The point-group endomorphism induced by the isogeny datum, using its automatically supplied norm formula.

Equations

• D.pointEnd' = D.pointEnd ⋯

theorem WeierstrassCurve.Affine.IsogenyEndDatum.pointEnd'_apply {F : Type u_1} [Field F] [DecidableEq F] [CharZero F] {W : Affine F} [W.GenusOnePlaceGate] [W.AbelTheorem] (D : W.IsogenyEndDatum) (P : W.Point) : D.pointEnd' P = W.genusOnePic0Equiv ((AlgebraicCurve.Pic0.pushforwardAlongHom D.ι ⋯ ⋯ ⋯) (pointClass P))

theorem WeierstrassCurve.Affine.IsogenyEndDatum.pointEnd'_eq_of_seam {F : Type u_1} [Field F] [DecidableEq F] [CharZero F] {W : Affine F} [W.GenusOnePlaceGate] [W.AbelTheorem] (D : W.IsogenyEndDatum) (g : W.Point → W.Point) (hg0 : g 0 = 0) (hg : ∀ (P : W.Point), AlgebraicCurve.Place.restrictAlong D.ι ⋯ (placeOfPoint P) = placeOfPoint (g P)) (P : W.Point) : D.pointEnd' P = g P

theorem AlgebraicCurve.Place.evalAt_add {K : Type u_1} {F : Type u_2} [Field K] [Field F] [Algebra K F] (v : Place K F) (hv : v.IsRational) {f g : F} (hf : f ∈ v.toValuationSubring) (hg : g ∈ v.toValuationSubring) : v.evalAt (f + g) = v.evalAt f + v.evalAt g

theorem AlgebraicCurve.Place.evalAt_sub {K : Type u_1} {F : Type u_2} [Field K] [Field F] [Algebra K F] (v : Place K F) (hv : v.IsRational) {f g : F} (hf : f ∈ v.toValuationSubring) (hg : g ∈ v.toValuationSubring) : v.evalAt (f - g) = v.evalAt f - v.evalAt g

@[reducible, inline]

abbrev ModularCurve.KwIsogenyEndAddDatumSupply {F : Type u} [Field F] [DecidableEq F] [CharZero F] (W : WeierstrassCurve.Affine F) [W.GenusOnePlaceGate] [W.AbelTheorem] : Prop

Every nonzero sum of point endomorphisms arising from isogeny data is represented by another such datum.

Equations

• ModularCurve.KwIsogenyEndAddDatumSupply W = ∀ (D₁ D₂ : W.IsogenyEndDatum), D₁.pointEnd' + D₂.pointEnd' ≠ 0 → ∃ (D₃ : W.IsogenyEndDatum), D₃.pointEnd' = D₁.pointEnd' + D₂.pointEnd'

theorem WeierstrassCurve.Affine.Δ_ne_zero_of_isElliptic {F : Type u} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] : Δ W ≠ 0

def WeierstrassCurve.Affine.placeOfPointEquiv {F : Type u} [Field F] (W : Affine F) [W.GenusOnePlaceGate] : W.Point ≃ AlgebraicCurve.Place F W.FunctionField

The equivalence between elliptic-curve points and places of the function field.

Equations

• W.placeOfPointEquiv = WeierstrassCurve.Affine.pointEquivPlace

theorem WeierstrassCurve.Affine.placeOfPoint_placeOfPointEquiv_symm {F : Type u} [Field F] (W : Affine F) [W.GenusOnePlaceGate] (w : AlgebraicCurve.Place F W.FunctionField) : placeOfPoint (W.placeOfPointEquiv.symm w) = w

noncomputable def WeierstrassCurve.Affine.IsogenyEndDatum.geomMorph {F : Type u} [Field F] {W : Affine F} [W.GenusOnePlaceGate] (D : W.IsogenyEndDatum) : W.Point → W.Point

The point map obtained by restricting places along the function-field endomorphism and converting back to points.

Equations

• D.geomMorph P = W.placeOfPointEquiv.symm (AlgebraicCurve.Place.restrictAlong D.ι ⋯ (WeierstrassCurve.Affine.placeOfPoint P))

theorem WeierstrassCurve.Affine.IsogenyEndDatum.placeOfPoint_geomMorph {F : Type u} [Field F] {W : Affine F} [W.GenusOnePlaceGate] (D : W.IsogenyEndDatum) (P : W.Point) : AlgebraicCurve.Place.restrictAlong D.ι ⋯ (placeOfPoint P) = placeOfPoint (D.geomMorph P)

theorem AlgebraicCurve.Place.restrictAlong_comp {K : Type u_1} {F : Type u_2} [Field K] [Field F] [Algebra K F] (φ ψ : F →ₐ[K] F) (hφ : φ.IsIntegral) (hψ : ψ.IsIntegral) (hcomp : (ψ.comp φ).IsIntegral) (w : Place K F) : restrictAlong (ψ.comp φ) hcomp w = restrictAlong φ hφ (restrictAlong ψ hψ w)

theorem AlgebraicCurve.Place.isRational_of_deg_eq_one {K : Type u_1} {F : Type u_2} [Field K] [Field F] [Algebra K F] (v : Place K F) (h : v.deg = 1) : v.IsRational

theorem WeierstrassCurve.Affine.IsogenyEndDatum.pointEnd_eq_geomMorph_sub_geomMorph_zero {F : Type u} [Field F] [DecidableEq F] [CharZero F] {W : Affine F} [W.GenusOnePlaceGate] [W.AbelTheorem] (D : W.IsogenyEndDatum) (P : W.Point) : D.pointEnd' P = D.geomMorph P - D.geomMorph 0

theorem WeierstrassCurve.Affine.isFinitePlace_of_mem {F : Type u_1} [Field F] {W : Affine F} (v : AlgebraicCurve.Place F W.FunctionField) (hx : W.polyToFunctionField Polynomial.X ∈ v.toValuationSubring) : IsFinitePlace v

theorem WeierstrassCurve.Affine.ord_X_neg_of_not_isFinitePlace {F : Type u_1} [Field F] {W : Affine F} (v : AlgebraicCurve.Place F W.FunctionField) (hv : ¬IsFinitePlace v) : v.ord (W.polyToFunctionField Polynomial.X) < 0

@[reducible, inline]

abbrev ModularCurve.KwIsogenyEndAddGeomMorphSupply {F : Type u} [Field F] [DecidableEq F] [CharZero F] (W : WeierstrassCurve.Affine F) [W.GenusOnePlaceGate] [W.AbelTheorem] : Prop

Every nonzero sum of isogeny point endomorphisms is represented by a datum whose geometric point map is the pointwise sum.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicCurve.Place.mem_restrictAlong_iff {K : Type u_1} {F : Type u_2} {F' : Type u_3} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] (φ : F →ₐ[K] F') (hφ : φ.IsIntegral) (w : Place K F') (f : F) : f ∈ (restrictAlong φ hφ w).toValuationSubring ↔ φ f ∈ w.toValuationSubring

theorem AlgebraicCurve.Place.ramificationIndexAlong_pos {K : Type u_1} {F : Type u_2} {F' : Type u_3} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] (φ : F →ₐ[K] F') (hφ : φ.IsIntegral) (w : Place K F') : 0 < ramificationIndexAlong φ w

theorem AlgebraicCurve.Place.ord_restrictAlong_ne_zero_iff {K : Type u_1} {F : Type u_2} {F' : Type u_3} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] (φ : F →ₐ[K] F') (hφ : φ.IsIntegral) (w : Place K F') (f : F) : (restrictAlong φ hφ w).ord f ≠ 0 ↔ w.ord (φ f) ≠ 0

theorem WeierstrassCurve.Affine.algebraMap_polynomial_eq_mk_C {F : Type u_1} [Field F] {W : Affine F} (p : Polynomial F) : (algebraMap (Polynomial F) W.CoordinateRing) p = (CoordinateRing.mk W) (Polynomial.C p)

theorem WeierstrassCurve.Affine.algebraMap_coordinateRing_ne_zero {F : Type u_1} [Field F] {W : Affine F} {r : W.CoordinateRing} (hr : r ≠ 0) : (algebraMap W.CoordinateRing W.FunctionField) r ≠ 0

theorem WeierstrassCurve.Affine.ord_placeOfEquation_ne_zero_iff {F : Type u_1} [Field F] {W : Affine F} [IsDedekindDomain W.CoordinateRing] {x y : F} (h : W.Equation x y) {r : W.CoordinateRing} (hr : r ≠ 0) : (placeOfEquation h).ord ((algebraMap W.CoordinateRing W.FunctionField) r) ≠ 0 ↔ r ∈ CoordinateRing.XYIdeal W x (Polynomial.C y)

theorem WeierstrassCurve.Affine.ord_placeOfEquation_nonneg {F : Type u_1} [Field F] {W : Affine F} [IsDedekindDomain W.CoordinateRing] {x y : F} (h : W.Equation x y) (r : W.CoordinateRing) : 0 ≤ (placeOfEquation h).ord ((algebraMap W.CoordinateRing W.FunctionField) r)

theorem WeierstrassCurve.Affine.ord_placeOfEquation_pos_iff {F : Type u_1} [Field F] {W : Affine F} [IsDedekindDomain W.CoordinateRing] {x y : F} (h : W.Equation x y) {r : W.CoordinateRing} (hr : r ≠ 0) : 0 < (placeOfEquation h).ord ((algebraMap W.CoordinateRing W.FunctionField) r) ↔ r ∈ CoordinateRing.XYIdeal W x (Polynomial.C y)

theorem WeierstrassCurve.Affine.IsFinitePlace.mem_centre_iff_ord_ne_zero {F : Type u_1} [Field F] {W : Affine F} {v : AlgebraicCurve.Place F W.FunctionField} (hv : IsFinitePlace v) {r : W.CoordinateRing} (hr : r ≠ 0) : r ∈ hv.centre ↔ v.ord ((algebraMap W.CoordinateRing W.FunctionField) r) ≠ 0

theorem WeierstrassCurve.Affine.centre_placeOfEquation {F : Type u_1} [Field F] {W : Affine F} [IsDedekindDomain W.CoordinateRing] {x y : F} (h : W.Equation x y) : ⋯.centre = CoordinateRing.XYIdeal W x (Polynomial.C y)

theorem WeierstrassCurve.Affine.eq_placeOfEquation_of_le_centre {F : Type u_1} [Field F] {W : Affine F} [IsAlgClosed F] [IsDedekindDomain W.CoordinateRing] {v : AlgebraicCurve.Place F W.FunctionField} (hv : IsFinitePlace v) {x y : F} (h : W.Equation x y) (hle : CoordinateRing.XYIdeal W x (Polynomial.C y) ≤ hv.centre) : v = placeOfEquation h

noncomputable def WeierstrassCurve.Affine.yGen {F : Type u_1} [Field F] (W : Affine F) : W.FunctionField

The image of the affine y-coordinate in the function field.

Equations

• W.yGen = (algebraMap W.CoordinateRing W.FunctionField) ((WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X)

theorem WeierstrassCurve.Affine.ord_polyToFunctionField_pos_iff {F : Type u_1} [Field F] {W : Affine F} [IsDedekindDomain W.CoordinateRing] {x y : F} (h : W.Equation x y) {p : Polynomial F} (hp : p ≠ 0) : 0 < (placeOfEquation h).ord (W.polyToFunctionField p) ↔ Polynomial.eval x p = 0

theorem WeierstrassCurve.point_infinite {F : Type u} [Field F] [IsAlgClosed F] (W : WeierstrassCurve F) [W.IsElliptic] : Infinite W.toAffine.Point

theorem WeierstrassCurve.Affine.eval₂_polynomial_of_equation_map {F : Type u} [Field F] {W : Affine F} {xP yP : W.FunctionField} (h : (toAffine (W.map (algebraMap F W.FunctionField))).Equation xP yP) : Polynomial.eval₂ (Polynomial.aeval xP).toRingHom yP W.polynomial = 0

noncomputable def WeierstrassCurve.Affine.pointPullbackCoordHom {F : Type u} [Field F] {W : Affine F} {xP yP : W.FunctionField} (h : (toAffine (W.map (algebraMap F W.FunctionField))).Equation xP yP) : W.CoordinateRing →ₐ[F] W.FunctionField

Evaluate the affine coordinate ring at a function-field-valued point satisfying the curve equation.

Equations

• WeierstrassCurve.Affine.pointPullbackCoordHom h = { toRingHom := AdjoinRoot.lift (Polynomial.aeval xP).toRingHom yP ⋯, commutes' := ⋯ }

theorem WeierstrassCurve.Affine.pointPullbackCoordHom_injective {F : Type u} [Field F] {W : Affine F} {xP yP : W.FunctionField} (h : (toAffine (W.map (algebraMap F W.FunctionField))).Equation xP yP) (hx : Function.Injective ⇑(Polynomial.aeval xP)) : Function.Injective ⇑(pointPullbackCoordHom h)

noncomputable def WeierstrassCurve.Affine.pointPullbackHom {F : Type u} [Field F] {W : Affine F} {xP yP : W.FunctionField} (h : (toAffine (W.map (algebraMap F W.FunctionField))).Equation xP yP) (hx : Function.Injective ⇑(Polynomial.aeval xP)) : W.FunctionField →ₐ[F] W.FunctionField

Extend coordinate evaluation to a function-field endomorphism using the supplied transcendence of its x-coordinate.

Equations

• WeierstrassCurve.Affine.pointPullbackHom h hx = IsFractionRing.liftAlgHom ⋯

theorem WeierstrassCurve.Affine.polyToFunctionField_eq_aeval {F : Type u} [Field F] {W : Affine F} (p : Polynomial F) : W.polyToFunctionField p = (Polynomial.aeval (W.polyToFunctionField Polynomial.X)) p

theorem WeierstrassCurve.Affine.equation_map_polyToFunctionField_yGen {F : Type u} [Field F] {W : Affine F} : (toAffine (W.map (algebraMap F W.FunctionField))).Equation (W.polyToFunctionField Polynomial.X) W.yGen

theorem WeierstrassCurve.Affine.AbstractSeam.map_XClass {F : Type u} [Field F] {W V : Affine F} (ι : V.FunctionField →ₐ[F] W.FunctionField) {ξ : W.FunctionField} (hX : ι (V.polyToFunctionField Polynomial.X) = ξ) (c : F) : ι ((algebraMap V.CoordinateRing V.FunctionField) (CoordinateRing.XClass V c)) = ξ - (algebraMap F W.FunctionField) c

theorem WeierstrassCurve.Affine.AbstractSeam.map_YClass {F : Type u} [Field F] {W V : Affine F} (ι : V.FunctionField →ₐ[F] W.FunctionField) {η : W.FunctionField} (hY : ι V.yGen = η) (c : F) : ι ((algebraMap V.CoordinateRing V.FunctionField) (CoordinateRing.YClass V (Polynomial.C c))) = η - (algebraMap F W.FunctionField) c

theorem WeierstrassCurve.Affine.AbstractSeam.restrictAlong_placeOfEquation {F : Type u} [Field F] {W V : Affine F} (ι : V.FunctionField →ₐ[F] W.FunctionField) (hι : ι.IsIntegral) {ξ η : W.FunctionField} (hX : ι (V.polyToFunctionField Polynomial.X) = ξ) (hY : ι V.yGen = η) [IsDedekindDomain V.CoordinateRing] [IsAlgClosed F] [WeierstrassCurve.IsElliptic W] {x y : F} (h : W.Equation x y) {a b : F} (h' : V.Equation a b) (hreg : ξ ∈ (placeOfEquation h).toValuationSubring) (hdx : 0 < (placeOfEquation h).ord (ξ - (algebraMap F W.FunctionField) a)) (hdy : 0 < (placeOfEquation h).ord (η - (algebraMap F W.FunctionField) b)) : AlgebraicCurve.Place.restrictAlong ι hι (placeOfEquation h) = placeOfEquation h'

theorem WeierstrassCurve.Affine.AbstractSeam.restrictAlong_eq_infinitePlace {F : Type u} [Field F] {W V : Affine F} (ι : V.FunctionField →ₐ[F] W.FunctionField) (hι : ι.IsIntegral) {ξ : W.FunctionField} (hX : ι (V.polyToFunctionField Polynomial.X) = ξ) [IsDedekindDomain V.CoordinateRing] [V.GenusOnePlaceGate] [GenusOnePlaceGate.IsCentred V] (v : AlgebraicCurve.Place F W.FunctionField) (hpole : ξ ∉ v.toValuationSubring) : AlgebraicCurve.Place.restrictAlong ι hι v = InfinitePlace.place

theorem WeierstrassCurve.Affine.transcendental_polyToFunctionField_X {F : Type u} [Field F] {W : Affine F} : Transcendental F (W.polyToFunctionField Polynomial.X)

@[instance_reducible]

noncomputable def instDecEqFunctionFieldEndst20Ps {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} : DecidableEq W.FunctionField

Classical decidable equality on the affine curve's function field for the endomorphism arguments.

Equations

• instDecEqFunctionFieldEndst20Ps = Classical.decEq W.FunctionField

@[instance_reducible]

noncomputable def ModularCurve.Es1a1.instDecEqFunctionFieldEs1a6Add {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} : DecidableEq W.FunctionField

Classical decidable equality on the function field for addition of isogeny maps.

Equations

• ModularCurve.Es1a1.instDecEqFunctionFieldEs1a6Add = Classical.decEq W.FunctionField

theorem ModularCurve.Es1a1.es1a6_add_equation {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) (φ : W.FunctionField →ₐ[F] W.FunctionField) : (WeierstrassCurve.toAffine (W.map (algebraMap F W.FunctionField))).Equation (φ (W.polyToFunctionField Polynomial.X)) (φ W.yGen)

def ModularCurve.Es1a1.es1a6AddCollapse {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) (φ₁ φ₂ : W.FunctionField →ₐ[F] W.FunctionField) : Prop

The two function-field-valued points have equal x-coordinates and opposite y-coordinates in the curve's group law.

Equations

• One or more equations did not get rendered due to their size.

theorem ModularCurve.Es1a1.es1a6_add_not_collapse_of_X_ne {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) (φ₁ φ₂ : W.FunctionField →ₐ[F] W.FunctionField) (hne : φ₁ (W.polyToFunctionField Polynomial.X) ≠ φ₂ (W.polyToFunctionField Polynomial.X)) : ¬es1a6AddCollapse W φ₁ φ₂

noncomputable def ModularCurve.Es1a1.es1a6AddSumX {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) (φ₁ φ₂ : W.FunctionField →ₐ[F] W.FunctionField) : W.FunctionField

The rational x-coordinate obtained by adding the two function-field-valued points.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ModularCurve.Es1a1.es1a6AddSumY {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) (φ₁ φ₂ : W.FunctionField →ₐ[F] W.FunctionField) : W.FunctionField

The rational y-coordinate obtained by adding the two function-field-valued points.

Equations

• One or more equations did not get rendered due to their size.

theorem ModularCurve.Es1a1.es1a6_addSum_equation {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) (φ₁ φ₂ : W.FunctionField →ₐ[F] W.FunctionField) (hcol : ¬es1a6AddCollapse W φ₁ φ₂) : (WeierstrassCurve.toAffine (W.map (algebraMap F W.FunctionField))).Equation (es1a6AddSumX W φ₁ φ₂) (es1a6AddSumY W φ₁ φ₂)

noncomputable def ModularCurve.Es1a1.es1a6AddSumPullbackHom {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) (φ₁ φ₂ : W.FunctionField →ₐ[F] W.FunctionField) (hcol : ¬es1a6AddCollapse W φ₁ φ₂) (htr : Function.Injective ⇑(Polynomial.aeval (es1a6AddSumX W φ₁ φ₂))) : W.FunctionField →ₐ[F] W.FunctionField

The function-field map defined by the sum coordinates, using the noncollapse and transcendence hypotheses.

Equations

• ModularCurve.Es1a1.es1a6AddSumPullbackHom W φ₁ φ₂ hcol htr = WeierstrassCurve.Affine.pointPullbackHom ⋯ htr

theorem ModularCurve.Es1a1.es1a6_addSumPullbackHom_X {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) (φ₁ φ₂ : W.FunctionField →ₐ[F] W.FunctionField) (hcol : ¬es1a6AddCollapse W φ₁ φ₂) (htr : Function.Injective ⇑(Polynomial.aeval (es1a6AddSumX W φ₁ φ₂))) : (es1a6AddSumPullbackHom W φ₁ φ₂ hcol htr) (W.polyToFunctionField Polynomial.X) = es1a6AddSumX W φ₁ φ₂

theorem ModularCurve.Es1a1.es1a6_addSumPullbackHom_yGen {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) (φ₁ φ₂ : W.FunctionField →ₐ[F] W.FunctionField) (hcol : ¬es1a6AddCollapse W φ₁ φ₂) (htr : Function.Injective ⇑(Polynomial.aeval (es1a6AddSumX W φ₁ φ₂))) : (es1a6AddSumPullbackHom W φ₁ φ₂ hcol htr) W.yGen = es1a6AddSumY W φ₁ φ₂

theorem ModularCurve.Es1a1.es1a6_add_aeval_sumX_injective_of_forall_ne {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) (φ₁ φ₂ : W.FunctionField →ₐ[F] W.FunctionField) [IsAlgClosed F] (hnc : ∀ (c : F), es1a6AddSumX W φ₁ φ₂ ≠ (algebraMap F W.FunctionField) c) : Function.Injective ⇑(Polynomial.aeval (es1a6AddSumX W φ₁ φ₂))

@[instance_reducible]

noncomputable def ModularCurve.Es1a1.instDecEqFunctionFieldEs1a6AddSeam {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} : DecidableEq W.FunctionField

Classical decidable equality on the function field for identifying sum coordinates at places.

Equations

• ModularCurve.Es1a1.instDecEqFunctionFieldEs1a6AddSeam = Classical.decEq W.FunctionField

def ModularCurve.Es1a1.es1a6AddSumSeamDataAt {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} (φ₁ φ₂ : W.FunctionField →ₐ[F] W.FunctionField) (v : AlgebraicCurve.Place F W.FunctionField) : W.Point → Prop

The sum coordinates specialize to the specified point at the place, with a pole in the x-coordinate for the point at infinity.

Equations

• One or more equations did not get rendered due to their size.
• ModularCurve.Es1a1.es1a6AddSumSeamDataAt φ₁ φ₂ v WeierstrassCurve.Affine.Point.zero = (ModularCurve.Es1a1.es1a6AddSumX W φ₁ φ₂ ∉ v.toValuationSubring)

theorem ModularCurve.Es1a1.es1a6_addSumSeam_of_data {F : Type u} [Field F] [IsAlgClosed F] {W : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W] [W.GenusOnePlaceGate] [WeierstrassCurve.Affine.GenusOnePlaceGate.IsCentred W] (φ₁ φ₂ : W.FunctionField →ₐ[F] W.FunctionField) (hcol : ¬es1a6AddCollapse W φ₁ φ₂) (htr : Function.Injective ⇑(Polynomial.aeval (es1a6AddSumX W φ₁ φ₂))) (hι : (es1a6AddSumPullbackHom W φ₁ φ₂ hcol htr).IsIntegral) (P Q : W.Point) (hdat : es1a6AddSumSeamDataAt φ₁ φ₂ (WeierstrassCurve.Affine.placeOfPoint P) Q) : AlgebraicCurve.Place.restrictAlong (es1a6AddSumPullbackHom W φ₁ φ₂ hcol htr) hι (WeierstrassCurve.Affine.placeOfPoint P) = WeierstrassCurve.Affine.placeOfPoint Q

def ModularCurve.Es1a1.es1a11CoordSeamDataAt {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} (φ : W.FunctionField →ₐ[F] W.FunctionField) (v : AlgebraicCurve.Place F W.FunctionField) : W.Point → Prop

The coordinates of the function-field map specialize to the specified point, with a pole in the x-coordinate at infinity.

Equations

• One or more equations did not get rendered due to their size.
• ModularCurve.Es1a1.es1a11CoordSeamDataAt φ v WeierstrassCurve.Affine.Point.zero = (φ (W.polyToFunctionField Polynomial.X) ∉ v.toValuationSubring)

@[instance_reducible]

noncomputable def ModularCurve.Es1a1.instDecEqFunctionFieldEs1a10NcPole {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} : DecidableEq W.FunctionField

Classical decidable equality on the function field for the pole case of the nonconstant-coordinate argument.

Equations

• ModularCurve.Es1a1.instDecEqFunctionFieldEs1a10NcPole = Classical.decEq W.FunctionField

@[instance_reducible]

noncomputable def ModularCurve.Es1a1.instDecEqFunctionFieldEs1a10NcVertical {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} : DecidableEq W.FunctionField

Classical decidable equality on the function field for the vertical case of the nonconstant-coordinate argument.

Equations

• ModularCurve.Es1a1.instDecEqFunctionFieldEs1a10NcVertical = Classical.decEq W.FunctionField

@[instance_reducible]

noncomputable def ModularCurve.Es1a1.instDecEqFunctionFieldEs1a9Nc {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} : DecidableEq W.FunctionField

Classical decidable equality on the function field for the nonconstant sum-coordinate argument.

Equations

• ModularCurve.Es1a1.instDecEqFunctionFieldEs1a9Nc = Classical.decEq W.FunctionField

theorem ModularCurve.Mmr73.mmr73_cs_ord_neg {K : Type u_1} {F : Type u_2} [Field K] [Field F] [Algebra K F] (v : AlgebraicCurve.Place K F) (h : F) : v.ord (-h) = v.ord h

theorem ModularCurve.Mmr73.mmr73_cs_evalAt_eq_of_ord_sub_pos {K : Type u_1} {F : Type u_2} [Field K] [Field F] [Algebra K F] (v : AlgebraicCurve.Place K F) (hv : v.IsRational) {f : F} {a : K} (hf : f ∈ v.toValuationSubring) (hpos : 0 < v.ord (f - (algebraMap K F) a)) : v.evalAt f = a

theorem ModularCurve.Mmr73.mmr73_cs_iota_ne_zero {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} (D : W.IsogenyEndDatum) {f : W.FunctionField} (hf : f ≠ 0) : D.ι f ≠ 0

theorem ModularCurve.Mmr73.mmr73_cs_geomMorph_some_coords {F : Type u} [Field F] [IsAlgClosed F] {W : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W] [W.GenusOnePlaceGate] [WeierstrassCurve.Affine.GenusOnePlaceGate.IsCentred W] (D : W.IsogenyEndDatum) (Q : W.Point) {a b : F} {hab : W.Nonsingular a b} (hQ : D.geomMorph Q = WeierstrassCurve.Affine.Point.some a b hab) (hx : D.ι (W.polyToFunctionField Polynomial.X) ∈ (WeierstrassCurve.Affine.placeOfPoint Q).toValuationSubring) (hy : D.ι W.yGen ∈ (WeierstrassCurve.Affine.placeOfPoint Q).toValuationSubring) : (WeierstrassCurve.Affine.placeOfPoint Q).evalAt (D.ι (W.polyToFunctionField Polynomial.X)) = a ∧ (WeierstrassCurve.Affine.placeOfPoint Q).evalAt (D.ι W.yGen) = b

theorem ModularCurve.Es1a1.kw_coordSeamDataAt_geomMorph {F : Type u} [Field F] [IsAlgClosed F] {W : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W] [W.GenusOnePlaceGate] [WeierstrassCurve.Affine.GenusOnePlaceGate.IsCentred W] (D : W.IsogenyEndDatum) (P : W.Point) : es1a11CoordSeamDataAt D.ι (WeierstrassCurve.Affine.placeOfPoint P) (D.geomMorph P)

def ModularCurve.Es1a1.es1a8AddCollapseCmp {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) (φ₁ φ₂ : W.FunctionField →ₐ[F] W.FunctionField) : Prop

The coordinate criterion that the two function-field-valued points are negatives of each other.

Equations

• One or more equations did not get rendered due to their size.

theorem ModularCurve.Es1a1.es1a8_functionField_algHom_ext_cmp {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {φ ψ : W.FunctionField →ₐ[F] W.FunctionField} (hX : φ (W.polyToFunctionField Polynomial.X) = ψ (W.polyToFunctionField Polynomial.X)) (hY : φ W.yGen = ψ W.yGen) : φ = ψ

theorem ModularCurve.Es1a1.es1a8_addCollapse_pointEnd_add_eq_zero_cmp {F : Type u} [Field F] [DecidableEq F] [IsAlgClosed F] [CharZero F] {W : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W] [W.GenusOnePlaceGate] [WeierstrassCurve.Affine.GenusOnePlaceGate.IsCentred W] [W.AbelTheorem] (D₁ D₂ : W.IsogenyEndDatum) (hcol : es1a8AddCollapseCmp W D₁.ι D₂.ι) : D₁.pointEnd' + D₂.pointEnd' = 0

@[reducible, inline]

abbrev ModularCurve.Es1a1.kwHk5fAddSumXNonConstGuardAt {F : Type u} [Field F] [DecidableEq F] [CharZero F] (W : WeierstrassCurve.Affine F) [W.GenusOnePlaceGate] [W.AbelTheorem] : Prop

A nonzero sum of isogeny point endomorphisms has a rational sum x-coordinate unequal to every constant.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev ModularCurve.Es1a1.kwHk5fAddIntegralFiniteDataAt {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) : Prop

The function-field map defined by noncollapsed transcendental sum coordinates is integral and finite.

Equations

• One or more equations did not get rendered due to their size.

theorem ModularCurve.Es1a1.kw_hk5f_addIntegralFiniteDataAt_proved {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) : kwHk5fAddIntegralFiniteDataAt W

theorem ModularCurve.Es1a1.kw_hk5f_addSumCoordSeamDataNCAt_proved {F : Type u_1} [Field F] [DecidableEq F] [IsAlgClosed F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (φ₁ φ₂ : W.FunctionField →ₐ[F] W.FunctionField) : ¬es1a6AddCollapse W φ₁ φ₂ → (∀ (c : F), es1a6AddSumX W φ₁ φ₂ ≠ (algebraMap F W.FunctionField) c) → ∀ (v : AlgebraicCurve.Place F W.FunctionField) (Q₁ Q₂ : W.Point), es1a11CoordSeamDataAt φ₁ v Q₁ → es1a11CoordSeamDataAt φ₂ v Q₂ → es1a6AddSumSeamDataAt φ₁ φ₂ v (Q₁ + Q₂)

theorem ModularCurve.Es1a1.kw_hk5f_addSumXNonConstGuardAt_proved {F : Type u} [Field F] [DecidableEq F] [IsAlgClosed F] [CharZero F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [W.GenusOnePlaceGate] [WeierstrassCurve.Affine.GenusOnePlaceGate.IsCentred W] [W.AbelTheorem] : kwHk5fAddSumXNonConstGuardAt W

theorem ModularCurve.Es1a1.kw_hk5f_addGeomMorphSupply_proved {F : Type u} [Field F] [DecidableEq F] [IsAlgClosed F] [CharZero F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [W.GenusOnePlaceGate] [WeierstrassCurve.Affine.GenusOnePlaceGate.IsCentred W] [W.AbelTheorem] : KwIsogenyEndAddGeomMorphSupply W

theorem ModularCurve.Es1a1.kw_hk5f_addDatumSupply_proved {F : Type u} [Field F] [DecidableEq F] [IsAlgClosed F] [CharZero F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [W.GenusOnePlaceGate] [WeierstrassCurve.Affine.GenusOnePlaceGate.IsCentred W] [W.AbelTheorem] : KwIsogenyEndAddDatumSupply W

theorem WeierstrassCurve.Affine.CoordinateRing.exists_sub_algebraMap_mem {F : Type u_1} [Field F] {W : Affine F} {x y : F} (h : W.Equation x y) (r : W.CoordinateRing) : ∃ (c : F), r - (algebraMap F W.CoordinateRing) c ∈ XYIdeal W x (Polynomial.C y)

theorem WeierstrassCurve.nonempty_pointTorsionBy_zmod {K : Type u_1} [Field K] [DecidableEq K] [IsAlgClosed K] [CharZero K] (W : WeierstrassCurve K) [W.IsElliptic] {n : ℕ} (hn : 1 ≤ n) : Nonempty (↥(Submodule.torsionBy ℤ W.toAffine.Point ↑n) ≃+ (Fin 2 → ZMod n))

noncomputable def ModularCurve.kwCoordinateRingBasis {R : Type u_1} [CommRing R] (V : WeierstrassCurve.Affine R) : Module.Basis (ℕ × Fin 2) R V.CoordinateRing

The constant-ring basis of the affine coordinate ring consisting of powers of x, with and without a factor of y.

Equations

• ModularCurve.kwCoordinateRingBasis V = (Polynomial.basisMonomials R).smulTower (WeierstrassCurve.Affine.CoordinateRing.basis V)

theorem WeierstrassCurve.Affine.kw_functionField_algHom_ext {F : Type u_1} [Field F] {W : Affine F} {L : Type u_2} [Field L] [Algebra F L] {f g : W.FunctionField →ₐ[F] L} (hX : f (W.polyToFunctionField Polynomial.X) = g (W.polyToFunctionField Polynomial.X)) (hy : f W.yGen = g W.yGen) : f = g

theorem WeierstrassCurve.Affine.eval₂_polynomial_of_equation_map_target {F : Type u} [Field F] {W : Affine F} {L : Type v} [Field L] [Algebra F L] {xP yP : L} (h : (toAffine (W.map (algebraMap F L))).Equation xP yP) : Polynomial.eval₂ (Polynomial.aeval xP).toRingHom yP W.polynomial = 0

noncomputable def WeierstrassCurve.Affine.pointPullbackCoordHomTo {F : Type u} [Field F] {W : Affine F} {L : Type v} [Field L] [Algebra F L] {xP yP : L} (h : (toAffine (W.map (algebraMap F L))).Equation xP yP) : W.CoordinateRing →ₐ[F] L

Evaluate the affine coordinate ring at a point over the specified extension field.

Equations

• WeierstrassCurve.Affine.pointPullbackCoordHomTo h = { toRingHom := AdjoinRoot.lift (Polynomial.aeval xP).toRingHom yP ⋯, commutes' := ⋯ }

theorem WeierstrassCurve.Affine.pointPullbackCoordHomTo_mk {F : Type u} [Field F] {W : Affine F} {L : Type v} [Field L] [Algebra F L] {xP yP : L} (h : (toAffine (W.map (algebraMap F L))).Equation xP yP) (g : Polynomial (Polynomial F)) : (pointPullbackCoordHomTo h) ((CoordinateRing.mk W) g) = Polynomial.eval₂ (Polynomial.aeval xP).toRingHom yP g

theorem WeierstrassCurve.Affine.pointPullbackCoordHomTo_comp_algebraMap {F : Type u} [Field F] {W : Affine F} {L : Type v} [Field L] [Algebra F L] {xP yP : L} (h : (toAffine (W.map (algebraMap F L))).Equation xP yP) : (pointPullbackCoordHomTo h).comp (algebraMap (Polynomial F) W.CoordinateRing) = (Polynomial.aeval xP).toRingHom

theorem WeierstrassCurve.Affine.pointPullbackCoordHomTo_injective {F : Type u} [Field F] {W : Affine F} {L : Type v} [Field L] [Algebra F L] {xP yP : L} (h : (toAffine (W.map (algebraMap F L))).Equation xP yP) (hx : Function.Injective ⇑(Polynomial.aeval xP)) : Function.Injective ⇑(pointPullbackCoordHomTo h)

noncomputable def WeierstrassCurve.Affine.pointPullbackHomTo {F : Type u} [Field F] {W : Affine F} {L : Type v} [Field L] [Algebra F L] {xP yP : L} (h : (toAffine (W.map (algebraMap F L))).Equation xP yP) (hx : Function.Injective ⇑(Polynomial.aeval xP)) : W.FunctionField →ₐ[F] L

Extend coordinate evaluation to the function field when the specified x-coordinate is transcendental over the base.

Equations

• WeierstrassCurve.Affine.pointPullbackHomTo h hx = IsFractionRing.liftAlgHom ⋯

theorem WeierstrassCurve.Affine.pointPullbackHomTo_algebraMap {F : Type u} [Field F] {W : Affine F} {L : Type v} [Field L] [Algebra F L] {xP yP : L} (h : (toAffine (W.map (algebraMap F L))).Equation xP yP) (hx : Function.Injective ⇑(Polynomial.aeval xP)) (r : W.CoordinateRing) : (pointPullbackHomTo h hx) ((algebraMap W.CoordinateRing W.FunctionField) r) = (pointPullbackCoordHomTo h) r

theorem WeierstrassCurve.Affine.pointPullbackHomTo_polyToFunctionField_X {F : Type u} [Field F] {W : Affine F} {L : Type v} [Field L] [Algebra F L] {xP yP : L} (h : (toAffine (W.map (algebraMap F L))).Equation xP yP) (hx : Function.Injective ⇑(Polynomial.aeval xP)) : (pointPullbackHomTo h hx) (W.polyToFunctionField Polynomial.X) = xP

theorem WeierstrassCurve.Affine.pointPullbackHomTo_yGen {F : Type u} [Field F] {W : Affine F} {L : Type v} [Field L] [Algebra F L] {xP yP : L} (h : (toAffine (W.map (algebraMap F L))).Equation xP yP) (hx : Function.Injective ⇑(Polynomial.aeval xP)) : (pointPullbackHomTo h hx) W.yGen = yP

noncomputable def ModularCurve.kwFdn2QephodHend7GeomMorphBC {K : Type u_1} [Field K] {E E' : WeierstrassCurve.Affine K} [E.GenusOnePlaceGate] [E'.GenusOnePlaceGate] (ι : E'.FunctionField →ₐ[K] E.FunctionField) (hι : ι.IsIntegral) : E.Point → E'.Point

The contravariant point map obtained by restricting places along the specified integral function-field map.

Equations

• ModularCurve.kwFdn2QephodHend7GeomMorphBC ι hι P = E'.placeOfPointEquiv.symm (AlgebraicCurve.Place.restrictAlong ι hι (WeierstrassCurve.Affine.placeOfPoint P))

theorem ModularCurve.kw_fdn2_qephod_hend7_placeOfPoint_geomMorphBC {K : Type u_1} [Field K] {E E' : WeierstrassCurve.Affine K} [E.GenusOnePlaceGate] [E'.GenusOnePlaceGate] (ι : E'.FunctionField →ₐ[K] E.FunctionField) (hι : ι.IsIntegral) (P : E.Point) : AlgebraicCurve.Place.restrictAlong ι hι (WeierstrassCurve.Affine.placeOfPoint P) = WeierstrassCurve.Affine.placeOfPoint (kwFdn2QephodHend7GeomMorphBC ι hι P)

theorem ModularCurve.kw_fdn2_qephod_hend7_pushforwardDegZero_pointDivisor_geomMorphBC {K : Type u_1} [Field K] {E E' : WeierstrassCurve.Affine K} [E.GenusOnePlaceGate] [E'.GenusOnePlaceGate] (ι : E'.FunctionField →ₐ[K] E.FunctionField) (hι : ι.IsIntegral) (P : E.Point) : (AlgebraicCurve.Pic0.pushforwardAlongDegZero ι hι) (WeierstrassCurve.Affine.pointDivisor P) = WeierstrassCurve.Affine.pointDivisor (kwFdn2QephodHend7GeomMorphBC ι hι P) - WeierstrassCurve.Affine.pointDivisor (kwFdn2QephodHend7GeomMorphBC ι hι 0)

theorem ModularCurve.kw_fdn2_qephod_hend7_pushforwardHom_pointClass_eq_sub {K : Type u_1} [Field K] {E E' : WeierstrassCurve.Affine K} [E.GenusOnePlaceGate] [E'.GenusOnePlaceGate] (ι : E'.FunctionField →ₐ[K] E.FunctionField) (hι : ι.IsIntegral) (hfin : AlgebraicCurve.FiniteAlong K ι) (hN : AlgebraicCurve.NormFormulaAlong K ι hfin) (P : E.Point) : (AlgebraicCurve.Pic0.pushforwardAlongHom ι hι hfin hN) (WeierstrassCurve.Affine.pointClass P) = WeierstrassCurve.Affine.pointClass (kwFdn2QephodHend7GeomMorphBC ι hι P) - WeierstrassCurve.Affine.pointClass (kwFdn2QephodHend7GeomMorphBC ι hι 0)

theorem ModularCurve.kw_fdn2_qephod_hend7_pmop_eq_geomMorphBC_sub {K : Type u_1} [Field K] [DecidableEq K] {E E' : WeierstrassCurve.Affine K} [E.GenusOnePlaceGate] [E.AbelTheorem] [E'.GenusOnePlaceGate] [E'.AbelTheorem] (ι : E'.FunctionField →ₐ[K] E.FunctionField) (hι : ι.IsIntegral) (hfin : AlgebraicCurve.FiniteAlong K ι) (hN : AlgebraicCurve.NormFormulaAlong K ι hfin) (P : E.Point) : (WeierstrassCurve.Affine.pointMapOfPushforward ι hι hfin hN) P = kwFdn2QephodHend7GeomMorphBC ι hι P - kwFdn2QephodHend7GeomMorphBC ι hι 0

theorem ModularCurve.kw_transcendental_polyToFunctionField_X_over_baseGeneral {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] (F' : Type w) [Field F'] [Algebra R₀ F'] [Algebra F F'] : Transcendental F ((WeierstrassCurve.Affine.baseChange W F').polyToFunctionField Polynomial.X)

theorem ModularCurve.kw_equation_map_polyToFunctionField_yGen_over_baseGeneral {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra R₀ F'] [Algebra F F'] [IsScalarTower R₀ F F'] : (WeierstrassCurve.toAffine ((WeierstrassCurve.Affine.baseChange W F).map (algebraMap F (WeierstrassCurve.Affine.baseChange W F').FunctionField))).Equation ((WeierstrassCurve.Affine.baseChange W F').polyToFunctionField Polynomial.X) (WeierstrassCurve.Affine.baseChange W F').yGen

noncomputable def ModularCurve.kwFunctionFieldMapAlongGeneral {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra R₀ F'] [Algebra F F'] [IsScalarTower R₀ F F'] : (WeierstrassCurve.Affine.baseChange W F).FunctionField →ₐ[F] (WeierstrassCurve.Affine.baseChange W F').FunctionField

The function-field homomorphism induced by extending the coefficient field of the Weierstrass curve.

Equations

• ModularCurve.kwFunctionFieldMapAlongGeneral W F F' = WeierstrassCurve.Affine.pointPullbackHomTo ⋯ ⋯

theorem ModularCurve.kw_functionFieldMapAlongGeneral_polyToFunctionField_X {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra R₀ F'] [Algebra F F'] [IsScalarTower R₀ F F'] : (kwFunctionFieldMapAlongGeneral W F F') ((WeierstrassCurve.Affine.baseChange W F).polyToFunctionField Polynomial.X) = (WeierstrassCurve.Affine.baseChange W F').polyToFunctionField Polynomial.X

theorem ModularCurve.kw_functionFieldMapAlongGeneral_yGen {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra R₀ F'] [Algebra F F'] [IsScalarTower R₀ F F'] : (kwFunctionFieldMapAlongGeneral W F F') (WeierstrassCurve.Affine.baseChange W F).yGen = (WeierstrassCurve.Affine.baseChange W F').yGen

def ModularCurve.KwFunctionFieldTensorIsDomainGeneral {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra F F'] : Prop

The tensor product of the curve's function field with the larger coefficient field is an integral domain.

Equations

• ModularCurve.KwFunctionFieldTensorIsDomainGeneral W F F' = IsDomain (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F')

theorem ModularCurve.kw_isScalarTower_base_right_tensorGeneral {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra R₀ F'] [Algebra F F'] [IsScalarTower R₀ F F'] : IsScalarTower R₀ F' (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F')

theorem ModularCurve.kw_isScalarTower_base_right_fracTensorGeneral {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra R₀ F'] [Algebra F F'] [IsScalarTower R₀ F F'] : IsScalarTower R₀ F' (FractionRing (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F'))

theorem ModularCurve.kw_equation_tensorFracXYGeneral {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra R₀ F'] [Algebra F F'] [IsScalarTower R₀ F F'] : (WeierstrassCurve.toAffine ((WeierstrassCurve.Affine.baseChange W F').map (algebraMap F' (FractionRing (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F'))))).Equation ((algebraMap (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F') (FractionRing (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F'))) ((WeierstrassCurve.Affine.baseChange W F).polyToFunctionField Polynomial.X ⊗ₜ[F] 1)) ((algebraMap (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F') (FractionRing (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F'))) ((WeierstrassCurve.Affine.baseChange W F).yGen ⊗ₜ[F] 1))

theorem ModularCurve.kw_transcendental_tensorFracXGeneral {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra F F'] : Function.Injective ⇑(Polynomial.aeval ((algebraMap (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F') (FractionRing (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F'))) ((WeierstrassCurve.Affine.baseChange W F).polyToFunctionField Polynomial.X ⊗ₜ[F] 1)))

noncomputable def ModularCurve.kwFunctionFieldTensorFracHomGeneral {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra R₀ F'] [Algebra F F'] [IsScalarTower R₀ F F'] [IsDomain (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F')] : (WeierstrassCurve.Affine.baseChange W F').FunctionField →ₐ[F'] FractionRing (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F')

Map the base-changed curve's function field into the fraction field of the tensor product of the original field and the new constants.

Equations

• ModularCurve.kwFunctionFieldTensorFracHomGeneral W F F' = WeierstrassCurve.Affine.pointPullbackHomTo ⋯ ⋯

theorem ModularCurve.kw_functionFieldTensorFracHomGeneral_X {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra R₀ F'] [Algebra F F'] [IsScalarTower R₀ F F'] [IsDomain (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F')] : (kwFunctionFieldTensorFracHomGeneral W F F') ((WeierstrassCurve.Affine.baseChange W F').polyToFunctionField Polynomial.X) = (algebraMap (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F') (FractionRing (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F'))) ((WeierstrassCurve.Affine.baseChange W F).polyToFunctionField Polynomial.X ⊗ₜ[F] 1)

theorem ModularCurve.kw_functionFieldTensorFracHomGeneral_yGen {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra R₀ F'] [Algebra F F'] [IsScalarTower R₀ F F'] [IsDomain (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F')] : (kwFunctionFieldTensorFracHomGeneral W F F') (WeierstrassCurve.Affine.baseChange W F').yGen = (algebraMap (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F') (FractionRing (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F'))) ((WeierstrassCurve.Affine.baseChange W F).yGen ⊗ₜ[F] 1)

theorem ModularCurve.kw_functionFieldTensorFracHomGeneral_bijective {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra R₀ F'] [Algebra F F'] [IsScalarTower R₀ F F'] [IsDomain (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F')] : Function.Bijective ⇑(kwFunctionFieldTensorFracHomGeneral W F F')

noncomputable def ModularCurve.kwFunctionFieldTensorFracEquivGeneral {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra R₀ F'] [Algebra F F'] [IsScalarTower R₀ F F'] [IsDomain (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F')] : (WeierstrassCurve.Affine.baseChange W F').FunctionField ≃ₐ[F'] FractionRing (TensorProduct F (WeierstrassCurve.Affine.baseChange W F).FunctionField F')

Identify the base-changed curve's function field with the fraction field of the function-field tensor product.

Equations

• ModularCurve.kwFunctionFieldTensorFracEquivGeneral W F F' = AlgEquiv.ofBijective (ModularCurve.kwFunctionFieldTensorFracHomGeneral W F F') ⋯

theorem ModularCurve.kw_coordinateRingMap_basisGeneral {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra F F'] (i : ℕ × Fin 2) : (WeierstrassCurve.Affine.CoordinateRing.map (WeierstrassCurve.toAffine (WeierstrassCurve.Affine.baseChange W F)) (algebraMap F F')) ((kwCoordinateRingBasis (WeierstrassCurve.toAffine (WeierstrassCurve.Affine.baseChange W F))) i) = (kwCoordinateRingBasis ((WeierstrassCurve.toAffine (WeierstrassCurve.Affine.baseChange W F)).map (algebraMap F F'))) i

noncomputable def ModularCurve.kwCoordinateRingMapAlongGeneral {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra F F'] : (WeierstrassCurve.toAffine (WeierstrassCurve.Affine.baseChange W F)).CoordinateRing →ₐ[F] ((WeierstrassCurve.toAffine (WeierstrassCurve.Affine.baseChange W F)).map (algebraMap F F')).CoordinateRing

The affine coordinate-ring homomorphism induced by extension of the coefficient field.

Equations

• One or more equations did not get rendered due to their size.

theorem ModularCurve.kw_coordinateRingTensor_isDomainGeneral {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra F F'] : IsDomain (TensorProduct F (WeierstrassCurve.toAffine (WeierstrassCurve.Affine.baseChange W F)).CoordinateRing F')

theorem ModularCurve.kw_functionFieldTensorIsDomain_dischargeGeneral {R₀ : Type u} [Field R₀] (W : WeierstrassCurve R₀) (F : Type v) [Field F] [Algebra R₀ F] (F' : Type w) [Field F'] [Algebra F F'] : KwFunctionFieldTensorIsDomainGeneral W F F'

theorem ModularCurve.fractionRing_span_and_independent {T : Type u} {T' : Type v} [CommRing T] [IsDomain T] [CommRing T'] [IsDomain T'] {ι : Type u_1} [Fintype ι] (ιT : T' →+* T) (ιFr : FractionRing T' →+* FractionRing T) (hιT_inj : Function.Injective ⇑ιT) (hιT_fin : ιT.Finite) (hιFr_am : ∀ (t : T'), ιFr ((algebraMap T' (FractionRing T')) t) = (algebraMap T (FractionRing T)) (ιT t)) (e : ι → T) (hspanT : ∀ (t : T), ∃ (c : ι → T'), t = ∑ i : ι, ιT (c i) * e i) (hliT : ∀ (c : ι → T'), ∑ i : ι, ιT (c i) * e i = 0 → ∀ (j : ι), c j = 0) : (∀ (z : FractionRing T), ∃ (d : ι → FractionRing T'), z = ∑ i : ι, ιFr (d i) * (algebraMap T (FractionRing T)) (e i)) ∧ ∀ (d : ι → FractionRing T'), ∑ i : ι, ιFr (d i) * (algebraMap T (FractionRing T)) (e i) = 0 → ∀ (j : ι), d j = 0