← all areas

Namespace WeierstrassProjModel 173 theorems

— 146 · RelativeGroupLaw 27

directly in WeierstrassProjModel 146

• Galois-equivariant bijection between relative d-torsion and E[d] WeierstrassProjModel.exists_torsionSubset_equiv_torsionBy_galoisEquivariant 0 below · cited by 1 · depth 9
• Finiteness of n-torsion kernel schemes of a relative group law WeierstrassProjModel.isFinite_schemeKerStr_of_isPointsEval 3 below · cited by 4 · depth 9
• Points evaluation for the glued relative group law WeierstrassProjModel.kw_a2_exists_isPointsEval_of_addMorphism 5 below · cited by 2 · depth 9
• Base change of the projective Weierstrass model over Spec WeierstrassProjModel.kw_bc_baseChangeIso 4 below · cited by 6 · depth 9
• Geometric integrality of the projective Weierstrass model WeierstrassProjModel.kw_hgi_geometricallyIntegral_of_baseChangeIso 0 below · cited by 36 · depth 9
• Smoothness of the projective Weierstrass model over Spec R WeierstrassProjModel.projModelStrCR_smooth 2 below · cited by 12 · depth 9
• Existence of a commutative relative group law on the projective Weierstrass model WeierstrassProjModel.relativeGroupLaw_exists 21 below · cited by 2 · depth 9
• Good reduction at p gives an elliptic model over ℤ₍ₚ₎ WeierstrassProjModel.toProjective_isElliptic_map_of_isGoodPrimeFor 1 below · cited by 1 · depth 9
• Gluing data for the projective Weierstrass addition morphism WeierstrassProjModel.addMorphism_gluing 7 below · cited by 1 · depth 10
• Degree-zero part of the Z-chart is R[X][Y] WeierstrassProjModel.exists_ringEquiv_zChartAwayDegreeZero 0 below · cited by 2 · depth 10
• Glued addition morphism computes `addMap` when Δ≠ 0 WeierstrassProjModel.kw_a2_map_mul_of_delta_ne_zero 4 below · cited by 6 · depth 10
• Projective Weierstrass chart base change is a pullback WeierstrassProjModel.kw_bc_awayIsPushoutAll 3 below · cited by 1 · depth 10
• Properness of the projective Weierstrass model over the base WeierstrassProjModel.projModelStrCR_isProper 0 below · cited by 32 · depth 10
• Smoothness of the projective Weierstrass model from two charts WeierstrassProjModel.projModelStrCR_smooth_of_zChartBridge_of_yChartSmooth 0 below · cited by 1 · depth 10
• Relative group law on the projective Weierstrass model WeierstrassProjModel.relativeGroupLaw_exists_of_gluing 15 below · cited by 1 · depth 10
• Multiplication by n on the projective Weierstrass model is locally quasi-finite WeierstrassProjModel.schemeNsmul_locallyQuasiFinite_of_isPointsEval 2 below · cited by 2 · depth 10
• Associativity of the glued addition morphism on Proj WeierstrassProjModel.addMorphism_assoc 7 below · cited by 1 · depth 11
• Commutativity of the glued addition morphism WeierstrassProjModel.addMorphism_comm 7 below · cited by 1 · depth 11
• Right unit law for the glued addition morphism WeierstrassProjModel.addMorphism_mul_zeroSect 8 below · cited by 1 · depth 11
• Inverse law for the glued addition morphism WeierstrassProjModel.addMorphism_negMor_mul 10 below · cited by 1 · depth 11
• Glued addition morphism on the projective model lies over the base WeierstrassProjModel.addMorphism_over 0 below · cited by 6 · depth 11
• Left unit law for the glued addition morphism WeierstrassProjModel.addMorphism_zeroSect_mul 8 below · cited by 1 · depth 11
• Generic point of the projective Weierstrass model over a field WeierstrassProjModel.exists_genericPoint_projModelCR_of_field 0 below · cited by 1 · depth 11
• Chart factorisation of the glued addition morphism WeierstrassProjModel.kw_a2_liftAddMor_factor 0 below · cited by 1 · depth 11
• Chart factorisation of the six-U locus computes addMap WeierstrassProjModel.kw_a2_sixU_class_eq_addMap_of_delta_ne_zero 2 below · cited by 7 · depth 11
• Six addition-law coordinates generate the unit ideal on each chart pair WeierstrassProjModel.kw_a2_sixu_cov 0 below · cited by 1 · depth 11
• Base change of the Y-chart of a projective Weierstrass model WeierstrassProjModel.kw_bc_awayIsPushout_Y 0 below · cited by 1 · depth 11
• Base change of the Z-chart of a projective Weierstrass model WeierstrassProjModel.kw_bc_awayIsPushout_Z 1 below · cited by 1 · depth 11
• Negation on the projective Weierstrass model is a Spec R-morphism WeierstrassProjModel.negMor_over 0 below · cited by 6 · depth 11
• Outer gluing compatibility of the chart-wise addition morphisms WeierstrassProjModel.outerCompat_of_smooth 4 below · cited by 1 · depth 11
• Per-chart compatibility of the six addition loci WeierstrassProjModel.perChartCompat_of_smooth 4 below · cited by 2 · depth 11
• Field-valued points of the projective Weierstrass model WeierstrassProjModel.exists_pointEval 0 below · cited by 16 · depth 12
• Chord polynomials give minus the projective addition formulas WeierstrassProjModel.kw_a2_checks_addXYZ_crossXZ 0 below · cited by 2 · depth 12
• Doubling cross-identity between Y and Z on the curve WeierstrassProjModel.kw_a2_checks_crossYZ 0 below · cited by 2 · depth 12
• Chart factorisations of the zero section give [0:1:0] WeierstrassProjModel.kw_a2_map_one 0 below · cited by 7 · depth 12
• Negation morphism factors through the Z≠ 0 chart WeierstrassProjModel.negMor_chartFactor 0 below · cited by 2 · depth 12
• The six addition-law chart morphisms are morphisms over Spec R WeierstrassProjModel.sixU_toE_over 0 below · cited by 7 · depth 12
• Relative group law and points evaluation on the projective Weierstrass model WeierstrassProjModel.exists_relativeGroupLaw_isPointsEval_of_isElliptic_of_invertible_two 31 below · cited by 2 · depth 15
• Finite Hopf algebra representing the n-torsion of a relative group law WeierstrassProjModel.exists_hopfAlgebra_withConv_equiv_torsionSubset_of_isFinite 13 below · cited by 1 · depth 16
• Relative d-torsion matches E(F)[d] under a points-evaluation WeierstrassProjModel.exists_torsionSubset_equiv_torsionBy_of_isPointsEval 0 below · cited by 1 · depth 16
• Free rank p² ℤₚ-Hopf algebra for W[p] WeierstrassProjModel.exists_finiteFree_hopfAlgebra_padicInt_rank_psq_of_isPointsEval_of_flat 26 below · cited by 1 · depth 17
• Relative group law and points evaluation on elliptic Weierstrass Proj models WeierstrassProjModel.exists_relativeGroupLaw_isPointsEval_of_isElliptic_of_isDomain 78 below · cited by 4 · depth 17
• Flatness of the n-torsion scheme over the base WeierstrassProjModel.flat_schemeKerStr_of_isPointsEval_of_isElliptic 28 below · cited by 1 · depth 17
• Commutativity of a relative group law with additive point evaluation WeierstrassProjModel.mul_comm_of_isPointsEval 11 below · cited by 7 · depth 17
• Gluing pinned per-chart addition morphisms on E×_R E WeierstrassProjModel.exists_addMorphism_of_perChart_addMorphism_pin 43 below · cited by 5 · depth 18
• A dominant function-field point of the self-product of a projective Weierstrass model WeierstrassProjModel.exists_dominant_field_point_selfPullback_of_isElliptic 10 below · cited by 1 · depth 18
• Points evaluation for a law pinned to six addition laws WeierstrassProjModel.exists_isPointsEval_of_addMorphism_sixU_pin 9 below · cited by 2 · depth 18
• Gluing per-chart addition morphisms from a nine-element cover WeierstrassProjModel.exists_perChart_addMorphism_of_thirdLaw_nineCoverage 40 below · cited by 5 · depth 18
• Relative group law with pinned addition morphism and zero section WeierstrassProjModel.exists_relativeGroupLaw_mul_eq_one_eq_zeroSect_of_addMorphism_sixU_pin 56 below · cited by 4 · depth 18
• Existence of a third addition law covering each chart of E× E WeierstrassProjModel.exists_thirdLaw_nineCoverage_of_isElliptic_of_isDomain 16 below · cited by 5 · depth 18
• Commutativity of a relative group law with additive points evaluation WeierstrassProjModel.mul_comm_of_isPointsEval_domain 10 below · cited by 1 · depth 18
• Flatness of multiplication by n on the projective Weierstrass model WeierstrassProjModel.schemeNsmul_flat_of_isPointsEval_of_isElliptic 27 below · cited by 3 · depth 18
• Nondegeneracy of the six Lange–Ruppert elements on every chart pair WeierstrassProjModel.exists_lrSixU_ne_zero_of_isElliptic 34 below · cited by 4 · depth 19
• Gluing per-chart addition morphisms over a nine-element cover WeierstrassProjModel.exists_perChart_addMorphism_of_nineGlue_compat 2 below · cited by 1 · depth 19
• Fibrewise flatness of multiplication by n on the Weierstrass model WeierstrassProjModel.flat_schemeFibreEndo_schemeNsmul_of_isPointsEval_of_isElliptic 17 below · cited by 2 · depth 19
• Chart rings of E×_R E are integral domains WeierstrassProjModel.isDomain_chartTensor_of_isElliptic 11 below · cited by 7 · depth 19
• Integrality of the self-fibre-product of an elliptic projective model WeierstrassProjModel.isIntegral_selfPullback_of_isElliptic_field 9 below · cited by 1 · depth 19
• Chart addition law for a pinned addition morphism off the diagonal WeierstrassProjModel.kw_a2_pin_map_mul_of_ne 8 below · cited by 6 · depth 19
• Nine-element unit-ideal coverage of each chart of E× E WeierstrassProjModel.kw_lrThird_nineCoverage_of_isElliptic 0 below · cited by 1 · depth 19
• Third-law chart agrees with chord/symmetric charts on overlaps WeierstrassProjModel.kw_lrThird_toE3_compat_of_isDomain 14 below · cited by 1 · depth 19
• Integrality of the Weierstrass model and its self-products WeierstrassProjModel.kw_r0_isIntegral_pullbacks 0 below · cited by 3 · depth 19
• Overlap compatibility of pinned per-chart addition morphisms WeierstrassProjModel.perChart_addMorphism_pin_outerCompat 42 below · cited by 1 · depth 19
• Pinned per-chart addition morphisms lie over Spec R WeierstrassProjModel.perChart_addMorphism_pin_over 38 below · cited by 3 · depth 19
• Associativity of a pinned addition morphism on the projective model WeierstrassProjModel.pin_addMorphism_assoc 44 below · cited by 2 · depth 19
• Right unit identity for a pinned addition morphism WeierstrassProjModel.pin_addMorphism_mul_zeroSect 24 below · cited by 2 · depth 19
• Left-inverse identity for a pinned addition morphism WeierstrassProjModel.pin_addMorphism_negMor_mul 30 below · cited by 3 · depth 19
• Left-unit identity for a pinned addition morphism WeierstrassProjModel.pin_addMorphism_zeroSect_mul 24 below · cited by 2 · depth 19
• Smoothness of relative dimension one of the projective Weierstrass model WeierstrassProjModel.projModelStrCR_smoothOfRelativeDimension_one 3 below · cited by 36 · depth 19
• Base change of the projective Weierstrass model to an R-field WeierstrassProjModel.projModel_pullback_iso_baseChange 4 below · cited by 37 · depth 19
• Some Lange–Ruppert u_l is nonzero on a chart tensor product WeierstrassProjModel.exists_lrSixU_ne_zero_xzcharts 24 below · cited by 1 · depth 20
• Some Lange–Ruppert element is nonzero on the (1,j) chart WeierstrassProjModel.exists_lrSixU_ne_zero_ychartL 16 below · cited by 1 · depth 20
• Nonvanishing of some Lange–Ruppert chart element for j=1 WeierstrassProjModel.exists_lrSixU_ne_zero_ychartR 16 below · cited by 1 · depth 20
• The Y-chart of the projective Weierstrass model WeierstrassProjModel.exists_yChartAway_equiv_coordinateRing 0 below · cited by 6 · depth 20
• The Z-chart of the projective Weierstrass model is the affine coordinate ring WeierstrassProjModel.exists_zChartAway_equiv_coordinateRing 1 below · cited by 12 · depth 20
• Non-vanishing of an addition-law element off the diagonal WeierstrassProjModel.kw_a2_exists_sixU_ne_zero_of_pointClass_ne 6 below · cited by 2 · depth 20
• The generic point is a nonzero point of the model WeierstrassProjModel.kw_ev_genericPoint_ne_zero 14 below · cited by 2 · depth 20
• Generic-point evaluation is not 2-torsion WeierstrassProjModel.kw_ev_genericPoint_not_two_torsion 18 below · cited by 1 · depth 20
• Three generic projections of E³ are pairwise off-diagonal WeierstrassProjModel.kw_ev_triple_projections_indep 41 below · cited by 1 · depth 20
• Dominance of the six-U localisation maps on a chart product WeierstrassProjModel.kw_lrSixU_locMap_isSchemeTheoreticallyDominant 12 below · cited by 1 · depth 20
• Third-law chart factorisation computes projective addition over F WeierstrassProjModel.kw_lrThird_u3_class_eq_addMap_of_delta_ne_zero 0 below · cited by 1 · depth 20
• The (i,j) pullback chart lies over Spec R WeierstrassProjModel.kw_pcmpin_chartIso_inv_cover_fst_over 0 below · cited by 1 · depth 20
• Dense witness for outer compatibility of pinned chart addition maps WeierstrassProjModel.kw_pcmpin_outerCompat_dense_witness 41 below · cited by 1 · depth 20
• Nontriviality of the chart rings of E ×_R E WeierstrassProjModel.nontrivial_chartTensor_of_isElliptic 10 below · cited by 1 · depth 20
• Proj base change for the projective Weierstrass model WeierstrassProjModel.projModel_isPullback_baseChange 3 below · cited by 2 · depth 20
• Self-compatibility of the three charts over a domain WeierstrassProjModel.thirdLaw_selfCompat_of_isDomain_of_lrSixU_compat 0 below · cited by 1 · depth 20
• Chart evaluation lands on the curve, with i-th coordinate 1 WeierstrassProjModel.chartEval_equation_and_apply_self_eq_one 0 below · cited by 4 · depth 21
• Z-chart dehomogenisation: degree-zero part away from X₂ WeierstrassProjModel.exists_ringEquiv_zChartAwayDegreeZero_univ 0 below · cited by 2 · depth 21
• Projective addition coordinates do not all vanish for distinct points WeierstrassProjModel.kw_a2_add_ne_zero_of_pointClass_ne 0 below · cited by 1 · depth 21
• Chord-law six-u elements evaluate to minus the projective addition formulae WeierstrassProjModel.kw_a2_productMap_sixU_inl_eq_neg_add 3 below · cited by 1 · depth 21
• Base change of the X₁-chart of the projective Weierstrass model is cartesian WeierstrassProjModel.kw_bc_awayIsPushout_Y_univ 0 below · cited by 3 · depth 21
• Base change is cartesian on the X₂-chart WeierstrassProjModel.kw_bc_awayIsPushout_Z_univ 1 below · cited by 3 · depth 21
• Generic point of an elliptic model: chart factorisation with 2P≠[0:1:0] WeierstrassProjModel.kw_ev_genericPoint_chartFactor_addMap_self_ne_zeroClass 17 below · cited by 1 · depth 21
• Chart factorisation of the generic point avoids [0:1:0] WeierstrassProjModel.kw_ev_genericPoint_chartFactor_pointClass_ne_zero 13 below · cited by 2 · depth 21
• Independent chart factorisations of the three projections of E³ WeierstrassProjModel.kw_ev_triple_projections_chartFactor_pointClass_indep 40 below · cited by 1 · depth 21
• Nonvanishing of the chord Z-component on the Y-chart WeierstrassProjModel.kw_lrSixU_addZ_ne_zero_ychartL 15 below · cited by 1 · depth 21
• Nonvanishing of the chord Z-component on (i,1) charts WeierstrassProjModel.kw_lrSixU_addZ_ne_zero_ychartR 15 below · cited by 1 · depth 21
• Generic chart projections of E×_R E have distinct point classes WeierstrassProjModel.kw_lr_chartTensor_genericProj_pointClass_ne 17 below · cited by 1 · depth 21
• Pinned per-chart addition maps agree at generic points of overlaps WeierstrassProjModel.kw_pcmpin_outerCompat_genericPoint_agree 40 below · cited by 1 · depth 21
• Nontriviality of the charts of a projective Weierstrass model WeierstrassProjModel.nontrivial_chart_of_isElliptic 0 below · cited by 4 · depth 21
• Affine charts of an elliptic projective Weierstrass model are domains WeierstrassProjModel.isDomain_chart_of_isElliptic 10 below · cited by 3 · depth 22
• Y-chart evaluation sends chart generators to coordinates of [0:1:0] WeierstrassProjModel.kwYChartEval_gen_eq 0 below · cited by 6 · depth 22
• Projective addition-law polynomials evaluate to the negated formulas WeierstrassProjModel.kw_a2_checks 2 below · cited by 1 · depth 22
• Doubling the generic Z-chart point avoids [0:1:0] WeierstrassProjModel.kw_ev_genericPoint_zChart_addMap_self_ne_zeroClass 15 below · cited by 1 · depth 22
• Generic point of the Weierstrass model factors through the Z-chart WeierstrassProjModel.kw_ev_genericPoint_zChart_factor 11 below · cited by 2 · depth 22
• Chart generators X_m/Xᵢ are nonzero on the projective Weierstrass model WeierstrassProjModel.kw_lrChart_gen_ne_zero 0 below · cited by 3 · depth 22
• Left Y-chart partial evaluation of the chord Z-coordinate WeierstrassProjModel.kw_lrSixU_addZ_ychartL_partialEval 2 below · cited by 1 · depth 22
• Partial evaluation of the chord Z-coordinate at [0:1:0] WeierstrassProjModel.kw_lrSixU_addZ_ychartR_partialEval 2 below · cited by 1 · depth 22
• Chart generators are not diagonal in the chart tensor product WeierstrassProjModel.kw_lr_chartTensor_genProd_ne_genTensOne 4 below · cited by 1 · depth 22
• Injectivity of a Z-chart factorisation of the generic point WeierstrassProjModel.kw_ev_genericPoint_zChart_psi_injective 11 below · cited by 1 · depth 23
• Value of the addition polynomial Z at the left infinity point WeierstrassProjModel.kw_lrAdd_Z_aeval_left_infty 0 below · cited by 1 · depth 23
• The Z addition polynomial at the right point at infinity WeierstrassProjModel.kw_lrAdd_Z_aeval_right_infty 0 below · cited by 1 · depth 23
• Nonvanishing of 2y+a₁x+a₃ in the Z-chart ring WeierstrassProjModel.kw_lrChart_negY_gen_ne_zero 0 below · cited by 1 · depth 23
• Chart generators are not diagonal: the case i,j ≠ 1 WeierstrassProjModel.kw_lr_chartTensor_genProd_ne_genTensOne_xzCase 0 below · cited by 1 · depth 23
• Rational endomorphism subring acts on the projective Weierstrass model WeierstrassProjModel.exists_action_rationalEndSubring_of_isAlgClosed 81 below · cited by 3 · depth 29
• Coefficient base-change homomorphism of projective Weierstrass models WeierstrassProjModel.exists_isCoefficientHom 0 below · cited by 52 · depth 29
• Coordinate-reading points evaluation for the projective Weierstrass model WeierstrassProjModel.exists_isPointsEval_apply_eq_some_of_eq_comp_zChartInclusion 91 below · cited by 5 · depth 29
• Variable change induces an isomorphism of projective Weierstrass models WeierstrassProjModel.exists_isVariableChangeHom_isIso_projMap 0 below · cited by 27 · depth 29
• Coordinate-reading points-evaluation for the projective Weierstrass model WeierstrassProjModel.exists_isPointsEval_apply_eq_some_of_eq_comp_zChartInclusion_of_isDomain 83 below · cited by 11 · depth 30
• Relative group law for unit discriminant over any base WeierstrassProjModel.exists_relativeGroupLaw_one_eq_zeroSect_isPointsEval_of_isUnit 81 below · cited by 4 · depth 30
• Rationally represented endomorphisms come from the projective Weierstrass model WeierstrassProjModel.exists_schemeHomOver_forall_apply_eq_of_isRationallyRepresented_of_isAlgClosed 75 below · cited by 1 · depth 30
• Agreement off a finite set of points extends to all points WeierstrassProjModel.apply_schemeHomOverComp_eq_of_finite_of_forall_not_mem 73 below · cited by 1 · depth 31
• Relative group law on a projective Weierstrass model WeierstrassProjModel.exists_relativeGroupLaw_one_eq_zeroSect_isPointsEval_of_isElliptic_of_isDomain 73 below · cited by 1 · depth 31
• Zero section lies in the origin chart, with vanishing coordinates WeierstrassProjModel.isOriginChartSection_kwZeroSect_kwYChartEval 0 below · cited by 11 · depth 31
• A variable change commutes with the zero section [0:1:0] WeierstrassProjModel.kwZeroSect_comp_projMap_of_isVariableChangeHom 0 below · cited by 8 · depth 31
• Rigidity lemma for projective Weierstrass models over a ring WeierstrassProjModel.eq_snd_comp_of_comp_eq_const_of_isElliptic 18 below · cited by 1 · depth 32
• Commutative relative group law with unit the zero section WeierstrassProjModel.exists_relativeGroupLaw_isCommutative_one_eq_zeroSect_of_isElliptic_of_baseChangeIso 83 below · cited by 1 · depth 32
• Global sections of the projective Weierstrass model after base change WeierstrassProjModel.bijective_appTop_pullback_snd_projModelStrCR 6 below · cited by 1 · depth 33
• n-torsion of a projective Weierstrass model is finite and flat WeierstrassProjModel.isFinite_and_flat_schemeKerStr_of_isPointsEval_of_isElliptic 28 below · cited by 7 · depth 33
• Properness, integrality and reduced self-product over a field WeierstrassProjModel.isProper_and_isIntegral_and_isReduced_selfPullback_pullback_snd_of_baseChangeIso 11 below · cited by 4 · depth 33
• Base change of the projective Weierstrass model over a ring WeierstrassProjModel.projModel_isPullback_baseChange_ring 3 below · cited by 2 · depth 33
• Relative group law on the projective Weierstrass model over a Noetherian domain WeierstrassProjModel.relativeGroupLaw_nonempty_of_isElliptic_of_baseChangeIso_of_isNoetherianRing 74 below · cited by 1 · depth 33
• Degree-zero functions on the two standard charts of a Weierstrass model WeierstrassProjModel.exists_fromZeroRingHom_eq_of_awayMap_eq 0 below · cited by 1 · depth 34
• Two-chart description of global sections of the Weierstrass model WeierstrassProjModel.projModelCR_sections_twoChart 0 below · cited by 1 · depth 34
• Relative group law on the projective model from a nine-element chart coverage WeierstrassProjModel.relativeGroupLaw_nonempty_of_thirdLaw_nineCoverage 69 below · cited by 1 · depth 34
• Relative group law from pinned per-chart addition morphisms WeierstrassProjModel.relativeGroupLaw_nonempty_of_perChart_addMorphism_pin 64 below · cited by 1 · depth 35
• Relative group law from a pinned addition morphism WeierstrassProjModel.relativeGroupLaw_nonempty_of_addMorphism_sixU_pin 56 below · cited by 1 · depth 36
• Dual-number lifts of a point form a line WeierstrassProjModel.exists_ne_forall_exists_eq_specMap_map_smul_comp_of_specMap_fstHom_comp_eq 14 below · cited by 2 · depth 38
• E[n] has rank n² at every point of the base WeierstrassProjModel.finrank_schemeKerStr_eq_sq_of_isPointsEval_of_isElliptic 715 below · cited by 2 · depth 38
• Origin-preserving isomorphisms of Weierstrass models are variable changes WeierstrassProjModel.exists_variableChange_smul_eq_and_projMap_eq_inv_of_iso_of_kwZeroSect_comp_eq_of_isArtinianRing 16 below · cited by 1 · depth 40
• Naturality of the variable-change morphism of projective Weierstrass models WeierstrassProjModel.projMap_coefficientHom_comp_projMap_variableChangeHom_eq 0 below · cited by 1 · depth 40
• A variable change inducing the identity on Proj is trivial WeierstrassProjModel.variableChange_eq_one_of_projMap_eq_id 3 below · cited by 1 · depth 40
• Pole orders 2 and 3 with unit leading coefficients under a zero-preserving isomorphism WeierstrassProjModel.coeff_laurent_zChart_of_iso_of_kwZeroSect_comp_eq 8 below · cited by 1 · depth 41
• Laurent expansion on the Z-chart and its pole filtration WeierstrassProjModel.exists_laurent_zChartRing_filtration 2 below · cited by 1 · depth 41
• Zero-preserving isomorphism of projective models restricts to Z-charts WeierstrassProjModel.exists_ringEquiv_zChartRing_of_iso_of_kwZeroSect_comp_eq 3 below · cited by 1 · depth 41
• Variable-change homomorphism on the Z-chart of Proj WeierstrassProjModel.exists_zChartIota_comp_projMap_eq_specMap_comp_zChartIota_of_isVariableChangeHom 0 below · cited by 2 · depth 41
• Morphisms from a projective Weierstrass model are determined on the Z-chart WeierstrassProjModel.hom_ext_of_zChartIota_comp_eq 1 below · cited by 1 · depth 41

WeierstrassProjModel.RelativeGroupLaw 27

• A relative Drinfeld basis consists of q-torsion points WeierstrassProjModel.RelativeGroupLaw.IsDrinfeldBasisOver.exists_comp_fst_schemeKer_eq 1 below · cited by 13 · depth 29
• Translating a commutative relative group law to the zero section WeierstrassProjModel.RelativeGroupLaw.exists_isCommutative_one_eq_zeroSect_of_isCommutative 0 below · cited by 4 · depth 29
• Unit section factors through the origin chart iff it is [0:1:0] WeierstrassProjModel.RelativeGroupLaw.exists_isOriginChartSection_iff_one_eq_kwZeroSect 0 below · cited by 30 · depth 30
• Relative group laws pull back along a cartesian square WeierstrassProjModel.RelativeGroupLaw.exists_relativeGroupLaw_comp_eq_of_isPullback 0 below · cited by 8 · depth 30
• Base change of the relative Drinfeld basis divisor and torsion ideal WeierstrassProjModel.RelativeGroupLaw.basisDivisorOver_comap_mapOnProdOver 3 below · cited by 2 · depth 31
• q-torsion ideal sheaf transports along a cartesian square WeierstrassProjModel.RelativeGroupLaw.comap_ker_schemeKer_eq_of_isPullback 4 below · cited by 1 · depth 31
• Graph-ideal product of [a]P+[b]Q transports along a cartesian square WeierstrassProjModel.RelativeGroupLaw.comap_prodKerGraph_linComb_eq_of_isPullback 5 below · cited by 1 · depth 31
• Relative group laws with equal unit section coincide WeierstrassProjModel.RelativeGroupLaw.mul_eq_of_one_eq_of_isElliptic 19 below · cited by 12 · depth 31
• Module-finite representability of relative Drinfeld Γ(q)-bases WeierstrassProjModel.RelativeGroupLaw.exists_moduleFinite_represents_isDrinfeldBasisOver_of_two_le 45 below · cited by 1 · depth 32
• Inversion in a relative group law is the negation morphism WeierstrassProjModel.RelativeGroupLaw.inv_val_eq_comp_negMor_of_one_eq_kwZeroSect 83 below · cited by 1 · depth 32
• Closedness of the relative Drinfeld-basis locus WeierstrassProjModel.RelativeGroupLaw.exists_idealSheafData_comap_eq_bot_iff_isDrinfeldBasisOver 43 below · cited by 3 · depth 33
• Relative group laws commute on K-points of elliptic models WeierstrassProjModel.RelativeGroupLaw.mul_comm_at_field_of_isElliptic_of_baseChangeIso 4 below · cited by 3 · depth 33
• Base change of a relative group law along R → K WeierstrassProjModel.RelativeGroupLaw.exists_pullback_snd_schemeHomOverEquiv 0 below · cited by 2 · depth 34
• Reducedness of the n-torsion scheme for invertible n WeierstrassProjModel.RelativeGroupLaw.isReduced_schemeKer_of_isPointsEval_of_isUnit 45 below · cited by 2 · depth 34
• Relative group laws on Weierstrass models over a domain commute WeierstrassProjModel.RelativeGroupLaw.isCommutative_of_isElliptic_of_baseChangeIso_of_isDomain 11 below · cited by 1 · depth 35
• Rigidity: two relative group laws with the zero section as unit agree on field points WeierstrassProjModel.RelativeGroupLaw.mul_eq_of_one_eq_zeroSect_of_isElliptic_of_baseChangeIso 19 below · cited by 1 · depth 35
• Agreement of relative group laws descends from K-points to F-points WeierstrassProjModel.RelativeGroupLaw.mul_eq_of_algebraTower_of_mul_eq 0 below · cited by 1 · depth 36
• Relative group laws with equal unit agree on K-points WeierstrassProjModel.RelativeGroupLaw.mul_eq_of_one_eq_of_isAlgClosed 5 below · cited by 1 · depth 36
• Representability of q-torsion by a module-finite flat algebra WeierstrassProjModel.RelativeGroupLaw.exists_moduleFinite_flat_represents_nsmul_eq_one 29 below · cited by 2 · depth 37
• Rigidity: equal units at id force equal multiplications on K-points WeierstrassProjModel.RelativeGroupLaw.mul_eq_at_id_of_one_eq_at_id_of_isAlgClosed 3 below · cited by 1 · depth 37
• Relative group law on T-points yields a group object over Spec R WeierstrassProjModel.RelativeGroupLaw.exists_grpObj_eq 0 below · cited by 1 · depth 38
• Transport of n-fold multiples along a group-law morphism WeierstrassProjModel.RelativeGroupLaw.nsmul_comp_eq_of_mul_comp_eq 0 below · cited by 1 · depth 38
• Rank of a finite flat surjective group-scheme homomorphism equals kernel rank WeierstrassProjModel.RelativeGroupLaw.finrank_eq_finrank_pullback_snd_one_of_hom 0 below · cited by 2 · depth 40
• Transfer of a relative group law between two structure ports WeierstrassProjModel.RelativeGroupLaw.exists_goodReductionJacobian_mul_eq_and_nsmul_eq 0 below · cited by 1 · depth 41
• Translation by a section is an automorphism over the base WeierstrassProjModel.RelativeGroupLaw.exists_iso_comp_eq_and_comp_hom_eq_mul 0 below · cited by 1 · depth 43
• Relative group laws on the projective Weierstrass model are commutative WeierstrassProjModel.RelativeGroupLaw.isCommutative_of_isElliptic_of_baseChangeIso 54 below · cited by 1 · depth 43
• Commutativity of a relative group law on an elliptic Weierstrass model WeierstrassProjModel.RelativeGroupLaw.mul_comm_of_forall_field_mul_comm 50 below · cited by 1 · depth 44