← all areas

Namespace GoodReductionJacobian 674 theorems

— 21 · AbelianSchemePropertyBundle 170 · BareDeformation 80 · PartialAction 13 · RelativeGroupLaw 390

directly in GoodReductionJacobian 21

• The abelian-scheme property bundle passes to fibres GoodReductionJacobian.abelianSchemePropertyBundle_fibreStr 0 below · cited by 19 · depth 13
• Abelian scheme bundle after base change to mathbf Z_{(ℓ)} GoodReductionJacobian.abelianSchemePropertyBundle_pullback_snd_ratLocalizedAt 1 below · cited by 3 · depth 15
• Isomorphisms of generic fibres of abelian schemes extend uniquely GoodReductionJacobian.exists_schemeHomOver_inverse_of_abelianSchemePropertyBundle_of_genericFibre 35 below · cited by 1 · depth 16
• The abelian-scheme property bundle passes to the generic fibre GoodReductionJacobian.abelianSchemePropertyBundle_genericFibreStr 0 below · cited by 1 · depth 25
• Products of abelian schemes over a field, in bundled form GoodReductionJacobian.abelianSchemePropertyBundle_prodStr 11 below · cited by 5 · depth 29
• Unique commutative relative group law with prescribed unit section GoodReductionJacobian.exists_relativeGroupLaw_one_eq_and_isCommutative_of_smooth_of_isClosedImmersion_proj_of_isNoetherianRing 306 below · cited by 3 · depth 29
• Local group law with prescribed unit over a Noetherian base GoodReductionJacobian.exists_away_relativeGroupLaw_baseChange_one_eq_of_isNoetherianRing_of_isClopen 303 below · cited by 1 · depth 30
• The constant first-order deformation of an abelian scheme GoodReductionJacobian.exists_bareDeformation_dualNumber_isPullback_fst_comp_eq_id 14 below · cited by 1 · depth 30
• Gluing relative group laws from basic opens of the base GoodReductionJacobian.exists_relativeGroupLaw_one_eq_of_forall_exists_away 0 below · cited by 1 · depth 30
• Group law on a geometric fibre is independent of the geometric point GoodReductionJacobian.nonempty_relativeGroupLaw_geometricFibre_of_nonempty_of_ker_eq 4 below · cited by 2 · depth 30
• Spreading a relative group law to a basic open neighbourhood GoodReductionJacobian.exists_not_mem_forall_nonempty_relativeGroupLaw_geometricFibre_of_not_mem 301 below · cited by 1 · depth 31
• Relative group law over the local ring at s GoodReductionJacobian.exists_relativeGroupLaw_baseChange_localizationAtPrime_one_eq_of_isNoetherianRing_of_isClopen 300 below · cited by 1 · depth 31
• Unique commutative relative group law from abelian geometric fibres GoodReductionJacobian.exists_relativeGroupLaw_one_eq_and_isCommutative_of_forall_abelian_geometricFibre 389 below · cited by 1 · depth 31
• Relative group law over the completed local ring at s GoodReductionJacobian.exists_relativeGroupLaw_baseChange_adicCompletion_one_eq_of_forall_nonempty_relativeGroupLaw_geometricFibre 297 below · cited by 1 · depth 32
• Relative group law over the completed local ring at a point of W GoodReductionJacobian.exists_relativeGroupLaw_baseChange_adicCompletion_one_eq_of_isNoetherianRing_of_isClopen 298 below · cited by 1 · depth 32
• Fibrewise criterion for smoothness and abelian base changes GoodReductionJacobian.smooth_and_isConnected_preimage_and_abelianSchemePropertyBundle_of_forall_geometricFibre 147 below · cited by 1 · depth 32
• Compatible group laws on all 𝔪-adic thickenings GoodReductionJacobian.exists_forall_relativeGroupLaw_adicThickening_one_eq_of_isNoetherianRing_of_isClopen 235 below · cited by 1 · depth 33
• Group law on A/R from laws on its I-adic thickenings GoodReductionJacobian.exists_relativeGroupLaw_one_eq_of_forall_relativeGroupLaw_adicThickening_of_isAdicComplete 115 below · cited by 2 · depth 33
• Algebraising the inversion of a compatible tower of group laws GoodReductionJacobian.exists_inv_hom_forall_comp_eq_of_forall_relativeGroupLaw_adicThickening_of_isAdicComplete 111 below · cited by 1 · depth 34
• Algebraisation of a compatible tower of group laws GoodReductionJacobian.exists_mul_hom_forall_lift_comp_eq_of_forall_relativeGroupLaw_adicThickening_of_isAdicComplete 111 below · cited by 1 · depth 34
• Group axioms over a complete base from levelwise laws GoodReductionJacobian.lift_comp_mul_eq_of_forall_relativeGroupLaw_adicThickening_of_isAdicComplete 4 below · cited by 1 · depth 34

GoodReductionJacobian.AbelianSchemePropertyBundle 170

• Abelian scheme property bundle is stable under base change to a field GoodReductionJacobian.AbelianSchemePropertyBundle.baseChange_of_field 12 below · cited by 35 · depth 12
• Morphisms from a split torus to an abelian variety are constant GoodReductionJacobian.AbelianSchemePropertyBundle.exists_eq_comp_of_hom_spec_addMonoidAlgebra_pi_int 6 below · cited by 11 · depth 13
• Abelian schemes over a field are geometrically integral GoodReductionJacobian.AbelianSchemePropertyBundle.geometricallyIntegral 10 below · cited by 38 · depth 13
• Morphisms G_m → A into an abelian scheme are constant GoodReductionJacobian.AbelianSchemePropertyBundle.exists_eq_comp_of_hom_spec_laurentPolynomial 5 below · cited by 1 · depth 14
• Every k-morphism A¹_k → A into an abelian scheme is constant GoodReductionJacobian.AbelianSchemePropertyBundle.exists_eq_comp_of_hom_spec_polynomial 4 below · cited by 1 · depth 15
• An abelian scheme over a field is integral GoodReductionJacobian.AbelianSchemePropertyBundle.isIntegral_of_field 7 below · cited by 39 · depth 15
• Extension of generic-fibre morphisms into an abelian scheme over a DVR GoodReductionJacobian.AbelianSchemePropertyBundle.genericFibreRestrict_surjective_of_quasiCompact 32 below · cited by 1 · depth 16
• Weil extension theorem for abelian-scheme targets over a DVR GoodReductionJacobian.AbelianSchemePropertyBundle.exists_extension_of_subset_opens 26 below · cited by 1 · depth 17
• Finite endomorphisms of abelian varieties are flat GoodReductionJacobian.AbelianSchemePropertyBundle.flat_of_isFinite 19 below · cited by 8 · depth 23
• Invertible sheaf on A with positive m^g-coefficient of χ GoodReductionJacobian.AbelianSchemePropertyBundle.exists_isInvertible_coeff_pos_forall_eulerChar_tensorPow_eq 664 below · cited by 1 · depth 26
• Projectivity of abelian varieties over an algebraically closed field GoodReductionJacobian.AbelianSchemePropertyBundle.exists_isInvertible_finiteBySections 610 below · cited by 6 · depth 26
• Unique extension of a generic-fibre homomorphism to an abelian scheme GoodReductionJacobian.AbelianSchemePropertyBundle.existsUnique_extension_hom_of_genericFibre 36 below · cited by 2 · depth 28
• Linear maps of complex uniformisations come from scheme homomorphisms GoodReductionJacobian.AbelianSchemePropertyBundle.exists_hom_mapPt_eq_pointEquiv_symm_quotientMap_of_le_comap 282 below · cited by 1 · depth 28
• Complex uniformisation: G(ℂ)≅ℂ^g/Λ with holomorphic charts GoodReductionJacobian.AbelianSchemePropertyBundle.exists_submodule_pointEquiv_quotient_differentiableOn_appLE 208 below · cited by 1 · depth 28
• Very ampleness by sections from geometric fibres GoodReductionJacobian.AbelianSchemePropertyBundle.closedImmersionBySections_of_forall_geometricFibre_of_finite_of_forall_isPullback 24 below · cited by 2 · depth 29
• Rigidity: fixing the unit section and all geometric points GoodReductionJacobian.AbelianSchemePropertyBundle.eq_id_of_one_comp_eq_of_forall_comp_eq_of_isAlgClosed 55 below · cited by 3 · depth 29
• Rigidity of morphisms of abelian schemes along nilpotent base changes GoodReductionJacobian.AbelianSchemePropertyBundle.eq_of_one_comp_eq_one_comp_of_isPullback_of_comp_eq_comp_of_isNilpotent 57 below · cited by 1 · depth 29
• Lattice-linear maps of uniformisations are algebraic on curves GoodReductionJacobian.AbelianSchemePropertyBundle.exists_hom_curve_mapPt_eq_pointEquiv_symm_quotientMap_mapPt 152 below · cited by 1 · depth 29
• Algebraicity of a point homomorphism generated by curves GoodReductionJacobian.AbelianSchemePropertyBundle.exists_hom_mapPt_eq_of_forall_curve_eq_mapPt_of_isAlgClosed 38 below · cited by 1 · depth 29
• Open locus where pulled-back sections form a basis GoodReductionJacobian.AbelianSchemePropertyBundle.exists_isOpen_forall_isSectionBasisOn_pullback_iff 1,094 below · cited by 3 · depth 29
• Every k-point of an abelian variety is a sum of curve points GoodReductionJacobian.AbelianSchemePropertyBundle.exists_smoothProperCurves_sum_surjective_of_isAlgClosed 97 below · cited by 2 · depth 29
• Sequential compactness of the ℂ-points of an abelian scheme GoodReductionJacobian.AbelianSchemePropertyBundle.exists_tendsto_appLE_complex 188 below · cited by 1 · depth 29
• Openness of the locus of relative group laws on geometric fibres GoodReductionJacobian.AbelianSchemePropertyBundle.isOpen_setOf_nonempty_relativeGroupLaw_geometricFibre 325 below · cited by 2 · depth 29
• Homomorphism on k-points extends to all test schemes GoodReductionJacobian.AbelianSchemePropertyBundle.mapPt_mul_eq_mul_mapPt_of_forall_point 2 below · cited by 1 · depth 29
• Finite projective sections and base change of section bases GoodReductionJacobian.AbelianSchemePropertyBundle.sections_finite_projective_and_isSectionBasisOn_pullback_type0 1,094 below · cited by 5 · depth 29
• Base change to a basic open of a smooth proper family with connected fibres GoodReductionJacobian.AbelianSchemePropertyBundle.baseChange_away_of_smooth_of_isProper 0 below · cited by 1 · depth 30
• First Čech cohomology of mathcal O_A has dimension g GoodReductionJacobian.AbelianSchemePropertyBundle.cechFinrank_unit_one_eq_of_charP 834 below · cited by 7 · depth 30
• Rigidity: endomorphisms agreeing on unit and geometric points GoodReductionJacobian.AbelianSchemePropertyBundle.eq_of_one_comp_eq_one_comp_of_forall_comp_eq_comp_of_isAlgClosed 56 below · cited by 3 · depth 30
• Rigidity: finite-order endomorphism fixing n-torsion is the identity GoodReductionJacobian.AbelianSchemePropertyBundle.eq_schemeHomOverId_of_schemeHomOverNpow_eq_of_forall_isTorsionPoint_of_isUnit_of_three_le 761 below · cited by 3 · depth 30
• Trivial kernel forces χ(L)² = 1 GoodReductionJacobian.AbelianSchemePropertyBundle.eulerChar_sq_eq_one_of_kernelTrivial 944 below · cited by 3 · depth 30
• Degree-one Čech cohomology of an abelian scheme with pinned endomorphism action GoodReductionJacobian.AbelianSchemePropertyBundle.exists_cls_one_endo_linearMap_pinned_unitPullback 130 below · cited by 2 · depth 30
• Euler characteristic of M^{⊗ n} on an abelian scheme GoodReductionJacobian.AbelianSchemePropertyBundle.exists_forall_eulerChar_tensorPow_eq_mul_pow 787 below · cited by 5 · depth 30
• Λ-equivariant lifting of abelian schemes along square-zero surjections GoodReductionJacobian.AbelianSchemePropertyBundle.exists_isPullback_forall_comp_act_eq_of_separabilityElement_of_ker_mul_ker_eq_bot_of_isAlgClosed 1,034 below · cited by 1 · depth 30
• Symmetric invertible sheaf with prescribed L⊗[-1]^*L GoodReductionJacobian.AbelianSchemePropertyBundle.exists_isSymmetric_nonempty_tensor_pullback_negMor_iso_of_kernelPts_finite 799 below · cited by 1 · depth 30
• Base change for global sections of an ample sheaf GoodReductionJacobian.AbelianSchemePropertyBundle.exists_linearEquiv_tensorProduct_sections_pullback_type0 1,091 below · cited by 3 · depth 30
• Finite projective sections of an invertible module on an abelian scheme GoodReductionJacobian.AbelianSchemePropertyBundle.finite_and_projective_sections_of_closedImmersionBySections_type0 1,090 below · cited by 2 · depth 30
• Abelian schemes over a ring are geometrically integral GoodReductionJacobian.AbelianSchemePropertyBundle.geometricallyIntegral_of_commRing 13 below · cited by 8 · depth 30
• Commutativity of a relative group law on an abelian scheme GoodReductionJacobian.AbelianSchemePropertyBundle.isCommutative 106 below · cited by 18 · depth 30
• Openness of the relative group law locus over a Noetherian base GoodReductionJacobian.AbelianSchemePropertyBundle.isOpen_setOf_nonempty_relativeGroupLaw_geometricFibre_of_isNoetherianRing 302 below · cited by 1 · depth 30
• Base change of the abelian scheme property bundle GoodReductionJacobian.AbelianSchemePropertyBundle.of_isPullback 13 below · cited by 68 · depth 30
• Abelian-scheme property bundle along a pullback over a field isomorphism GoodReductionJacobian.AbelianSchemePropertyBundle.of_isPullback_ringEquiv 14 below · cited by 1 · depth 30
• Global functions on a fibre of an abelian scheme GoodReductionJacobian.AbelianSchemePropertyBundle.bijective_appTop_fibre_of_isPullback 17 below · cited by 6 · depth 31
• Global functions on a base change of an abelian scheme GoodReductionJacobian.AbelianSchemePropertyBundle.bijective_specIso_inv_comp_appTop_of_isPullback 50 below · cited by 15 · depth 31
• Pull-back along [n] multiplies χ of a line bundle by n^{2g} GoodReductionJacobian.AbelianSchemePropertyBundle.eulerChar_pullback_schemeNsmul_eq_pow_mul_eulerChar 766 below · cited by 2 · depth 31
• Mumford's Riemann–Roch: χ(M)²=rankK(M) GoodReductionJacobian.AbelianSchemePropertyBundle.eulerChar_sq_eq_finrank_of_forall_iff_isInStabilizer_type0 934 below · cited by 5 · depth 31
• Pinned endomorphism action on Čech algebras of an abelian scheme GoodReductionJacobian.AbelianSchemePropertyBundle.exists_endo_algHom_pinned_unitPullback_of_cls_cup 81 below · cited by 2 · depth 31
• Étale-local splitting of the n-torsion of an abelian scheme GoodReductionJacobian.AbelianSchemePropertyBundle.exists_etale_typeGroup_nsmul_eq_one_iff_of_isUnit 795 below · cited by 1 · depth 31
• Halving a point after a faithfully flat base extension GoodReductionJacobian.AbelianSchemePropertyBundle.exists_faithfullyFlat_mul_self_eq_schemeHomOverComp 716 below · cited by 1 · depth 31
• Noetherian approximation of an abelian scheme with very ample bundle GoodReductionJacobian.AbelianSchemePropertyBundle.exists_fg_subalgebra_abelianScheme_closedImmersionBySections_pullback_iso 156 below · cited by 2 · depth 31
• Higher Čech cohomology vanishes on the fibre over a field GoodReductionJacobian.AbelianSchemePropertyBundle.exists_forall_subsingleton_HSucc_pullback_fst_of_closedImmersionBySections 1,039 below · cited by 2 · depth 31
• Graded Čech algebra of an abelian scheme and Künneth injectivity GoodReductionJacobian.AbelianSchemePropertyBundle.exists_gradedMonoid_kunneth_injective_cech_unit 102 below · cited by 2 · depth 31
• Line bundles extend from the generic fibre of an abelian scheme GoodReductionJacobian.AbelianSchemePropertyBundle.exists_isInvertible_pullback_iso_of_isDiscreteValuationRing 42 below · cited by 3 · depth 31
• Equivariant lifting of abelian schemes along a small surjection GoodReductionJacobian.AbelianSchemePropertyBundle.exists_isPullback_forall_comp_act_eq_of_separabilityElement_of_ker_mul_maximalIdeal_eq_bot_of_isAlgClosed 1,033 below · cited by 1 · depth 31
• Two-variable Snapper polynomial for χ(M₀^{⊗ a}⊗ M₁^{⊗ b}) GoodReductionJacobian.AbelianSchemePropertyBundle.exists_mvPolynomial_totalDegree_le_forall_eulerChar_tensorPow_tensor_tensorPow_eq 95 below · cited by 2 · depth 31
• Divisibility of k-points of an abelian variety, k algebraically closed GoodReductionJacobian.AbelianSchemePropertyBundle.exists_nsmulPt_eq_of_isAlgClosed_of_isCommutative 706 below · cited by 5 · depth 31
• Positivity of geometric fibre h⁰ spreads from a generic geometric point GoodReductionJacobian.AbelianSchemePropertyBundle.geomFibreH0Finrank_pos_of_pos_of_injective_of_isDomain 79 below · cited by 1 · depth 31
• Openness and base change of the abelian-fibre locus GoodReductionJacobian.AbelianSchemePropertyBundle.isOpen_setOf_abelian_geometricFibre_and_preimage_eq_of_isPullback 376 below · cited by 2 · depth 31
• Lower bound g ≤ dim_K check H¹(A,mathcal O_A) in characteristic p GoodReductionJacobian.AbelianSchemePropertyBundle.le_cechFinrank_unit_one_of_charP 747 below · cited by 3 · depth 31
• Rigidity: unit-preserving maps of abelian schemes are homomorphisms GoodReductionJacobian.AbelianSchemePropertyBundle.mul_comp_eq_mul_comp_of_one_comp_eq_one 58 below · cited by 2 · depth 31
• Abelian scheme property is stable under fibre product over Spec R GoodReductionJacobian.AbelianSchemePropertyBundle.prodStr_commRing 15 below · cited by 8 · depth 31
• Unit-preserving morphism of abelian schemes is a homomorphism GoodReductionJacobian.AbelianSchemePropertyBundle.schemeHomOverComp_mul_eq_mul_of_schemeHomOverComp_one_eq_one 105 below · cited by 3 · depth 31
• Geometric fibres of an abelian scheme: smooth, irreducible, dimension g GoodReductionJacobian.AbelianSchemePropertyBundle.smooth_irreducibleSpace_geometricFibre_of_topologicalKrullDim_eq 21 below · cited by 1 · depth 31
• Vanishing of Čech 𝒪-cohomology above the relative dimension GoodReductionJacobian.AbelianSchemePropertyBundle.subsingleton_HSucc_unit_of_le 621 below · cited by 5 · depth 31
• Global functions on an abelian scheme descend to the base GoodReductionJacobian.AbelianSchemePropertyBundle.surjective_appTop_and_pullback_snd_away 50 below · cited by 6 · depth 31
• f_*mathcal O_A=𝒪 universally for abelian schemes GoodReductionJacobian.AbelianSchemePropertyBundle.bijective_algebraMap_sections_pullback 49 below · cited by 15 · depth 32
• Global functions on an abelian variety: check H⁰(mathcal O_A) is one-dimensional GoodReductionJacobian.AbelianSchemePropertyBundle.cechFinrank_unit_zero_eq_one 13 below · cited by 4 · depth 32
• Rigidity: a homomorphism fixing one geometric fibre is the identity GoodReductionJacobian.AbelianSchemePropertyBundle.eq_schemeHomOverId_of_forall_schemeHomOverComp_eq_quotient_of_isDomain 64 below · cited by 1 · depth 32
• Euler characteristic of the dual of an invertible sheaf GoodReductionJacobian.AbelianSchemePropertyBundle.eulerChar_dual_eq_neg_one_pow_mul_eulerChar 788 below · cited by 1 · depth 32
• Riemann–Roch: χ(M)χ(M^∨)=(-1)^grkK(M) GoodReductionJacobian.AbelianSchemePropertyBundle.eulerChar_mul_eulerChar_dual_eq_neg_one_pow_mul_finrank_of_forall_iff_isInStabilizer 790 below · cited by 1 · depth 32
• Filtration of [n]_*mathcal O_A by n-torsion invertible modules GoodReductionJacobian.AbelianSchemePropertyBundle.exists_affSES_filtration_pushforwardUnit_schemeNsmul 757 below · cited by 1 · depth 32
• Čech-level primitivity of 1-cocycles on A× A GoodReductionJacobian.AbelianSchemePropertyBundle.exists_d_eq_unitPullback_mul_sub_fst_sub_snd_of_d_one_eq_zero 42 below · cited by 5 · depth 32
• Geometric n-torsion basis of rank 2g GoodReductionJacobian.AbelianSchemePropertyBundle.exists_finComb_basis_nsmul_eq_one_of_isAlgClosed 703 below · cited by 1 · depth 32
• n-torsion of an abelian scheme is finite étale of rank n^{2g} GoodReductionJacobian.AbelianSchemePropertyBundle.exists_finite_etale_rankAtStalk_eq_pow_nsmul_eq_one_iff_of_isUnit 780 below · cited by 1 · depth 32
• The n-torsion Hopf algebra of an abelian variety GoodReductionJacobian.AbelianSchemePropertyBundle.exists_hopfAlgebra_torsion_finrank_eq_pow_and_nsmulAlgHom_eq 707 below · cited by 5 · depth 32
• Picard equality locus on an abelian scheme is closed GoodReductionJacobian.AbelianSchemePropertyBundle.exists_isClosedImmersion_lfp_forall_iff_locIsoOnBase_pullback 223 below · cited by 2 · depth 32
• Base change of an abelian scheme with polarisation and automorphism GoodReductionJacobian.AbelianSchemePropertyBundle.exists_isPullback_closedImmersionBySections_comp_eq_comp_of_isIso_of_pullback_iso 18 below · cited by 1 · depth 32
• Lifting abelian schemes along nilpotent surjections of Artinian bases GoodReductionJacobian.AbelianSchemePropertyBundle.exists_isPullback_of_isArtinianRing_of_isNilpotent_ker_of_le_cechFinrank 817 below · cited by 2 · depth 32
• Primitives of A[n] inject into Čech H¹(𝒪_A) GoodReductionJacobian.AbelianSchemePropertyBundle.exists_linearMap_primitives_HSucc_unit_injective_of_torsion_points_equiv 34 below · cited by 2 · depth 32
• An abelian variety of dimension g has an affine cover of size g+1 GoodReductionJacobian.AbelianSchemePropertyBundle.exists_orderedAffineCover_card_eq 613 below · cited by 7 · depth 32
• Base change to a field of an abelian scheme with sections presentation GoodReductionJacobian.AbelianSchemePropertyBundle.exists_relativeGroupLaw_pullbackSnd_specMap_and_closedImmersionBySections 18 below · cited by 1 · depth 32
• A rigidified bundle detecting local isomorphy on the base GoodReductionJacobian.AbelianSchemePropertyBundle.exists_rigidifiedLineBundle_forall_locIsoOnBase_pullback_iff 65 below · cited by 2 · depth 32
• Finite order of sheaf-preserving automorphisms over a finite field GoodReductionJacobian.AbelianSchemePropertyBundle.exists_schemeHomOverNpow_eq_schemeHomOverId_of_isIso_of_pullback_iso_of_finite 68 below · cited by 1 · depth 32
• Integrality and fibre irreducibility for an abelian scheme and its square GoodReductionJacobian.AbelianSchemePropertyBundle.isIntegral_and_isPreirreducible_fibre_of_isDomain 14 below · cited by 2 · depth 32
• Openness of the abelian geometric-fibre locus over a basic open GoodReductionJacobian.AbelianSchemePropertyBundle.isOpen_setOf_not_mem_and_abelian_geometricFibre 370 below · cited by 1 · depth 32
• Additivity in the endomorphism of degree-one Čech pull-back GoodReductionJacobian.AbelianSchemePropertyBundle.sub_sub_mem_range_d_zero_of_unitPullback_pinned_of_pointwise_mul 56 below · cited by 1 · depth 32
• Pullback along [n] detects vanishing of Čech cohomology GoodReductionJacobian.AbelianSchemePropertyBundle.subsingleton_HSucc_of_subsingleton_HSucc_pullback_schemeNsmul 709 below · cited by 1 · depth 32
• Local multiplicative frames for eigenparts of [n]_*𝒪_A GoodReductionJacobian.AbelianSchemePropertyBundle.exists_affineOpens_bijective_smul_eigenSubdatum_and_bijective_smul_eigenOne 733 below · cited by 1 · depth 33
• n-torsion of an abelian scheme is finite étale GoodReductionJacobian.AbelianSchemePropertyBundle.exists_finite_etale_isClosedImmersion_nsmul_eq_one_iff_of_isUnit 14 below · cited by 1 · depth 33
• Symmetric principal square roots over a finite faithfully flat algebra GoodReductionJacobian.AbelianSchemePropertyBundle.exists_finite_faithfullyFlat_atPrime_symmetric_principalSqrt_of_faithfullyFlat_of_isNoetherianRing 1,106 below · cited by 2 · depth 33
• Morphism lifts iff its obstruction cochain is a coboundary GoodReductionJacobian.AbelianSchemePropertyBundle.exists_hom_lift_iff_forall_mem_range_d_of_local_lifts 23 below · cited by 1 · depth 33
• Stabiliser of an invertible sheaf as closed subgroup scheme GoodReductionJacobian.AbelianSchemePropertyBundle.exists_isClosedImmersion_relativeGroupLaw_forall_iff_locIsoOnBase_sliceAt_mumfordBundle_of_isAlgClosed 637 below · cited by 2 · depth 33
• Symmetrising an invertible sheaf with trivial kernel GoodReductionJacobian.AbelianSchemePropertyBundle.exists_isSymmetric_kernelTrivial_locIsoOnBase_of_kernelTrivial_of_isAlgClosed 806 below · cited by 2 · depth 33
• Primitives of H inject into Čech H¹(𝒪_A) GoodReductionJacobian.AbelianSchemePropertyBundle.exists_linearMap_primitives_HSucc_unit_injective_of_isIso_shear 30 below · cited by 1 · depth 33
• Dense open locus where b x^{-j}u⁻ᶜ avoids a closed set GoodReductionJacobian.AbelianSchemePropertyBundle.exists_opens_dense_forall_mul_pow_inv_mul_pow_inv_notMem 707 below · cited by 2 · depth 33
• Rigidity lemma: contraction spreads to an open neighbourhood GoodReductionJacobian.AbelianSchemePropertyBundle.exists_opens_forall_comp_eq_comp_of_forall_comp_eq_comp 51 below · cited by 1 · depth 33
• Obstruction cocycle of local lifts along a small surjection GoodReductionJacobian.AbelianSchemePropertyBundle.exists_pointDerivations_obstruction_cocycle_of_local_lifts_hom 15 below · cited by 2 · depth 33
• Smooth lifting of an abelian scheme along a small surjection GoodReductionJacobian.AbelianSchemePropertyBundle.exists_smooth_isPullback_of_ker_mul_maximalIdeal_eq_bot_of_le_cechFinrank 779 below · cited by 1 · depth 33
• Character eigendecomposition of [n]_*𝒪_A on every open GoodReductionJacobian.AbelianSchemePropertyBundle.finite_isNsmulCharacter_and_ncard_eq_pow_and_bijective_sum_eigenInclusion 730 below · cited by 1 · depth 33
• Positive h⁰ on geometric fibres of a Proj-presented line bundle GoodReductionJacobian.AbelianSchemePropertyBundle.geomFibreH0Finrank_pos_of_closedImmersionBySections 64 below · cited by 1 · depth 33
• Closedness of the locus of fibrewise τ-constancy GoodReductionJacobian.AbelianSchemePropertyBundle.isClosed_setOf_forall_comp_eq_comp 0 below · cited by 1 · depth 33
• Trivial kernel over one field fibre descends to local base GoodReductionJacobian.AbelianSchemePropertyBundle.kernelTrivial_of_kernelTrivial_baseChange_field_of_isLocalRing 1,048 below · cited by 1 · depth 33
• Abelian scheme property bundle from a principal open cover GoodReductionJacobian.AbelianSchemePropertyBundle.of_forall_isPullback_away 0 below · cited by 1 · depth 33
• Descent of the abelian-scheme property bundle along faithfully flat base change GoodReductionJacobian.AbelianSchemePropertyBundle.of_isPullback_of_faithfullyFlat 3 below · cited by 1 · depth 33
• Abelian scheme property transported along a cartesian square GoodReductionJacobian.AbelianSchemePropertyBundle.of_isPullback_of_field 13 below · cited by 5 · depth 33
• Nilpotent thickenings preserve the abelian-scheme property bundle GoodReductionJacobian.AbelianSchemePropertyBundle.of_isPullback_of_isNilpotent_ker_of_relativeGroupLaw 1 below · cited by 2 · depth 33
• Rank n^{2g} of the n-torsion subscheme of an abelian scheme GoodReductionJacobian.AbelianSchemePropertyBundle.rankAtStalk_eq_pow_of_nsmul_eq_one_iff_of_isUnit 766 below · cited by 1 · depth 33
• Global functions on a geometric fibre of an abelian scheme GoodReductionJacobian.AbelianSchemePropertyBundle.bijective_appTop_fibre_of_isPullback_of_isAlgClosed 16 below · cited by 1 · depth 34
• Trivial eigencomponent of [n]_*mathcal O_A is mathcal O_A GoodReductionJacobian.AbelianSchemePropertyBundle.bijective_smul_eigenOne 722 below · cited by 1 · depth 34
• Local unit χ-eigensection of [n]_*𝒪_A GoodReductionJacobian.AbelianSchemePropertyBundle.exists_affineOpens_isUnit_eigenSubdatum 729 below · cited by 1 · depth 34
• Independence of the obstruction cochain of the chosen local lifts GoodReductionJacobian.AbelianSchemePropertyBundle.exists_d_eq_obstruction_cocycle_sub_of_local_lifts_hom 16 below · cited by 2 · depth 34
• Symmetric square roots over a finite flat algebra over S_𝔭 GoodReductionJacobian.AbelianSchemePropertyBundle.exists_finite_faithfullyFlat_atPrime_isSymmetric_locIsoOnBase_of_faithfullyFlat 1,066 below · cited by 1 · depth 34
• Lifting a morphism whose obstruction cochain is a coboundary GoodReductionJacobian.AbelianSchemePropertyBundle.exists_hom_lift_of_pointDerivations_coboundary 19 below · cited by 1 · depth 34
• Lifting a morphism when the obstruction cochain is a coboundary GoodReductionJacobian.AbelianSchemePropertyBundle.exists_hom_lift_of_pointDerivations_coboundary_of_smooth_source 19 below · cited by 1 · depth 34
• Closed-subscheme representability of the kernel K(L), Noetherian base GoodReductionJacobian.AbelianSchemePropertyBundle.exists_isClosedImmersion_forall_iff_locIsoOnBase_sliceAt_mumfordBundle_of_isNoetherianRing 156 below · cited by 8 · depth 34
• Primitives of H inject into degree-one Čech cohomology of mathcal O_A GoodReductionJacobian.AbelianSchemePropertyBundle.exists_linearMap_primitives_HSucc_unit_injective_of_forall_affineOpens_coaction 15 below · cited by 1 · depth 34
• Abelian schemes: obstruction 2-cocycle is a coboundary GoodReductionJacobian.AbelianSchemePropertyBundle.exists_pointDerivations_d_eq_obstruction_two_cocycle 765 below · cited by 1 · depth 34
• Obstruction cocycle comparing local lifts along a small extension GoodReductionJacobian.AbelianSchemePropertyBundle.exists_pointDerivations_obstruction_cocycle_of_local_lifts_hom_of_smooth_source 15 below · cited by 1 · depth 34
• ℓ-power torsion points are Zariski-dense in an abelian variety GoodReductionJacobian.AbelianSchemePropertyBundle.forall_mem_of_isClosed_of_forall_torsion_mem 705 below · cited by 2 · depth 34
• Constancy of geometric-fibre h⁰ over a local base GoodReductionJacobian.AbelianSchemePropertyBundle.geomFibreH0Finrank_eq_of_subsingleton_HSucc_closedFibre 89 below · cited by 1 · depth 34
• Kernel triviality for a bundle with χ(L)² = 1 GoodReductionJacobian.AbelianSchemePropertyBundle.kernelTrivial_of_eulerChar_sq_eq_one 1,033 below · cited by 2 · depth 34
• Trivial Mumford kernel from the geometric fibres GoodReductionJacobian.AbelianSchemePropertyBundle.kernelTrivial_of_forall_kernelTrivial_geomFibre_of_isNoetherianRing 161 below · cited by 2 · depth 34
• Kernel triviality for a symmetric square root over a finite algebra GoodReductionJacobian.AbelianSchemePropertyBundle.kernelTrivial_of_isSymmetric_of_locIsoOnBase_of_finite_atPrime_of_faithfullyFlat 855 below · cited by 1 · depth 34
• Primitivity of the obstruction cocycle of an abelian scheme GoodReductionJacobian.AbelianSchemePropertyBundle.exists_d_eq_unitPullback_mul_sub_fst_sub_snd_obstruction_two_cocycle 57 below · cited by 1 · depth 35
• Global sections of an abelian scheme over a field are constants GoodReductionJacobian.AbelianSchemePropertyBundle.exists_eq_algebraMap_sections_top 14 below · cited by 3 · depth 35
• Finite flat corepresentability of the symmetric-root class functor over W GoodReductionJacobian.AbelianSchemePropertyBundle.exists_finite_faithfullyFlat_corepresents_symmRoot_classFunctor_under 1,031 below · cited by 1 · depth 35
• Lagrange resolvent over the n-torsion deck group GoodReductionJacobian.AbelianSchemePropertyBundle.exists_fintype_torsionSubset_sum_deckApp_mem_eigenSubmodule 691 below · cited by 1 · depth 35
• Higher Čech vanishing spreads from the closed geometric fibre GoodReductionJacobian.AbelianSchemePropertyBundle.exists_forall_subsingleton_HSucc_pullback_of_subsingleton_HSucc_closedFibre 85 below · cited by 1 · depth 35
• Morphisms agreeing after [n] differ locally by n-torsion translation GoodReductionJacobian.AbelianSchemePropertyBundle.exists_iSup_eq_top_iota_comp_eq_iota_comp_comp_translate_of_comp_schemeNsmul_eq 36 below · cited by 2 · depth 35
• Transfer of h¹ and vanishing to the residue-field fibre GoodReductionJacobian.AbelianSchemePropertyBundle.exists_le_cechFinrank_and_subsingleton_HSucc_of_isPullback_residueField 627 below · cited by 1 · depth 35
• Separating a K-point from its non-trivial n-torsion translates GoodReductionJacobian.AbelianSchemePropertyBundle.exists_mem_basicOpen_forall_notMem_basicOpen_deckApp 707 below · cited by 1 · depth 35
• n-torsion translations act transitively on fibres of [n] GoodReductionJacobian.AbelianSchemePropertyBundle.exists_mem_torsionSubset_translate_base_eq_of_schemeNsmul_base_eq 37 below · cited by 1 · depth 35
• Spreading symmetric principal square roots to a basic open GoodReductionJacobian.AbelianSchemePropertyBundle.exists_not_mem_finite_faithfullyFlat_symmetric_principalSqrt_of_faithfullyFlat_atPrime_of_isNoetherianRing 1,132 below · cited by 1 · depth 35
• Positivity of geometric h⁰ spreads to a basic open set GoodReductionJacobian.AbelianSchemePropertyBundle.exists_not_mem_forall_geomFibreH0Finrank_pos_of_forall_atPrime 980 below · cited by 1 · depth 35
• Spreading K(L)=A[2] from S_𝔭 to S_g GoodReductionJacobian.AbelianSchemePropertyBundle.exists_not_mem_kernelIsTwoTorsion_away_of_kernelIsTwoTorsion_atPrime_of_isNoetherianRing 162 below · cited by 1 · depth 35
• Spreading Rosati compatibility from S_𝔭 to a basic open GoodReductionJacobian.AbelianSchemePropertyBundle.exists_not_mem_rosatiCompatible_away_of_rosatiCompatible_atPrime_of_isNoetherianRing 231 below · cited by 1 · depth 35
• Nonzero n-torsion K[ε]-point at the origin GoodReductionJacobian.AbelianSchemePropertyBundle.exists_nsmul_eq_one_dualNumber_ne_one_of_natCast_eq_zero 11 below · cited by 1 · depth 35
• Every point of a proper K-scheme specialises to a K-point GoodReductionJacobian.AbelianSchemePropertyBundle.exists_point_specializes_base_closedPoint 0 below · cited by 1 · depth 35
• Symmetric square roots with 2-torsion kernel are principal GoodReductionJacobian.AbelianSchemePropertyBundle.kernelTrivial_of_isSymmetric_of_locIsoOnBase_of_forall_kernelIsTwoTorsion_geomFibre 795 below · cited by 1 · depth 35
• Birigidified invertible modules on A× A over small extensions GoodReductionJacobian.AbelianSchemePropertyBundle.nonempty_iso_of_pullback_iso_of_sliceAt_one_of_isPullback_of_ker_mul_self_of_isNoetherianRing 133 below · cited by 3 · depth 35
• Trivialisation of (u× v)^*Λ(L) on both unit slices GoodReductionJacobian.AbelianSchemePropertyBundle.nonempty_pullback_sliceAt_one_pullback_mumfordBundle_iso_unit_of_comp_one_eq 3 below · cited by 2 · depth 35
• Flat descent for the symmetric square root class functor GoodReductionJacobian.AbelianSchemePropertyBundle.symmRoot_classFunctor_injective_and_exists_of_flat_of_surjective_typeZero 116 below · cited by 1 · depth 35
• Inversion acts as -1 on Čech 1-cocycles of 𝒪_A GoodReductionJacobian.AbelianSchemePropertyBundle.exists_d_eq_unitPullback_inv_add_unitPullback_id_of_d_one_eq_zero 55 below · cited by 2 · depth 36
• Local corepresentability of admissible rigidified bundle classes GoodReductionJacobian.AbelianSchemePropertyBundle.exists_equiv_admClassFunctor_ringHom_natural_of_isLocalRing 1,021 below · cited by 1 · depth 36
• Given one symmetric root, root and admissible class functors agree GoodReductionJacobian.AbelianSchemePropertyBundle.exists_equiv_symmRoot_adm_classFunctor_natural 27 below · cited by 1 · depth 36
• Čech–Hopf package with endomorphisms for abelian surfaces GoodReductionJacobian.AbelianSchemePropertyBundle.exists_gradedMonoid_kunneth_injective_cupGenerated_endo_cech_unit_of_topologicalKrullDim_eq_two 935 below · cited by 2 · depth 36
• Ideal-theoretic representability of the Rosati-compatibility locus GoodReductionJacobian.AbelianSchemePropertyBundle.exists_ideal_forall_rosatiCompatible_baseChange_iff_forall_map_eq_zero 229 below · cited by 1 · depth 36
• Spreading a symmetric principal square root to a basic open neighbourhood GoodReductionJacobian.AbelianSchemePropertyBundle.exists_not_mem_finite_faithfullyFlat_symmetric_principalSqrt_of_finite_atPrime 200 below · cited by 1 · depth 36
• Positivity of h⁰ specialises to the special fibre over a DVR GoodReductionJacobian.AbelianSchemePropertyBundle.geomFibreH0Finrank_pos_special_of_pos_generic_of_isDiscreteValuationRing 79 below · cited by 1 · depth 36
• Flat descent of symmetry and square-root clauses for invertible modules GoodReductionJacobian.AbelianSchemePropertyBundle.isSymmetric_locIsoOnBase_of_pullback_baseChangeSnd_of_flat_of_surjective 81 below · cited by 1 · depth 36
• Čech H¹ of A×_k A detected by the two axis sections GoodReductionJacobian.AbelianSchemePropertyBundle.mem_range_d_zero_of_unitPullback_section_mem_range 84 below · cited by 1 · depth 36
• Symmetric invertible sheaf trivial on closed fibre, Artin local base GoodReductionJacobian.AbelianSchemePropertyBundle.nonempty_iso_unit_of_isSymmetric_of_pullback_residue_iso_unit_of_isUnit_two_of_isArtinianRing 129 below · cited by 1 · depth 36
• Symmetric invertible sheaf trivial modulo a square-zero ideal GoodReductionJacobian.AbelianSchemePropertyBundle.nonempty_iso_unit_of_pullback_iso_unit_of_isSymmetric_of_ker_mul_maximalIdeal_of_isUnit_two_of_isNoetherianRing 126 below · cited by 2 · depth 36
• Euler characteristic agrees on generic and special fibres GoodReductionJacobian.AbelianSchemePropertyBundle.eulerChar_pullback_generic_eq_eulerChar_pullback_special_of_isDiscreteValuationRing 92 below · cited by 1 · depth 37
• Equivariant Čech realisation of the primitives of A[p] GoodReductionJacobian.AbelianSchemePropertyBundle.exists_linearMap_primitives_ker_d_one_forall_unitPullback_sub_mem_range_of_charP 839 below · cited by 2 · depth 37
• Symmetric principal root spreads from S_𝔭 to a finite flat cover GoodReductionJacobian.AbelianSchemePropertyBundle.exists_not_mem_finite_faithfullyFlat_symmetric_principalSqrt_away_mul_of_symmetric_principalSqrt_faithfullyFlat_atPrime 20 below · cited by 1 · depth 37
• Spreading a symmetric principal square root to a principal localisation GoodReductionJacobian.AbelianSchemePropertyBundle.exists_not_mem_forall_isLocalization_powers_symmetric_principalSqrt_of_isLocalization_primeCompl 195 below · cited by 1 · depth 37
• Fibrewise h⁰ positivity spreads from a prime to a stage GoodReductionJacobian.AbelianSchemePropertyBundle.exists_not_mem_forall_isUnit_geomFibreH0Finrank_pos_pullback_of_stage 15 below · cited by 1 · depth 37
• Degree-two Čech classes on an abelian surface are cup products GoodReductionJacobian.AbelianSchemePropertyBundle.exists_sub_sum_cup_mem_range_d_one_of_mem_ker_d_two_of_topologicalKrullDim_eq_two 927 below · cited by 1 · depth 37
• Invertible module with non-zero section and co-section is trivial GoodReductionJacobian.AbelianSchemePropertyBundle.nonempty_iso_unit_of_ne_zero_section_dual 23 below · cited by 1 · depth 37
• Čech finiteness and vanishing Euler characteristic of 𝒪_A GoodReductionJacobian.AbelianSchemePropertyBundle.cechFinite_unit_and_eulerChar_unit_eq_zero 836 below · cited by 1 · depth 38
• Maps equal after [n] differ locally by n-torsion translation GoodReductionJacobian.AbelianSchemePropertyBundle.exists_iSup_eq_top_iota_comp_eq_iota_comp_comp_translation_of_comp_schemeNsmul_eq 45 below · cited by 4 · depth 38
• Pinned cocycle map from primitives to degree-one Čech cocycles GoodReductionJacobian.AbelianSchemePropertyBundle.exists_linearMap_primitives_ker_d_one_and_lifts_of_forall_affineOpens_coaction 15 below · cited by 1 · depth 38
• Spreading out kernel triviality from the local stage to a neighbourhood GoodReductionJacobian.AbelianSchemePropertyBundle.exists_not_mem_dvd_forall_isLocalization_powers_kernelTrivial_pullback_of_kernelTrivial_atPrime 168 below · cited by 1 · depth 38
• Descent of a symmetric square root to a finite stage GoodReductionJacobian.AbelianSchemePropertyBundle.exists_not_mem_forall_isLocalization_powers_exists_isSymmetric_locIsoOnBase_iso_of_isLocalization_primeCompl 29 below · cited by 1 · depth 38
• Čech Euler characteristics of twists as polynomial values GoodReductionJacobian.AbelianSchemePropertyBundle.exists_polynomial_coeff_eq_forall_eulerChar_tensor_tensorPow_eq 104 below · cited by 1 · depth 38
• Pull-back of descended difference cochains modulo coboundaries GoodReductionJacobian.AbelianSchemePropertyBundle.unitPullback_sub_unitPullback_mem_range_d_zero_of_coaction_lifts 0 below · cited by 1 · depth 38
• Spreading symmetry and the square relation from C₀ to C[1/rr'] GoodReductionJacobian.AbelianSchemePropertyBundle.exists_not_mem_forall_isLocalization_powers_mul_isSymmetric_locIsoOnBase_pullback_of_isLocalization_primeCompl 20 below · cited by 1 · depth 39
• Invertible module over a semilocalisation descends to r-inverting algebras GoodReductionJacobian.AbelianSchemePropertyBundle.exists_not_mem_forall_isUnit_exists_isInvertible_pullback_iso_of_isLocalization_primeCompl 21 below · cited by 1 · depth 39
• Spreading triviality of K from the local ring to a basic open GoodReductionJacobian.AbelianSchemePropertyBundle.exists_not_mem_forall_kernelTrivial_isLocalization_powers_of_kernelTrivial_isLocalization_primeCompl_of_finite 167 below · cited by 1 · depth 39
• Triviality of K(τ) spreads from S_𝔭 to some S_g GoodReductionJacobian.AbelianSchemePropertyBundle.exists_not_mem_kernelTrivial_away_of_kernelTrivial_atPrime_of_isNoetherianRing 163 below · cited by 1 · depth 40

GoodReductionJacobian.BareDeformation 80

• Endomorphism lifts to a regluing iff its Kodaira–Spencer obstruction vanishes GoodReductionJacobian.BareDeformation.exists_comp_eq_comp_iff_map_tmul_sub_eq_zero_of_isRegluingBy_of_hom_bare 78 below · cited by 1 · depth 30
• Isomorphic regluings have cohomologous tangent cocycles GoodReductionJacobian.BareDeformation.exists_d_eq_sub_of_isIso_of_isTangentCoordsOfPairAt_bare 20 below · cited by 1 · depth 30
• Bare deformations are regluings carrying a cocycle tangent class GoodReductionJacobian.BareDeformation.exists_isRegluingBy_exists_isTangentCoordsOfPairAt_of_bareDeformation_bare 31 below · cited by 1 · depth 30
• Regluing a bare deformation along a Čech tangent cocycle GoodReductionJacobian.BareDeformation.exists_isRegluingBy_isTangentCoordsOfPairAt_bare 144 below · cited by 2 · depth 30
• Tangent class of a base-changed reglued bare deformation GoodReductionJacobian.BareDeformation.exists_isRegluingBy_isTangentCoordsOfPairAt_comp_of_isPullback_ringHom_bare 5 below · cited by 1 · depth 30
• Unique level-N structure on a bare deformation GoodReductionJacobian.BareDeformation.exists_level_lift_of_smoothOfRelativeDimension 58 below · cited by 4 · depth 30
• Regluings with cohomologous tangent cocycles give isomorphic deformations GoodReductionJacobian.BareDeformation.isIso_of_isRegluingBy_of_exists_d_eq_sub_bare 22 below · cited by 1 · depth 30
• Re-gluing preserves smoothness of relative dimension n GoodReductionJacobian.BareDeformation.smoothOfRelativeDimension_of_isRegluingBy 0 below · cited by 1 · depth 30
• Tangent cochain of a re-glued deformation is a cocycle GoodReductionJacobian.BareDeformation.d_one_apply_eq_zero_of_isRegluingBy_of_isTangentCoordsOfPairAt_bare 17 below · cited by 1 · depth 31
• Cohomologous tangent cocycles give compatible chart automorphisms GoodReductionJacobian.BareDeformation.exists_chartIso_comp_eq_of_isRegluingBy_of_exists_d_eq_sub 20 below · cited by 2 · depth 31
• Isomorphic regluings give compatible chart automorphisms GoodReductionJacobian.BareDeformation.exists_chartIso_comp_eq_of_isRegluingBy_of_isIso 1 below · cited by 2 · depth 31
• Lifting an endomorphism to a re-glued deformation: obstruction criterion GoodReductionJacobian.BareDeformation.exists_comp_eq_comp_iff_add_map_tmul_sub_eq_zero_of_isRegluingBy_of_local_lifts_bare 77 below · cited by 2 · depth 31
• Compatible chart automorphisms make the two tangent cocycles cohomologous GoodReductionJacobian.BareDeformation.exists_d_eq_sub_of_chartIso_comp_eq_of_isTangentCoordsOfPairAt 17 below · cited by 2 · depth 31
• Gluing deformation charts along overlap automorphisms GoodReductionJacobian.BareDeformation.exists_glued_scheme_of_overlap_isos 3 below · cited by 3 · depth 31
• Every bare deformation re-glues a fixed one on an affine cover GoodReductionJacobian.BareDeformation.exists_isRegluingBy_of_bareDeformation_bare 11 below · cited by 1 · depth 31
• Re-gluing commutes with base change along φ GoodReductionJacobian.BareDeformation.exists_isRegluingBy_of_isRegluingBy_of_isPullback_of_preimage_eq 0 below · cited by 1 · depth 31
• Functoriality of tangent coordinates under a semilinear self-base-change GoodReductionJacobian.BareDeformation.exists_isTangentCoordsOfPairAt_comp_of_isPullback_ringHom_of_comp_eq_of_over_over_bare 3 below · cited by 1 · depth 31
• Overlap automorphism realising a tangent cocycle component GoodReductionJacobian.BareDeformation.exists_overlap_iso_isTangentCoordsOfPairAt_bare 6 below · cited by 1 · depth 31
• Point-derivation tangent coordinates for the overlaps of a regluing GoodReductionJacobian.BareDeformation.exists_pointDerivations_isTangentCoordsOfPairAt_of_isRegluingBy_bare 15 below · cited by 1 · depth 31
• Commutative group law on a smooth cartesian lift over B GoodReductionJacobian.BareDeformation.exists_relativeGroupLaw_of_isPullback_of_smooth 136 below · cited by 3 · depth 31
• Triple-overlap cocycle identity for the regluing automorphisms GoodReductionJacobian.BareDeformation.exists_restrict_comp_eq_of_isTangentCoordsOfPairAt_of_d_eq_zero_bare 18 below · cited by 1 · depth 31
• Torsion kernels of a bare deformation are base changes GoodReductionJacobian.BareDeformation.exists_schemeKer_comparison 1 below · cited by 3 · depth 31
• Clopenness of the level locus in the N-torsion subscheme GoodReductionJacobian.BareDeformation.isClopen_levelPiece 18 below · cited by 1 · depth 31
• Regluings along intertwined transition data are isomorphic GoodReductionJacobian.BareDeformation.isIso_of_isRegluingBy_of_forall_comp_hom_eq 0 below · cited by 3 · depth 31
• Geometric fibres of the lifted level locus are (ℤ/N)² GoodReductionJacobian.BareDeformation.levelPiece_fibre 0 below · cited by 1 · depth 31
• Lifted level piece: closed immersion, finite flat of rank N² GoodReductionJacobian.BareDeformation.levelPiece_isClosedImmersion_finite_flat_finrank 39 below · cited by 2 · depth 31
• Group-law and level stability of the lifted level piece W GoodReductionJacobian.BareDeformation.levelPiece_points 4 below · cited by 1 · depth 31
• Uniqueness of the lifted level subscheme of a bare deformation GoodReductionJacobian.BareDeformation.levelPiece_unique 41 below · cited by 1 · depth 31
• Endomorphism of an open fixing a nilpotent thickening's reduction is pointwise trivial GoodReductionJacobian.BareDeformation.base_eq_of_morphismRestrict_comp_eq 0 below · cited by 1 · depth 32
• τ-twisted obstruction cochain of local lifts is a cocycle GoodReductionJacobian.BareDeformation.d_twisted_hom_obstruction_cochain_eq_zero_of_isRegluingBy_bare 12 below · cited by 1 · depth 32
• Lifting a ring action to a bare deformation GoodReductionJacobian.BareDeformation.exists_act_of_forall_exists_comp_eq_comp_of_isArtinianRing 28 below · cited by 1 · depth 32
• Coboundary criterion for lifting an endomorphism to a reglued deformation GoodReductionJacobian.BareDeformation.exists_comp_eq_comp_iff_forall_mem_range_d_of_isRegluingBy_of_twisted_local_lifts_bare 32 below · cited by 1 · depth 32
• Comparison map, cartesian square and smoothness for a glued chart scheme GoodReductionJacobian.BareDeformation.exists_comparison_isPullback_smooth_of_glued 0 below · cited by 1 · depth 32
• Correcting a bare deformation so that each Λ-endomorphism lifts GoodReductionJacobian.BareDeformation.exists_forall_exists_comp_eq_comp_of_separabilityElement_of_ker_mul_maximalIdeal_eq_bot 253 below · cited by 1 · depth 32
• Chartwise lifts and their τ-twisted obstruction cochain GoodReductionJacobian.BareDeformation.exists_local_lifts_twisted_hom_obstruction_cochain_of_isRegluingBy_bare 32 below · cited by 1 · depth 32
• Four-term re-gluing identity for the endomorphism obstruction cocycle GoodReductionJacobian.BareDeformation.exists_orderedAffineCover_d_eq_unitPullback_hom_obstruction_cocycle_sub_of_isRegluingBy_bare 33 below · cited by 1 · depth 32
• Pair tangent field transported by a cartesian self-map GoodReductionJacobian.BareDeformation.isTangentOfPair_specMap_comp_of_isPullback_ringHom_of_comp_eq_bare 0 below · cited by 1 · depth 32
• N-torsion is a subgroup, stable under lifted endomorphisms GoodReductionJacobian.BareDeformation.nsmulPt_eq_one_of_mul_inv_one_pushPt_comp 0 below · cited by 1 · depth 32
• Closure on points of the level image in a bare deformation GoodReductionJacobian.BareDeformation.range_subset_image_lev_of_mul_inv_one_pushPt 0 below · cited by 1 · depth 32
• Chart-wise lifts of an endomorphism into a reglued deformation GoodReductionJacobian.BareDeformation.exists_chart_lift_comp_eq_of_isRegluingBy_bare 31 below · cited by 2 · depth 33
• Regluing law: four-term obstruction combination is a coboundary GoodReductionJacobian.BareDeformation.exists_d_eq_unitPullback_hom_obstruction_cocycle_sub_baseChange_of_local_lifts_factor_bare 31 below · cited by 1 · depth 33
• Serre–Tate lifting of an abelian scheme along its formal group GoodReductionJacobian.BareDeformation.exists_isFormalCoordinates_liftsCoordinates_of_isArtinianRing_of_isAlgClosed 1,160 below · cited by 1 · depth 33
• Refinement of a cover on which local lifts factor GoodReductionJacobian.BareDeformation.exists_orderedAffineCover_local_lifts_factor_bare 0 below · cited by 2 · depth 33
• Affine frame for a bare deformation and its residue fibre GoodReductionJacobian.BareDeformation.exists_orderedAffineCover_unit_chart_frame_bare 2 below · cited by 1 · depth 33
• Separability element trivialises the obstruction cocycle GoodReductionJacobian.BareDeformation.exists_pointDerivations_forall_map_hom_obstruction_cocycle_add_sub_eq_zero_of_separabilityElement_bare 45 below · cited by 1 · depth 33
• Λ-action on the special fibre of a bare deformation GoodReductionJacobian.BareDeformation.exists_specialFibre_act_comp_eq_of_act_bare 0 below · cited by 1 · depth 33
• Transporting pair tangent coordinates to a subchart of a local lift GoodReductionJacobian.BareDeformation.exists_algHom_isTangentCoordsOfPairAt_regluing_of_local_lift_factor_bare 10 below · cited by 2 · depth 34
• Refining four chart factorisations to a common overlap GoodReductionJacobian.BareDeformation.exists_factor_inf_of_local_lifts_factor_bare 0 below · cited by 2 · depth 34
• Serre–Tate lifting along one small surjection GoodReductionJacobian.BareDeformation.exists_isFormalCoordinates_liftsCoordinates_of_ker_mul_maximalIdeal_eq_bot 1,159 below · cited by 1 · depth 34
• Tangent coordinates for a pair of local lifts GoodReductionJacobian.BareDeformation.exists_isTangentCoordsOfPairAt_local_lifts_factor_bare 6 below · cited by 2 · depth 34
• Untwisting the twisted lift coordinates on a smaller affine open GoodReductionJacobian.BareDeformation.exists_isTangentCoordsOfPairAt_local_lifts_untwist_bare 17 below · cited by 2 · depth 34
• Tangent coordinates of a pair transported through a regluing chart GoodReductionJacobian.BareDeformation.isTangentCoordsOfPairAt_comp_regluing_chart_of_comp_incl_bare 4 below · cited by 3 · depth 34
• Chartwise lift of ψ on sections over the residue field GoodReductionJacobian.BareDeformation.map_app_app_eq_map_app_of_specMap_comp_eq_of_local_lift_factor_bare 0 below · cited by 2 · depth 34
• Obstruction class of a composite endomorphism GoodReductionJacobian.BareDeformation.map_hom_obstruction_cocycle_comp_eq_add_map_tmul_of_local_lifts_bare 35 below · cited by 1 · depth 34
• Additivity of the obstruction class under pointwise product GoodReductionJacobian.BareDeformation.map_hom_obstruction_cocycle_eq_add_of_local_lifts_mul_bare 13 below · cited by 1 · depth 34
• Isomorphic regluings have cohomologous tangent cocycles GoodReductionJacobian.BareDeformation.exists_d_eq_sub_of_isIso_of_isTangentCoordsOfPairAt 20 below · cited by 1 · depth 35
• Obstruction cochain of a composite endomorphism: coboundary identity GoodReductionJacobian.BareDeformation.exists_d_eq_unitPullback_hom_obstruction_cocycle_comp_sub_map_tmul_sub_baseChange_of_local_lifts_factor_bare 33 below · cited by 1 · depth 35
• Formal coordinates on a bare deformation lifting given ones GoodReductionJacobian.BareDeformation.exists_deformation_isFormalCoordinates_liftsCoordinates 18 below · cited by 3 · depth 35
• Re-coordinatising a group law by a strict isomorphism GoodReductionJacobian.BareDeformation.exists_isFormalCoordinates_liftsCoordinates_of_isIso 1 below · cited by 1 · depth 35
• Re-gluing a bare deformation by a tangent 1-cocycle GoodReductionJacobian.BareDeformation.exists_isRegluingBy_isTangentCoordsOfPairAt 144 below · cited by 2 · depth 35
• Kodaira–Spencer linearity for re-glued bare deformations GoodReductionJacobian.BareDeformation.exists_linearMap_pointDerivations_forall_isShiftBy 247 below · cited by 1 · depth 35
• Formal coordinates transfer to the fibre of a bare deformation GoodReductionJacobian.BareDeformation.exists_isFormalCoordinates_map_liftsCoordinates 0 below · cited by 1 · depth 36
• Tangent coordinates comparing a composite lift with a factored lift GoodReductionJacobian.BareDeformation.exists_isTangentCoordsOfPairAt_comp_local_lifts_factor_bare 6 below · cited by 1 · depth 36
• Overlap automorphisms realising a prescribed tangent cochain GoodReductionJacobian.BareDeformation.exists_overlap_iso_isTangentCoordsOfPairAt 6 below · cited by 1 · depth 36
• Triple-overlap identity for the chart automorphisms of a cocycle GoodReductionJacobian.BareDeformation.exists_restrict_comp_eq_of_isTangentCoordsOfPairAt_of_d_eq_zero 18 below · cited by 1 · depth 36
• Re-gluing by c+rc' shifts the formal group by w+rw' GoodReductionJacobian.BareDeformation.isShiftBy_add_smul_of_isRegluingBy_of_isTangentCoordsOfPairAt_add_smul 241 below · cited by 1 · depth 36
• Shift class of a regluing depends only on the Čech class GoodReductionJacobian.BareDeformation.isShiftBy_of_isShiftBy_of_isRegluingBy_of_exists_d_eq_sub 100 below · cited by 2 · depth 36
• Affine combination identity for slices of an overlap automorphism GoodReductionJacobian.BareDeformation.appTop_eq_add_mul_sub_of_slices 2 below · cited by 1 · depth 37
• Cocycle identity for the transitions of a re-gluing GoodReductionJacobian.BareDeformation.exists_cocycle_of_isRegluingBy 1 below · cited by 1 · depth 37
• Base change of a bare deformation with formal coordinates GoodReductionJacobian.BareDeformation.exists_isPullback_isFormalCoordinates_map_of_ringHom_comp_eq 14 below · cited by 1 · depth 37
• Re-gluing commutes with base change along a retraction GoodReductionJacobian.BareDeformation.exists_isRegluingBy_of_isRegluingBy_of_isPullback 0 below · cited by 1 · depth 37
• Isomorphic bare deformations admit a unit-preserving, multiplicative isomorphism GoodReductionJacobian.BareDeformation.exists_iso_one_comp_eq_mapPt_mul_of_isIso 59 below · cited by 2 · depth 37
• Overlap automorphisms over a triple fibre product base GoodReductionJacobian.BareDeformation.exists_overlap_isos_comap_of_sections 11 below · cited by 1 · depth 37
• Transport of formal coordinates along an isomorphism of bare deformations GoodReductionJacobian.BareDeformation.isFormalCoordinates_and_liftsCoordinates_mapPt_inv 0 below · cited by 2 · depth 37
• Strict isomorphism of the formal groups of a bare deformation GoodReductionJacobian.BareDeformation.isIso_of_isFormalCoordinates_of_liftsCoordinates 5 below · cited by 2 · depth 37
• Cohomologous tangent cocycles give isomorphic regluings GoodReductionJacobian.BareDeformation.isIso_of_isRegluingBy_of_exists_d_eq_sub 22 below · cited by 1 · depth 37
• Universal overlap automorphism over a triple fibre product of bases GoodReductionJacobian.BareDeformation.exists_overlap_isos_comap_slice 6 below · cited by 1 · depth 38
• Cocycle identity descends to the base-changed overlap automorphisms GoodReductionJacobian.BareDeformation.overlap_isos_comap_cocycle_of_slice 7 below · cited by 1 · depth 38
• Three slices jointly determine morphisms of pulled-back overlaps GoodReductionJacobian.BareDeformation.eq_of_forall_slice_comp_eq 3 below · cited by 1 · depth 39
• Slice-prescribed endomorphism of a pulled-back overlap GoodReductionJacobian.BareDeformation.exists_endo_comap_inter_of_slices 5 below · cited by 1 · depth 39

GoodReductionJacobian.PartialAction 13

• Rational translation action with a small stable closed subset GoodReductionJacobian.PartialAction.exists_compatible_stable_defined_one_of_not_isProper 54 below · cited by 1 · depth 33
• Pointwise fixed k-point of a partial group action is universally fixed GoodReductionJacobian.PartialAction.exists_defined_act_eq_of_forall_act_eq 7 below · cited by 2 · depth 33
• Isotropy subgroup of a moved point in a low-dimensional stable closed set GoodReductionJacobian.PartialAction.exists_isClosedImmersion_range_ne_univ_of_act_ne 14 below · cited by 1 · depth 33
• Affineness of a group fixing a point of its model GoodReductionJacobian.PartialAction.isAffine_of_forall_exists_defined_act_eq 27 below · cited by 1 · depth 33
• Rosenlicht's modification at a boundary point of codimension one GoodReductionJacobian.PartialAction.exists_closure_image_eq_closure_singleton_of_ringKrullDim_eq_one 43 below · cited by 1 · depth 34
• Stable divisor swept out by a divisor under a partial action GoodReductionJacobian.PartialAction.exists_stable_defined_one_of_closure_image_eq_closure_singleton 11 below · cited by 1 · depth 34
• Rosenlicht's fixed-point criterion for affineness of G GoodReductionJacobian.PartialAction.isAffine_of_forall_act_eq 26 below · cited by 1 · depth 34
• A maximal compatible partial action is a rational action GoodReductionJacobian.PartialAction.unitActs_and_assoc_of_compatible_of_maximal 9 below · cited by 1 · depth 34
• Transported partial action agrees with the lifted one GoodReductionJacobian.PartialAction.base_hom_eq_of_compatible_of_isIso_stalkMap 7 below · cited by 1 · depth 35
• Closure of a partial-action image equals closure of image of generic point GoodReductionJacobian.PartialAction.closure_image_preimage_closure_eq_closure_singleton 0 below · cited by 1 · depth 35
• Infinitesimal point acting trivially on all jets is the unit GoodReductionJacobian.PartialAction.eq_one_of_forall_act_jet_eq_of_subsingleton 6 below · cited by 1 · depth 35
• Jet representations for a partial action fixing a rational point GoodReductionJacobian.PartialAction.exists_generalLinearGroup_jet_of_forall_defined_act_eq 3 below · cited by 1 · depth 35
• Partial action sends boundary points to boundary points GoodReductionJacobian.PartialAction.hom_base_notMem_of_snd_notMem_of_isProper 7 below · cited by 1 · depth 35

GoodReductionJacobian.RelativeGroupLaw 390

• Multiplication by n is epi on the fppf points sheaf GoodReductionJacobian.RelativeGroupLaw.epi_zsmul_of_sectionsEquiv_of_flat_of_surjective 0 below · cited by 2 · depth 12
• Hopf algebra of n-torsion when [n] is finite flat GoodReductionJacobian.RelativeGroupLaw.exists_hopfAlgebra_torsion_of_isFinite_of_flat 2 below · cited by 11 · depth 12
• Lifting ℓ-power torsion of reductions with bounded exponent loss GoodReductionJacobian.RelativeGroupLaw.exists_isTorsionPoint_pow_and_reduction_eq_of_mem_closure_endomorphisms_of_forall_isTorsionPoint 30 below · cited by 1 · depth 12
• Commutative relative group law gives an abelian fppf points sheaf GoodReductionJacobian.RelativeGroupLaw.exists_sheaf_smallFppfTopology_sectionsEquiv_of_isCommutative 1 below · cited by 3 · depth 12
• Multiplication by a unit n on an abelian scheme is finite and flat GoodReductionJacobian.RelativeGroupLaw.isFinite_and_flat_schemeNsmul_of_isUnit 31 below · cited by 13 · depth 12
• Kernel of [n] as a commutative group object GoodReductionJacobian.RelativeGroupLaw.exists_grpObj_schemeKer_eq 0 below · cited by 2 · depth 13
• Finite part of the n-torsion over a henselian local ring GoodReductionJacobian.RelativeGroupLaw.exists_hopfAlgebra_finitePart_schemeKer_of_henselianLocalRing 9 below · cited by 9 · depth 13
• Hopf algebra of n-torsion when [n] is finite flat GoodReductionJacobian.RelativeGroupLaw.exists_hopfAlgebra_torsion_of_isFinite_of_flat_schemeNsmul 2 below · cited by 4 · depth 13
• The n-kernel of a commutative relative group law GoodReductionJacobian.RelativeGroupLaw.exists_relativeGroupLaw_schemeKer_forall_mem_torsionSubset_iff 0 below · cited by 9 · depth 13
• Commutativity passes to the fibre of a relative group law GoodReductionJacobian.RelativeGroupLaw.fibre_mul_comm 0 below · cited by 6 · depth 13
• Multiplication by n commutes with passage to a fibre GoodReductionJacobian.RelativeGroupLaw.fibre_schemeNsmul_eq_schemeFibreEndo 0 below · cited by 12 · depth 13
• Flatness of multiplication by n on an abelian scheme GoodReductionJacobian.RelativeGroupLaw.flat_schemeNsmul_of_isFinite 28 below · cited by 3 · depth 13
• Finite multiplication by n on an abelian scheme is flat GoodReductionJacobian.RelativeGroupLaw.flat_schemeNsmul_of_isFinite_of_abelianSchemePropertyBundle 24 below · cited by 3 · depth 13
• Quasi-finite n-torsion kernels are affine over one-dimensional bases GoodReductionJacobian.RelativeGroupLaw.isAffine_schemeKer_of_locallyQuasiFinite 2 below · cited by 2 · depth 13
• Local quasi-finiteness of the n-torsion kernel over the base GoodReductionJacobian.RelativeGroupLaw.locallyQuasiFinite_schemeKerStr_of_locallyQuasiFinite_schemeNsmul 0 below · cited by 4 · depth 13
• Locally quasi-finite [n] from finite geometric n-torsion GoodReductionJacobian.RelativeGroupLaw.locallyQuasiFinite_schemeNsmul_of_finite_torsionSubset 0 below · cited by 6 · depth 13
• Multiplication by a unit n is locally quasi-finite GoodReductionJacobian.RelativeGroupLaw.locallyQuasiFinite_schemeNsmul_of_isUnit 3 below · cited by 9 · depth 13
• Exponent-m convolution character points give m-torsion sections GoodReductionJacobian.RelativeGroupLaw.nsmul_eq_one_of_forall_withConv_point 1 below · cited by 4 · depth 13
• Fibrewise quasi-finiteness makes [n] flat, surjective, quasi-finite GoodReductionJacobian.RelativeGroupLaw.nsmul_flat_surjective_locallyQuasiFinite_of_forall_locallyQuasiFinite_fibre_schemeNsmul 34 below · cited by 3 · depth 13
• Quasi-compactness of the n-torsion over the base GoodReductionJacobian.RelativeGroupLaw.quasiCompact_schemeKerStr_of_quasiCompact_schemeNsmul 0 below · cited by 4 · depth 13
• Multiplication by n commutes with base change of a relative group law GoodReductionJacobian.RelativeGroupLaw.baseChange_schemeNsmul_comp_fst_and_eq_pullback_map 0 below · cited by 15 · depth 14
• Square-zero deformations with invertible n-torsion are trivial GoodReductionJacobian.RelativeGroupLaw.eq_one_of_sqZero_of_nsmul_eq_one_of_isUnit 0 below · cited by 1 · depth 14
• Homomorphic endomorphism restricts uniquely to the n-torsion kernel GoodReductionJacobian.RelativeGroupLaw.existsUnique_schemeKer_comp_fst_eq_fst_comp_of_hom 0 below · cited by 1 · depth 14
• Functoriality of the coordinate Hopf algebra of relative group laws GoodReductionJacobian.RelativeGroupLaw.exists_bialgHom_of_schemeHomOver_of_forall_mul 0 below · cited by 1 · depth 14
• Coordinate Hopf algebra of an affine flat relative group law GoodReductionJacobian.RelativeGroupLaw.exists_hopfAlgebra_algEquiv_globalSections_of_isAffineHom 1 below · cited by 3 · depth 14
• Common kernel of two morphisms to relative group laws is closed GoodReductionJacobian.RelativeGroupLaw.exists_isClosedImmersion_comp_eq_one_iff 0 below · cited by 2 · depth 14
• Image of an idempotent endomorphism of a commutative relative group law GoodReductionJacobian.RelativeGroupLaw.exists_relativeGroupLaw_image_of_idempotent 0 below · cited by 1 · depth 14
• Hopf points sheaf as a retract of G[n] GoodReductionJacobian.RelativeGroupLaw.exists_retract_kernel_zsmul_hopfPointsSheaf_of_idempotent 7 below · cited by 1 · depth 14
• Iterated base change of a relative group law GoodReductionJacobian.RelativeGroupLaw.exists_schemeHomOver_baseChange_baseChange_iso 0 below · cited by 2 · depth 14
• Fibrewise flatness of multiplication by n GoodReductionJacobian.RelativeGroupLaw.flat_schemeFibreEndo_schemeNsmul 22 below · cited by 2 · depth 14
• Fibrewise flatness criterion for multiplication by n GoodReductionJacobian.RelativeGroupLaw.flat_schemeNsmul_of_fibrewiseFlat 4 below · cited by 1 · depth 14
• Flatness of [n] from flatness on all fibres GoodReductionJacobian.RelativeGroupLaw.flat_schemeNsmul_of_forall_flat_fibre_schemeNsmul 7 below · cited by 2 · depth 14
• Flatness of [n] on a smooth proper group scheme over a field GoodReductionJacobian.RelativeGroupLaw.flat_schemeNsmul_of_isFinite_of_field 19 below · cited by 3 · depth 14
• Flatness of a quasi-finite [n] on a smooth connected group GoodReductionJacobian.RelativeGroupLaw.flat_schemeNsmul_of_locallyQuasiFinite_of_field 18 below · cited by 4 · depth 14
• Formal unramifiedness of [n] via square-zero torsion vanishing GoodReductionJacobian.RelativeGroupLaw.formallyUnramified_schemeNsmul_of_forall_sqZero 0 below · cited by 2 · depth 14
• Locally quasi-finite from locally quasi-finite kernel GoodReductionJacobian.RelativeGroupLaw.locallyQuasiFinite_of_locallyQuasiFinite_kernel 0 below · cited by 5 · depth 14
• Kernel of [n] is locally quasi-finite over a field point where n is invertible GoodReductionJacobian.RelativeGroupLaw.locallyQuasiFinite_pullback_snd_schemeKerStr_of_isUnit 5 below · cited by 8 · depth 14
• Flat multiplication by n on an irreducible group law is surjective GoodReductionJacobian.RelativeGroupLaw.surjective_schemeNsmul_of_flat_of_field 0 below · cited by 9 · depth 14
• Surjectivity of [n] from surjectivity on all fibres GoodReductionJacobian.RelativeGroupLaw.surjective_schemeNsmul_of_forall_surjective_fibre_schemeNsmul 1 below · cited by 4 · depth 14
• Dual-number points of the kernel of Ribet's matrix are constant GoodReductionJacobian.RelativeGroupLaw.dualNumber_eq_comp_of_ker_ribetMatrix 0 below · cited by 1 · depth 15
• Torsion of invertible order injects into the residue fibre GoodReductionJacobian.RelativeGroupLaw.eq_one_of_isTorsionPoint_of_comp_residue_eq 3 below · cited by 6 · depth 15
• Sections of G[n] as points of the kernel scheme GoodReductionJacobian.RelativeGroupLaw.exists_equiv_obj_kernel_zsmul_schemeHomOver_fst_schemeNsmul 1 below · cited by 1 · depth 15
• Hopf points of an affine group law over arbitrary test schemes GoodReductionJacobian.RelativeGroupLaw.exists_equiv_schemeHomOver_withConv_algHom_of_isAffineHom 0 below · cited by 1 · depth 15
• A relative group law comes from a group object GoodReductionJacobian.RelativeGroupLaw.exists_grpObj_eq 0 below · cited by 4 · depth 15
• Joint kernel m-torsion commutes with base change GoodReductionJacobian.RelativeGroupLaw.exists_isPullback_schemeKer_kerPairLaw_baseChange 0 below · cited by 2 · depth 15
• Idempotent image splits off a retract of G[n] GoodReductionJacobian.RelativeGroupLaw.exists_retract_kernel_zsmul_of_idempotent 0 below · cited by 1 · depth 15
• Coordinate ring of the n-torsion kernel is flat of finite type GoodReductionJacobian.RelativeGroupLaw.flat_and_finiteType_of_locallyQuasiFinite_schemeKerStr 2 below · cited by 1 · depth 15
• Multiplication by a unit is formally unramified GoodReductionJacobian.RelativeGroupLaw.formallyUnramified_schemeNsmul_of_isUnit_of_isLocalRing 1 below · cited by 19 · depth 15
• Multiplication by p^k on the (p)-fibre is locally quasi-finite GoodReductionJacobian.RelativeGroupLaw.locallyQuasiFinite_fibre_schemeNsmul_primePow_of_forall_nsmul_eq_one_imp_eq_one 1 below · cited by 1 · depth 15
• Properties of the n-torsion kernel of a relative group law GoodReductionJacobian.RelativeGroupLaw.schemeKerStr_props_of_schemeNsmul 0 below · cited by 3 · depth 15
• Generic-fibre homomorphism property spreads to all points GoodReductionJacobian.RelativeGroupLaw.comp_mul_eq_mul_comp_of_genericFibre 1 below · cited by 8 · depth 16
• Universal injectivity on geometric points makes [n] locally quasi-finite GoodReductionJacobian.RelativeGroupLaw.locallyQuasiFinite_schemeNsmul_of_forall_nsmul_eq_one_imp_eq_one 0 below · cited by 1 · depth 16
• Flatness, surjectivity and quasi-finiteness of [n] over ℤ GoodReductionJacobian.RelativeGroupLaw.nsmul_flat_surjective_locallyQuasiFinite_of_locallyQuasiFinite_primePow 39 below · cited by 1 · depth 16
• Homomorphisms of relative group laws preserve unit and multiples GoodReductionJacobian.RelativeGroupLaw.schemeNsmul_comp_eq_comp_schemeNsmul_of_hom 0 below · cited by 4 · depth 16
• Functoriality of torsion Hopf algebras under homomorphisms of group laws GoodReductionJacobian.RelativeGroupLaw.exists_bialgHom_torsion_of_hom 0 below · cited by 3 · depth 17
• Weil extension via a diagonal difference morphism GoodReductionJacobian.RelativeGroupLaw.exists_extension_of_diagonal_difference_extension 3 below · cited by 5 · depth 17
• Difference map extends over the diagonal (Weil extension, step 1) GoodReductionJacobian.RelativeGroupLaw.exists_opens_diagonal_difference_extension 24 below · cited by 5 · depth 17
• Reduced special fibre of the n-torsion kernel for n invertible GoodReductionJacobian.RelativeGroupLaw.isReduced_pullback_schemeKerStr_residueField_of_isUnit 2 below · cited by 5 · depth 17
• Largest open of definition of the difference map GoodReductionJacobian.RelativeGroupLaw.exists_isGreatest_opens_difference_extension 3 below · cited by 1 · depth 18
• Formal unramifiedness of the n-torsion of a base-changed group law GoodReductionJacobian.RelativeGroupLaw.formallyUnramified_schemeKerStr_baseChange_of_isUnit 2 below · cited by 2 · depth 19
• Lifting torsion points from the residue field to a henselian valuation ring GoodReductionJacobian.RelativeGroupLaw.exists_isTorsionPoint_specMap_residue_comp_eq_of_isAlgClosed 11 below · cited by 3 · depth 20
• Translation by a section is an automorphism over the base GoodReductionJacobian.RelativeGroupLaw.exists_iso_hom_comp_eq_and_comp_hom_eq_mul 0 below · cited by 3 · depth 20
• Relative group law glued from translated charts GoodReductionJacobian.RelativeGroupLaw.exists_relativeGroupLaw_glued_charts_mul_eq 1 below · cited by 1 · depth 20
• Chart index map on A'-points: additive and surjective GoodReductionJacobian.RelativeGroupLaw.exists_spec_glued_charts 1 below · cited by 1 · depth 20
• Translated graph of a non-extending K-point is a closed immersion GoodReductionJacobian.RelativeGroupLaw.isClosedImmersion_lift_fst_mul_of_not_exists_section 10 below · cited by 1 · depth 20
• Multiplication by a unit n is étale on a smooth relative group law GoodReductionJacobian.RelativeGroupLaw.etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension 2 below · cited by 12 · depth 21
• Reduction is bijective on n-torsion over a henselian base GoodReductionJacobian.RelativeGroupLaw.eq_one_of_pow_eq_one_of_reduction_eq_and_exists_pow_eq_one_reduction_eq_of_isUnit_of_henselianLocalRing 9 below · cited by 7 · depth 22
• Difference cocycle from a points-torsor condition GoodReductionJacobian.RelativeGroupLaw.exists_cocycle_forall_comp_eq_specMap_comp_of_forall_existsUnique_conv_eq 0 below · cited by 1 · depth 22
• Čech 1-cocycles along a finite flat local cover are coboundaries GoodReductionJacobian.RelativeGroupLaw.exists_eq_mul_inv_of_cocycle_of_isLocalRing_of_smooth_of_henselianLocalRing 12 below · cited by 1 · depth 22
• Abelian subvariety generated by a set of endomorphisms GoodReductionJacobian.RelativeGroupLaw.exists_isClosedImmersion_range_eq_closure_endomorphisms_of_field 14 below · cited by 1 · depth 22
• Identity component of a group scheme over a field GoodReductionJacobian.RelativeGroupLaw.exists_isOpenImmersion_geometricallyConnected_range_eq_connectedComponent 6 below · cited by 15 · depth 22
• Removing non-identity components of a closed fibre from a group scheme GoodReductionJacobian.RelativeGroupLaw.exists_isOpenImmersion_preimage_range_eq_connectedComponent_of_isClosedImmersion 7 below · cited by 2 · depth 22
• The p-divisible group of an abelian scheme: height 2d GoodReductionJacobian.RelativeGroupLaw.exists_pDivisibleGroup_closedImmersion_isIso_torsion_of_abelianSchemePropertyBundle 734 below · cited by 3 · depth 22
• Schematic closure of a closed subgroup of the generic fibre GoodReductionJacobian.RelativeGroupLaw.exists_relativeGroupLaw_closure_genericFibre_iso_of_isClosedImmersion 2 below · cited by 2 · depth 22
• Closed subfunctor inherits a relative group law; endomorphisms restrict GoodReductionJacobian.RelativeGroupLaw.exists_relativeGroupLaw_comp_eq_mul_and_forall_exists_comp_eq_of_isClosedImmersion 0 below · cited by 2 · depth 22
• Proper group law on the image of a homomorphism GoodReductionJacobian.RelativeGroupLaw.exists_relativeGroupLaw_isProper_image_of_homomorphism_of_isProper 1 below · cited by 1 · depth 22
• Realisable polynomial operators form all of ℤ[Xᵢ] GoodReductionJacobian.RelativeGroupLaw.forall_mvPolynomial_exists_hom_mul_and_pts_smul_eq_comp_of_forall_X 0 below · cited by 1 · depth 22
• Reducedness and smoothness from a factorisation of [m] GoodReductionJacobian.RelativeGroupLaw.isReduced_and_smooth_of_schemeNsmul_eq_comp_of_isReduced_of_isUnit 5 below · cited by 1 · depth 22
• Dual number points over the unit are p-torsion tangent vectors GoodReductionJacobian.RelativeGroupLaw.exists_equiv_algHom_dualNumber_over_counit_schemeHomOver_one_coe_eq_of_torsionSubset_points 1 below · cited by 1 · depth 23
• Identity component of a group scheme over an algebraically closed field GoodReductionJacobian.RelativeGroupLaw.exists_isOpenImmersion_irreducibleSpace_range_eq_connectedComponent_finiteIndex 3 below · cited by 10 · depth 23
• The p-divisible group of a smooth relative group law, scheme-theoretically GoodReductionJacobian.RelativeGroupLaw.exists_pDivisibleGroup_closedImmersion_isIso_torsion_of_smoothOfRelativeDimension 17 below · cited by 1 · depth 23
• Image of a homomorphism is an abelian subvariety GoodReductionJacobian.RelativeGroupLaw.exists_relativeGroupLaw_image_of_homomorphism 1 below · cited by 2 · depth 23
• Relative group law on the image of a homomorphism, after base change GoodReductionJacobian.RelativeGroupLaw.exists_relativeGroupLaw_image_of_homomorphism_baseChange 0 below · cited by 1 · depth 23
• Relative group law on the scheme-theoretic image of a homomorphism GoodReductionJacobian.RelativeGroupLaw.exists_relativeGroupLaw_image_of_homomorphism_of_flat 0 below · cited by 2 · depth 23
• Residue-field point of a representing solution scheme GoodReductionJacobian.RelativeGroupLaw.exists_residueField_point_solutionScheme_of_cocycle 2 below · cited by 1 · depth 23
• Hensel lifting of n-th roots for a smooth relative group law GoodReductionJacobian.RelativeGroupLaw.exists_schemeHomOverComp_eq_and_nsmul_eq_of_henselianLocalRing 5 below · cited by 1 · depth 23
• Smooth group law over a local ring has constant relative dimension GoodReductionJacobian.RelativeGroupLaw.exists_smoothOfRelativeDimension_of_smooth_of_isLocalRing 0 below · cited by 20 · depth 23
• Representability of the coboundary-solution functor inside an affine chart GoodReductionJacobian.RelativeGroupLaw.exists_solutionScheme_existsUnique 4 below · cited by 1 · depth 23
• Multiplication by n on an abelian scheme is finite and flat GoodReductionJacobian.RelativeGroupLaw.isFinite_and_flat_schemeNsmul 714 below · cited by 18 · depth 23
• Proper group law: finite kernel forces finite endomorphism GoodReductionJacobian.RelativeGroupLaw.isFinite_of_isFinite_endKerStr 0 below · cited by 9 · depth 23
• Count of n-torsion points of an abelian variety: n^{2g} GoodReductionJacobian.RelativeGroupLaw.natCard_isTorsionPoint_eq_pow_of_natCast_ne_zero 689 below · cited by 27 · depth 23
• Smoothness of the solution scheme of a cocycle GoodReductionJacobian.RelativeGroupLaw.smooth_of_solutionScheme_of_cocycle 2 below · cited by 1 · depth 23
• Finite flat endomorphisms: surjectivity and degree equals kernel order GoodReductionJacobian.RelativeGroupLaw.surjective_and_endDegree_eq_finrank_of_isFinite_of_flat 0 below · cited by 7 · depth 23
• Degree of [n] on an abelian variety equals n^{2g} GoodReductionJacobian.RelativeGroupLaw.endDegree_nsmul_idPoint_eq_pow_of_natCast_ne_zero 688 below · cited by 4 · depth 24
• Multiplicativity of degree for finite flat endomorphisms GoodReductionJacobian.RelativeGroupLaw.endDegree_schemeHomOverComp_of_isFinite_of_flat 1 below · cited by 5 · depth 24
• Irreducible components through a rational point of a group scheme GoodReductionJacobian.RelativeGroupLaw.eq_of_mem_irreducibleComponents_of_apply_closedPoint_mem 2 below · cited by 2 · depth 24
• Étale kernel of G(π) when dπ=0 GoodReductionJacobian.RelativeGroupLaw.etale_endKerStr_endAeval_of_map_maximalIdeal_le_sq 2 below · cited by 1 · depth 24
• Degree is homogeneous of degree 2g on endomorphisms GoodReductionJacobian.RelativeGroupLaw.exists_isHomogeneous_eval_eq_endDegree_of_abelianSchemePropertyBundle 716 below · cited by 5 · depth 24
• Existence of the p-divisible group J[p^∞] GoodReductionJacobian.RelativeGroupLaw.exists_pDivisibleGroup_point_equiv_torsionSubset_of_isFinite_of_flat 13 below · cited by 1 · depth 24
• Smooth relative dimension d forces p-divisible dimension d GoodReductionJacobian.RelativeGroupLaw.hasDimension_of_point_equiv_torsionSubset_of_smoothOfRelativeDimension 2 below · cited by 1 · depth 24
• Étale kernel of an endomorphism: finiteness and degree GoodReductionJacobian.RelativeGroupLaw.isFinite_endKerStr_and_natCard_eq_endDegree_of_etale 0 below · cited by 10 · depth 24
• Multiplication by n on an abelian scheme is locally quasi-finite GoodReductionJacobian.RelativeGroupLaw.locallyQuasiFinite_schemeNsmul 707 below · cited by 1 · depth 24
• Square-zero deformations of the unit are killed by ℓ GoodReductionJacobian.RelativeGroupLaw.nsmul_eq_one_of_sqZero_of_natCast_eq_zero 0 below · cited by 3 · depth 24
• Multiplication by n is surjective on K-points GoodReductionJacobian.RelativeGroupLaw.nsmul_surjective_of_isAlgClosed_of_connectedSpace 2 below · cited by 17 · depth 24
• A cocycle for a relative group law is trivial on the diagonal GoodReductionJacobian.RelativeGroupLaw.schemeHomOverComp_lift_self_eq_one_of_cocycle 0 below · cited by 2 · depth 24
• Geometrically reduced group law over a field gives smoothness GoodReductionJacobian.RelativeGroupLaw.smooth_of_geometricallyReduced_of_locallyOfFiniteType 0 below · cited by 4 · depth 24
• A symmetric invertible sheaf with positive top Euler coefficient GoodReductionJacobian.RelativeGroupLaw.exists_isInvertible_nonempty_pullback_inv_iso_coeff_pos_forall_eulerChar_tensorPow_eq 666 below · cited by 1 · depth 25
• Degree of αⁿβ is polynomial in n GoodReductionJacobian.RelativeGroupLaw.exists_polynomial_eval_eq_endDegree_zpow_mul_of_abelianSchemePropertyBundle 693 below · cited by 4 · depth 25
• Relative group laws on abelian schemes are commutative GoodReductionJacobian.RelativeGroupLaw.isCommutative_of_abelianSchemePropertyBundle 19 below · cited by 6 · depth 25
• Commutativity of relative group laws on proper geometrically integral schemes GoodReductionJacobian.RelativeGroupLaw.isCommutative_of_isProper_of_geometricallyIntegral 0 below · cited by 10 · depth 25
• Multiplication by n>0 on an abelian variety is locally quasi-finite GoodReductionJacobian.RelativeGroupLaw.locallyQuasiFinite_schemeNsmul_of_field 702 below · cited by 6 · depth 25
• Rigidity: relative group laws with equal unit agree GoodReductionJacobian.RelativeGroupLaw.mul_eq_mul_of_one_eq_of_abelianSchemePropertyBundle 18 below · cited by 7 · depth 25
• Endomorphism degree scales the top Snapper coefficient GoodReductionJacobian.RelativeGroupLaw.coeff_eq_endDegree_mul_coeff_of_forall_eulerChar_tensorPow_eq 668 below · cited by 1 · depth 26
• Closed n-torsion subschemes are étale when n is invertible GoodReductionJacobian.RelativeGroupLaw.etale_of_isClosedImmersion_of_nsmul_eq_one_of_isUnit 6 below · cited by 3 · depth 26
• Spreading out a relative group law to a finite level GoodReductionJacobian.RelativeGroupLaw.exists_intermediateField_forall_exists_relativeGroupLaw_of_isPullback_algebraMap 3 below · cited by 1 · depth 26
• Finite subgroup of k-points as reduced finite closed subscheme GoodReductionJacobian.RelativeGroupLaw.exists_isReduced_isFinite_isClosedImmersion_forall_iff_mem_of_finite_of_isAlgClosed 0 below · cited by 5 · depth 26
• Base change of [n] on a relative group law is cartesian GoodReductionJacobian.RelativeGroupLaw.isPullback_schemeNsmul_baseChange_and_of_isStableUnderBaseChange 1 below · cited by 10 · depth 26
• Multiplication by p is locally quasi-finite in characteristic p GoodReductionJacobian.RelativeGroupLaw.locallyQuasiFinite_schemeNsmul_of_charP 698 below · cited by 1 · depth 26
• Néron–Ogg–Shafarevich: unramified ℓ-power torsion gives an abelian scheme GoodReductionJacobian.RelativeGroupLaw.abelianSchemePropertyBundle_of_neronModelPropertyBundle_of_forall_specMap_comp_eq_self 963 below · cited by 3 · depth 27
• Vanishing degree-g coefficient of χ((γ^*L)^{⊗ m}) for non-isogenies GoodReductionJacobian.RelativeGroupLaw.coeff_eq_zero_of_not_isFinite_endKerStr_of_forall_eulerChar_tensorPow_eq 646 below · cited by 1 · depth 27
• Degree of multiplication by n on an abelian variety is n^{2g} GoodReductionJacobian.RelativeGroupLaw.endDegree_nsmul_idPoint_eq_pow 702 below · cited by 8 · depth 27
• Torsion points are determined by their geometric points GoodReductionJacobian.RelativeGroupLaw.eq_of_nsmulPt_eq_one_of_forall_comp_eq 1 below · cited by 3 · depth 27
• Descent of a homomorphism through a flat surjective quotient GoodReductionJacobian.RelativeGroupLaw.existsUnique_comp_eq_of_forall_mapPt_eq_one_of_flat_of_surjective 1 below · cited by 4 · depth 27
• Homomorphisms killing E factor uniquely through the quotient GoodReductionJacobian.RelativeGroupLaw.existsUnique_quotient_desc_hom_of_isColimit 0 below · cited by 3 · depth 27
• Descending an abelian scheme to a finite level of a directed union GoodReductionJacobian.RelativeGroupLaw.exists_abelianSchemePropertyBundle_isPullback_inf_toSubring_of_directed_iUnion_of_isIso 110 below · cited by 1 · depth 27
• Base change of a p-divisible group inside a relative group law GoodReductionJacobian.RelativeGroupLaw.exists_closedImmersion_isIso_torsion_tensorProduct_baseChange_of_isIso_torsion 0 below · cited by 2 · depth 27
• Constant finite étale subgroup scheme over a discrete valuation ring GoodReductionJacobian.RelativeGroupLaw.exists_group_forall_nonempty_pointsEquiv_of_isFinite_of_etale 2 below · cited by 2 · depth 27
• n-torsion of an abelian scheme is defined over a finite subextension GoodReductionJacobian.RelativeGroupLaw.exists_intermediateField_finiteDimensional_forall_smul_eq_of_mem_torsionBy_of_topologicalKrullDim_eq 696 below · cited by 1 · depth 27
• Néron models over a henselian discrete valuation ring GoodReductionJacobian.RelativeGroupLaw.exists_neronModelPropertyBundle_genericFibre_iso_of_abelianSchemePropertyBundle_of_henselianLocalRing 267 below · cited by 3 · depth 27
• Torsion sections cut out a clopen multisection of A[n] GoodReductionJacobian.RelativeGroupLaw.exists_opens_schemeKer_isClosed_finrank_eq_forall_factorsThrough_iff_of_sections 2 below · cited by 1 · depth 27
• Finite parts of p-power torsion form a p-divisible group GoodReductionJacobian.RelativeGroupLaw.exists_pDivisibleGroup_closedImmersion_finitePart_of_henselianLocalRing 10 below · cited by 1 · depth 27
• Quotient of an abelian scheme by a finite flat subgroup GoodReductionJacobian.RelativeGroupLaw.exists_quotient_abelianSchemePropertyBundle_of_finiteFlat_subgroup 11 below · cited by 2 · depth 27
• Quotient of an abelian scheme by a finite flat subgroup GoodReductionJacobian.RelativeGroupLaw.exists_quotient_abelianSchemePropertyBundle_of_finiteFlat_subgroup_of_affineOrbit_of_commRing 18 below · cited by 1 · depth 27
• Finite kernel on k-points from injectivity on n-torsion GoodReductionJacobian.RelativeGroupLaw.finite_setOf_schemeHomOverComp_eq_one_of_isProper_of_forall_isTorsionPoint 696 below · cited by 1 · depth 27
• Finite sets in an abelian scheme lie in one affine open GoodReductionJacobian.RelativeGroupLaw.forall_finset_exists_isAffineOpen_of_isAlgClosed 8 below · cited by 2 · depth 27
• Closed n-torsion subschemes formally unramified over a local base GoodReductionJacobian.RelativeGroupLaw.formallyUnramified_pullback_snd_of_isClosedImmersion_of_nsmul_eq_one 4 below · cited by 5 · depth 27
• Surjective homomorphism with finite kernel is finite and flat GoodReductionJacobian.RelativeGroupLaw.isFinite_and_flat_of_surjective_of_isFinite_pullback_snd 16 below · cited by 1 · depth 27
• Finite geometric kernels imply u locally quasi-finite GoodReductionJacobian.RelativeGroupLaw.locallyQuasiFinite_of_finite_setOf_schemeHomOverComp_eq_one 0 below · cited by 2 · depth 27
• Order n^{2g} for the n-torsion of A(Ω) GoodReductionJacobian.RelativeGroupLaw.natCard_torsionBy_algPoints_eq_pow_of_topologicalKrullDim_eq 694 below · cited by 15 · depth 27
• Inertia fixes n-torsion points when n is invertible GoodReductionJacobian.RelativeGroupLaw.specMap_comp_eq_self_of_mem_inertiaSubgroupIn_of_isTorsionPoint 3 below · cited by 2 · depth 27
• Formal coordinates separate endomorphisms of a formal group GoodReductionJacobian.RelativeGroupLaw.IsFormalCoordinates.eq_of_forall_apply_nilEval_eq 0 below · cited by 2 · depth 28
• Néron model with proper identity component is an abelian scheme GoodReductionJacobian.RelativeGroupLaw.abelianSchemePropertyBundle_of_neronModelPropertyBundle_of_forall_isProper 111 below · cited by 1 · depth 28
• Quotients of abelian schemes by finite flat subgroup schemes GoodReductionJacobian.RelativeGroupLaw.abelianSchemePropertyBundle_quotient 2 below · cited by 1 · depth 28
• Abelian scheme property passes to a finite flat quotient GoodReductionJacobian.RelativeGroupLaw.abelianSchemePropertyBundle_quotient_of_commRing 9 below · cited by 1 · depth 28
• n-fold multiple of a point factors through [n]_A GoodReductionJacobian.RelativeGroupLaw.coe_nsmul_eq_comp_schemeNsmul 0 below · cited by 11 · depth 28
• Multiplication by p coequalises the kernel pair of Frobenius GoodReductionJacobian.RelativeGroupLaw.comp_schemeNsmul_eq_of_comp_frobenius_eq_of_isCommutative 0 below · cited by 1 · depth 28
• Homomorphisms of complex-uniformised group schemes lift to linear maps GoodReductionJacobian.RelativeGroupLaw.existsUnique_linearMap_forall_pointEquiv_mapPt_eq_of_differentiableOn_appLE 1 below · cited by 1 · depth 28
• Abelian subvariety of finite index in a proper group scheme GoodReductionJacobian.RelativeGroupLaw.exists_abelianSchemePropertyBundle_isClosedImmersion_finiteIndex_of_isProper 6 below · cited by 2 · depth 28
• Endomorphism killing n-torsion is n times an endomorphism GoodReductionJacobian.RelativeGroupLaw.exists_eq_pow_of_forall_isTorsionPoint_schemeHomOverComp_eq_one 33 below · cited by 3 · depth 28
• Commutant of endomorphisms: free ℤ-module of finite rank GoodReductionJacobian.RelativeGroupLaw.exists_existsUnique_eq_prod_zpow_of_forall_comm_of_forall_endDegree_ne_zero 724 below · cited by 1 · depth 28
• Abelian schemes with group law descend to finitely generated subalgebras GoodReductionJacobian.RelativeGroupLaw.exists_fg_subalgebra_abelianSchemePropertyBundle_isPullback_of_isNoetherianRing 108 below · cited by 6 · depth 28
• Group-scheme isomorphisms descend to a finitely generated subalgebra GoodReductionJacobian.RelativeGroupLaw.exists_fg_subalgebra_forall_iso_pullback_of_iso_pullback_of_locallyOfFinitePresentation 5 below · cited by 1 · depth 28
• Finite flat closed subgroup extending generic-fibre N-torsion GoodReductionJacobian.RelativeGroupLaw.exists_finite_flat_closedSubgroupScheme_of_torsion_genericFibre 3 below · cited by 1 · depth 28
• Finite closed subgroup of a relative group law is Spec of a Hopf algebra GoodReductionJacobian.RelativeGroupLaw.exists_hopfAlgebra_iso_of_isClosedImmersion_of_isFinite_of_subgroup 10 below · cited by 2 · depth 28
• Image of a finite reduced subgroup scheme under a finite flat homomorphism GoodReductionJacobian.RelativeGroupLaw.exists_image_closedSubgroup_of_isFinite 4 below · cited by 1 · depth 28
• Counted Serre–Tate lemma: ℓ^{2dv} torsion points on the special fibre GoodReductionJacobian.RelativeGroupLaw.exists_injective_isTorsionPoint_of_neronModelPropertyBundle_of_forall_specMap_comp_eq_self 714 below · cited by 1 · depth 28
• Kernels of multiplication by n commute with base change GoodReductionJacobian.RelativeGroupLaw.exists_isPullback_schemeKerStr_of_isPullback 0 below · cited by 4 · depth 28
• Flat closed torsion subscheme is clopen in A[n] GoodReductionJacobian.RelativeGroupLaw.exists_opens_schemeKer_iso_of_isClosedImmersion_of_nsmulPt_eq_one 1 below · cited by 7 · depth 28
• Descent of a commutative relative group law to a quotient GoodReductionJacobian.RelativeGroupLaw.exists_relativeGroupLaw_quotient_of_isColimit 1 below · cited by 2 · depth 28
• Finite point set with d² d-torsion points is (ℤ/N)² GoodReductionJacobian.RelativeGroupLaw.exists_zmod_prod_equiv_of_natCard_nsmul_eq_one_eq_sq 1 below · cited by 4 · depth 28
• Finite locally free equivalence relation from a finite flat subgroup GoodReductionJacobian.RelativeGroupLaw.finiteLocallyFree_equivalenceRelation_action 0 below · cited by 1 · depth 28
• Finite flat closed subgroup gives finite locally free equivalence relation GoodReductionJacobian.RelativeGroupLaw.finiteLocallyFree_mono_equivalence_actionGroupoid 0 below · cited by 1 · depth 28
• Proper identity component, or O(m²ᵈ⁻¹) geometric m-torsion points GoodReductionJacobian.RelativeGroupLaw.forall_isProper_or_exists_natCard_isTorsionPoint_le_mul_pow 909 below · cited by 1 · depth 28
• Commutativity of a relative group law from its generic fibre GoodReductionJacobian.RelativeGroupLaw.isCommutative_of_isCommutative_genericFibre 1 below · cited by 1 · depth 28
• Surjective endomorphisms have finite kernel scheme GoodReductionJacobian.RelativeGroupLaw.isFinite_endKerStr_of_surjective 8 below · cited by 2 · depth 28
• Multiplication by n on an abelian variety: degree n^{2g} GoodReductionJacobian.RelativeGroupLaw.isFinite_schemeKerStr_and_finrank_eq_pow_and_finrank_schemeNsmul_eq_pow 703 below · cited by 20 · depth 28
• Rank of finite part of n-torsion read on special fibre GoodReductionJacobian.RelativeGroupLaw.isFinite_schemeKerStr_baseChange_and_finrank_eq_finrank_sections_of_isOpenImmersion_of_forall_mem_range 2 below · cited by 2 · depth 28
• Reducedness of ker[n] when [n] is flat and n invertible GoodReductionJacobian.RelativeGroupLaw.isReduced_schemeKer_of_flat_schemeNsmul_of_isUnit 3 below · cited by 2 · depth 28
• Points factoring through a flat model of an N-torsion generic subscheme are N-torsion GoodReductionJacobian.RelativeGroupLaw.nsmul_eq_one_of_factor_of_flat_of_genericFibre_iso 0 below · cited by 1 · depth 28
• Formal coordinates separate tuples of series over B/I GoodReductionJacobian.RelativeGroupLaw.IsFormalCoordinates.funext_of_forall_apply_nilEval_eq_of_constantCoeff_eq_zero 0 below · cited by 9 · depth 29
• Dividing a homomorphism killing n-torsion by [n] GoodReductionJacobian.RelativeGroupLaw.existsUnique_schemeNsmul_comp_eq_of_forall_isTorsionPoint 0 below · cited by 6 · depth 29
• Descent of a relative group law to a finitely generated subalgebra GoodReductionJacobian.RelativeGroupLaw.exists_fg_subalgebra_relativeGroupLaw_pullback_snd_of_locallyOfFinitePresentation 3 below · cited by 4 · depth 29
• Uniform exponent for points killed by a finite-kernel homomorphism GoodReductionJacobian.RelativeGroupLaw.exists_forall_nsmul_eq_one_of_isFinite_pullback_snd 3 below · cited by 2 · depth 29
• Morphisms of relative group laws induce formal group homomorphisms GoodReductionJacobian.RelativeGroupLaw.exists_hom_comp_eq_apply_nilEval_of_isFormalCoordinates 3 below · cited by 5 · depth 29
• Torsion condition on a section cut out by an ideal GoodReductionJacobian.RelativeGroupLaw.exists_ideal_nsmul_eq_one_iff_le_ker 0 below · cited by 2 · depth 29
• Injectivity of reduction on n-torsion at unramified primes GoodReductionJacobian.RelativeGroupLaw.exists_injective_specialize_isTorsionPoint_of_isUnramifiedAt 5 below · cited by 1 · depth 29
• The n-division field is finite Galois with faithful action GoodReductionJacobian.RelativeGroupLaw.exists_isGalois_forall_isTorsionPoint_exists_specMap_comp_eq_and_forall_eq_one 35 below · cited by 1 · depth 29
• Local exponential of a smooth commutative group scheme over ℂ GoodReductionJacobian.RelativeGroupLaw.exists_localExp_differentiableOn_appLE_of_smoothOfRelativeDimension 19 below · cited by 1 · depth 29
• N-torsion points in relative dimension one form (ℤ/N)² GoodReductionJacobian.RelativeGroupLaw.exists_zmod_prod_equiv_nsmulPt_eq_one_of_smoothOfRelativeDimension_one_of_isAlgClosed 698 below · cited by 1 · depth 29
• Full-level locus for n-torsion sections is clopen GoodReductionJacobian.RelativeGroupLaw.isClopen_setOf_finComb_injective_and_forall_torsion_exists 17 below · cited by 2 · depth 29
• Connected commutative group: proper, or m-torsion at most m^{2g-1} GoodReductionJacobian.RelativeGroupLaw.isProper_or_natCard_isTorsionPoint_le_pow_sub_one 908 below · cited by 1 · depth 29
• Surjectivity of multiplication by n on an abelian scheme GoodReductionJacobian.RelativeGroupLaw.surjective_schemeNsmul 718 below · cited by 8 · depth 29
• Rigidity: unit-preserving maps to abelian varieties are homomorphisms GoodReductionJacobian.RelativeGroupLaw.comp_mul_eq_mul_comp_of_comp_one_eq_one_of_abelianSchemePropertyBundle 62 below · cited by 4 · depth 30
• Rigidity over an Artinian local base for group-scheme targets GoodReductionJacobian.RelativeGroupLaw.eq_of_comp_eq_of_isPullback_of_isArtinianRing 4 below · cited by 6 · depth 30
• Rigidity of n-torsion points over a local base GoodReductionJacobian.RelativeGroupLaw.eq_of_isTorsionPoint_of_comp_eq 3 below · cited by 2 · depth 30
• A relative group law is determined by its unit section GoodReductionJacobian.RelativeGroupLaw.eq_of_one_eq_of_abelianSchemePropertyBundle 106 below · cited by 7 · depth 30
• Rigidity: finite-order endomorphism fixing n-torsion, n≥ 3 GoodReductionJacobian.RelativeGroupLaw.eq_schemeHomOverId_of_schemeHomOverNpow_eq_of_forall_isTorsionPoint_of_three_le 717 below · cited by 2 · depth 30
• Holomorphic chart at the identity of a smooth ℂ-group scheme GoodReductionJacobian.RelativeGroupLaw.exists_chart_differentiableOn_mul_of_smoothOfRelativeDimension 15 below · cited by 1 · depth 30
• Hom-scheme of abelian schemes with Hilbert-polynomial pieces GoodReductionJacobian.RelativeGroupLaw.exists_homScheme_represents_hilbertPieces_of_closedImmersionBySections 430 below · cited by 2 · depth 30
• Existence of a Hom scheme for abelian schemes GoodReductionJacobian.RelativeGroupLaw.exists_homScheme_represents_of_closedImmersionBySections_lfp 431 below · cited by 2 · depth 30
• Injectivity of specialisation on n-torsion over a smooth base GoodReductionJacobian.RelativeGroupLaw.exists_injective_specialize_isTorsionPoint_of_smooth 4 below · cited by 1 · depth 30
• Chevalley decomposition of a non-proper commutative group scheme GoodReductionJacobian.RelativeGroupLaw.exists_isAffine_isClosedImmersion_abelianSchemePropertyBundle_of_not_isProper 876 below · cited by 1 · depth 30
• Invariant frame of the top differentials on a smooth group scheme GoodReductionJacobian.RelativeGroupLaw.exists_isFrameOn_topDifferentials_forall_topFormMap_mul_eq 43 below · cited by 1 · depth 30
• Proper integral k-scheme realising ordered products of rational points GoodReductionJacobian.RelativeGroupLaw.exists_isProper_isIntegral_forall_schemeHomOverComp_eq_foldr_of_isAlgClosed 1 below · cited by 1 · depth 30
• Formal group of a smooth commutative relative group law GoodReductionJacobian.RelativeGroupLaw.exists_mvFormalGroup_kernelOfReduction_of_smooth 5 below · cited by 6 · depth 30
• Reduced closed subscheme whose k-points form a subgroup GoodReductionJacobian.RelativeGroupLaw.exists_relativeGroupLaw_comp_eq_mul_of_isReduced_of_isClosedImmersion_of_isAlgClosed 3 below · cited by 1 · depth 30
• Transport of a relative group law along an isomorphism GoodReductionJacobian.RelativeGroupLaw.exists_relativeGroupLaw_mul_comp_hom_eq_of_iso 0 below · cited by 2 · depth 30
• Group law forces constant relative dimension GoodReductionJacobian.RelativeGroupLaw.exists_smoothOfRelativeDimension_of_smooth 3 below · cited by 8 · depth 30
• Torsion bound m^h for connected commutative affine group laws GoodReductionJacobian.RelativeGroupLaw.finite_and_natCard_isTorsionPoint_le_pow_of_isAffine 35 below · cited by 1 · depth 30
• Tensor powers on abelian fibres: h⁰ scales by d^g GoodReductionJacobian.RelativeGroupLaw.geomFibreH0Finrank_tensorPow_eq_pow_mul_of_hom_of_closedImmersionBySections 1,084 below · cited by 1 · depth 30
• Clopen independence locus for n-torsion sections GoodReductionJacobian.RelativeGroupLaw.isClopen_setOf_forall_finComb_injective_of_isUnit 15 below · cited by 1 · depth 30
• Clopenness of the locus where given n-torsion sections span GoodReductionJacobian.RelativeGroupLaw.isClopen_setOf_forall_torsion_exists_finComb_eq_of_isUnit 15 below · cited by 1 · depth 30
• The n-torsion subscheme is finite and flat over the base GoodReductionJacobian.RelativeGroupLaw.isFinite_and_flat_schemeKerStr 715 below · cited by 1 · depth 30
• Infinitesimal points push forward along algebra maps GoodReductionJacobian.RelativeGroupLaw.isInfinitesimal_map_schemeHomOverComp 0 below · cited by 1 · depth 30
• Infinitesimality modulo the nilradical via field-valued points GoodReductionJacobian.RelativeGroupLaw.isInfinitesimal_nilradical_iff_forall_field_schemeHomOverComp_eq_one 0 below · cited by 1 · depth 30
• Proper bijective homomorphism over char-zero field is an isomorphism GoodReductionJacobian.RelativeGroupLaw.isIso_of_isProper_of_bijective_schemeHomOverComp_of_charZero 18 below · cited by 1 · depth 30
• Smooth with n-dimensional fibres and a group law is smooth of relative dimension n GoodReductionJacobian.RelativeGroupLaw.smoothOfRelativeDimension_of_forall_topologicalKrullDim_eq 8 below · cited by 23 · depth 30
• Negation commutes with a homomorphism of relative group laws GoodReductionJacobian.RelativeGroupLaw.comp_negMor_eq_negMor_comp_of_hom 0 below · cited by 11 · depth 31
• Multiplicativity of `endDegree` under composition of isogenies GoodReductionJacobian.RelativeGroupLaw.endDegree_schemeHomOverComp_eq_mul_of_ne_zero 27 below · cited by 3 · depth 31
• Endomorphisms agreeing on all p-power torsion points coincide GoodReductionJacobian.RelativeGroupLaw.eq_of_forall_isTorsionPoint_pow_schemeHomOverComp_eq 701 below · cited by 1 · depth 31
• Uniqueness of lifts of homomorphisms along nilpotent thickenings GoodReductionJacobian.RelativeGroupLaw.eq_of_forall_mul_comp_eq_of_comp_eq_of_isNilpotent_ker 50 below · cited by 6 · depth 31
• Preimage of a connected affine closed subgroup under a smooth surjection GoodReductionJacobian.RelativeGroupLaw.exists_isAffine_isClosedImmersion_of_isAffine_of_comp_eq_one_iff 3 below · cited by 1 · depth 31
• Left-invariant global frame on the top differentials of G/K GoodReductionJacobian.RelativeGroupLaw.exists_isFrameOn_topDifferentials_forall_topFormMap_appLE_mul_eq 41 below · cited by 1 · depth 31
• Translation by a point is an automorphism over the base GoodReductionJacobian.RelativeGroupLaw.exists_iso_hom_comp_eq_one_comp_eq 0 below · cited by 1 · depth 31
• Re-centring a relative group law at a given section GoodReductionJacobian.RelativeGroupLaw.exists_one_eq_of_section 0 below · cited by 3 · depth 31
• Quotient of a smooth group scheme by a smooth normal subgroup GoodReductionJacobian.RelativeGroupLaw.exists_quotient_smoothOfRelativeDimension_sub_of_isClosedImmersion_of_isAlgClosed 61 below · cited by 3 · depth 31
• Points factoring through an open part of A[n] GoodReductionJacobian.RelativeGroupLaw.factorsThrough_opens_schemeKer_iff_nsmulPt_eq_one_and_range_subset 1 below · cited by 2 · depth 31
• Unit-preserving morphisms of abelian schemes are homomorphisms GoodReductionJacobian.RelativeGroupLaw.forall_mul_comp_eq_iff_one_comp_eq_of_abelianSchemePropertyBundle 107 below · cited by 1 · depth 31
• Kernel of [n] is finite flat étale when n∈ R^× GoodReductionJacobian.RelativeGroupLaw.isFinite_flat_etale_schemeKerStr_of_isUnit 34 below · cited by 6 · depth 31
• Properness from absence of positive-dimensional affine subgroups GoodReductionJacobian.RelativeGroupLaw.isProper_of_forall_isAffine_isClosedImmersion_eq_zero 871 below · cited by 1 · depth 31
• Comparison map intertwines group laws with matching unit sections GoodReductionJacobian.RelativeGroupLaw.mul_comp_eq_mul_of_isPullback_of_one_comp_eq 108 below · cited by 1 · depth 31
• Pull-back along [n] of M^{⊗ a}⊗([-1]^*M)^{⊗ b} GoodReductionJacobian.RelativeGroupLaw.nonempty_pullback_schemeNsmul_tensorPow_tensor_tensorPow_iso_monoidalV2 587 below · cited by 1 · depth 31
• Globalising a fibrewise additive holomorphic family of points GoodReductionJacobian.RelativeGroupLaw.relAn_relCov_of_isLocalHom_family_of_differentiableOn_near_zero 23 below · cited by 1 · depth 31
• Rosati compatibility descends from the generic fibre over a DVR GoodReductionJacobian.RelativeGroupLaw.rosatiCompatible_of_rosatiCompatible_generic_of_isDiscreteValuationRing 51 below · cited by 2 · depth 31
• Base-change compatibility of the level-n basis locus GoodReductionJacobian.RelativeGroupLaw.setOf_finComb_injective_and_forall_torsion_exists_baseChange_eq_preimage 0 below · cited by 1 · depth 31
• From chart-level translation identity to invariance at field-valued points GoodReductionJacobian.RelativeGroupLaw.topFormMap_mul_eq_of_forall_topFormMap_appLE_mul_eq 1 below · cited by 1 · depth 31
• Frobenius in formal coordinates: s ↦ s^r GoodReductionJacobian.RelativeGroupLaw.IsFormalCoordinates.val_apply_pow_eq_specMap_frobenius_comp_val_apply 0 below · cited by 2 · depth 32
• Inversion commutes with transition maps between base changes GoodReductionJacobian.RelativeGroupLaw.comp_negMor_eq_negMor_comp_of_compatible 0 below · cited by 10 · depth 32
• Connectedness of the pullback of a connected closed subscheme GoodReductionJacobian.RelativeGroupLaw.connectedSpace_pullback_of_comp_eq_one_iff 0 below · cited by 1 · depth 32
• Néron–Ogg–Shafarevich: unramified ℓ-torsion gives good reduction GoodReductionJacobian.RelativeGroupLaw.exists_abelianSchemePropertyBundle_isPullback_of_forall_specMap_comp_eq_self_of_henselianLocalRing 1,169 below · cited by 1 · depth 32
• Zariski-local exhaustion of n-torsion by finitely many torsion sections GoodReductionJacobian.RelativeGroupLaw.exists_cover_comp_eq_comp_finComb_of_nsmul_eq_one_of_etale 1 below · cited by 1 · depth 32
• Weil extension over a field: extension from a dense open GoodReductionJacobian.RelativeGroupLaw.exists_extension_of_diagonal_difference_extension_of_dense 4 below · cited by 1 · depth 32
• Basis of the n-torsion after a finite étale cover GoodReductionJacobian.RelativeGroupLaw.exists_finite_etale_faithfullyFlat_finComb_basis_of_forall_isAlgClosed 3 below · cited by 1 · depth 32
• Base change of a relative group law along a cartesian square GoodReductionJacobian.RelativeGroupLaw.exists_forall_mul_comp_eq_of_isPullback 0 below · cited by 5 · depth 32
• Existence of the fppf quotient G/N as a scheme GoodReductionJacobian.RelativeGroupLaw.exists_fppf_quotient_isPullback_action_of_isClosedImmersion 40 below · cited by 1 · depth 32
• Finite sets of points of a smooth separated group scheme over a henselian DVR lie in an affine open GoodReductionJacobian.RelativeGroupLaw.exists_isAffineOpen_forall_mem_of_smooth_of_henselianLocalRing 28 below · cited by 1 · depth 32
• Finiteness of the stabiliser of L when χ(L)≠ 0 GoodReductionJacobian.RelativeGroupLaw.exists_isClosedImmersion_isFinite_forall_iff_isInStabilizer_of_eulerChar_ne_zero 891 below · cited by 2 · depth 32
• Rosenlicht decomposition for an abelian subvariety, commutative case GoodReductionJacobian.RelativeGroupLaw.exists_isClosedImmersion_surjective_mul_of_isProper_of_isCommutative 806 below · cited by 1 · depth 32
• Lifting a commutative group law along a small surjection GoodReductionJacobian.RelativeGroupLaw.exists_isCommutative_comp_eq_mul_of_isPullback_of_ker_mul_maximalIdeal_eq_bot 135 below · cited by 2 · depth 32
• Translation by a point trivialises T ×_R G GoodReductionJacobian.RelativeGroupLaw.exists_iso_pullback_hom_fst_eq_and_hom_snd_eq_mul 0 below · cited by 1 · depth 32
• Base change of a relative group law along S→ S'→ S'' GoodReductionJacobian.RelativeGroupLaw.exists_law_baseChange_comp_eq_of_comp_eq 0 below · cited by 2 · depth 32
• Descent of a relative group law with descending unit section GoodReductionJacobian.RelativeGroupLaw.exists_one_eq_of_abelianSchemePropertyBundle_of_isPullback_of_faithfullyFlat 110 below · cited by 4 · depth 32
• Difference map extends across the diagonal (Weil extension, step 1) GoodReductionJacobian.RelativeGroupLaw.exists_opens_diagonal_difference_extension_of_forall_ringKrullDim_le_one 26 below · cited by 1 · depth 32
• Shear isomorphism G×_Q G≅ N×_k G for a quotient homomorphism GoodReductionJacobian.RelativeGroupLaw.exists_pullback_iso_pullback_of_comp_eq_one_iff 0 below · cited by 1 · depth 32
• Relative analytic chart at the unit, with holomorphic multiplication GoodReductionJacobian.RelativeGroupLaw.exists_relChart_one_differentiableOn_mul_of_analyticChart 23 below · cited by 1 · depth 32
• Group law on a quotient by a closed normal subgroup GoodReductionJacobian.RelativeGroupLaw.exists_relativeGroupLaw_quotient_of_isPullback_action_of_surjective 0 below · cited by 1 · depth 32
• Cotangent space of p-torsion in characteristic p has dimension g GoodReductionJacobian.RelativeGroupLaw.finrank_cotangent_ker_counit_eq_of_torsion_points_equiv_of_charP 5 below · cited by 3 · depth 32
• Rosenlicht's dichotomy for non-proper connected group schemes GoodReductionJacobian.RelativeGroupLaw.isAffine_or_exists_isClosedImmersion_lt_of_not_isProper 92 below · cited by 1 · depth 32
• Homomorphism on points is stable under affine base change GoodReductionJacobian.RelativeGroupLaw.isHomOnPoints_baseChange_comp 0 below · cited by 1 · depth 32
• Stabiliser of M^{⊗ j} maps into stabiliser of M under x ↦ x^j GoodReductionJacobian.RelativeGroupLaw.isInStabilizer_pow_of_isInStabilizer_tensorPow_of_abelianSchemePropertyBundle 586 below · cited by 3 · depth 32
• Multiplication and first projection form a cartesian square GoodReductionJacobian.RelativeGroupLaw.isPullback_mul_fst 0 below · cited by 1 · depth 32
• Base change and multiplicativity of the composite e_χ gg φ GoodReductionJacobian.RelativeGroupLaw.liftComp_baseChange_and_isHomOnPoints 0 below · cited by 1 · depth 32
• Uniqueness of a base-changed group law compatible with L GoodReductionJacobian.RelativeGroupLaw.mul_eq_mul_of_compatible_baseChange 0 below · cited by 4 · depth 32
• Mumford's formula for [n]^*L on an abelian scheme GoodReductionJacobian.RelativeGroupLaw.nonempty_pullback_schemeNsmul_iso_tensorPow_tensor_pullback_inv_tensorPow_monoidalV2 585 below · cited by 1 · depth 32
• Base change and homomorphy of monomials prod_l φ_l^{e_l} GoodReductionJacobian.RelativeGroupLaw.prod_zpow_baseChange_and_isHomOnPoints 0 below · cited by 1 · depth 32
• Smoothness and dimension for an effective quotient by a smooth subscheme GoodReductionJacobian.RelativeGroupLaw.smoothOfRelativeDimension_of_isPullback_action_of_surjective 18 below · cited by 1 · depth 32
• Fibre smoothness, irreducibility, dimension and group law along a cartesian square GoodReductionJacobian.RelativeGroupLaw.smooth_irreducibleSpace_geometricFibre_iff_of_isPullback 1 below · cited by 2 · depth 32
• Independence of the geometric point for abelian fibre conditions GoodReductionJacobian.RelativeGroupLaw.smooth_irreducibleSpace_geometricFibre_iff_of_ker_eq_ker 15 below · cited by 1 · depth 32
• Closed subgroup action: shear, freeness, equivalence relation GoodReductionJacobian.RelativeGroupLaw.action_shear_and_equivalence_of_isClosedImmersion 0 below · cited by 1 · depth 33
• Translation composed with a point is multiplication by the constant point GoodReductionJacobian.RelativeGroupLaw.comp_translate_eq_mul 0 below · cited by 3 · depth 33
• Rigidity of two lifts agreeing on reduction and a section GoodReductionJacobian.RelativeGroupLaw.eq_of_comp_eq_of_section_comp_eq_of_ker_mul_maximalIdeal_eq_bot 18 below · cited by 1 · depth 33
• Rigidity of homomorphisms along a nilpotent thickening GoodReductionJacobian.RelativeGroupLaw.eq_of_forall_comp_eq_of_isNilpotent_ker_of_isNoetherianRing 28 below · cited by 4 · depth 33
• Uniqueness of a relative group law compatible with base change GoodReductionJacobian.RelativeGroupLaw.eq_of_forall_mul_comp_fst_eq 0 below · cited by 3 · depth 33
• Translation torsor: [n] : A → A under Spec H GoodReductionJacobian.RelativeGroupLaw.exists_action_isIso_shear_of_torsion_points_equiv 2 below · cited by 2 · depth 33
• Holomorphy of sections at the unit point over an analytic chart GoodReductionJacobian.RelativeGroupLaw.exists_differentiableOn_appLE_one_of_analyticChart 0 below · cited by 1 · depth 33
• Gluing relative group laws along an open cover of the base GoodReductionJacobian.RelativeGroupLaw.exists_forall_mul_eq_of_iSup_eq_top 0 below · cited by 1 · depth 33
• Lifting N^μ times a homomorphism of abelian schemes GoodReductionJacobian.RelativeGroupLaw.exists_hom_comp_eq_comp_schemeNsmul_comp_of_natCast_eq_zero 14 below · cited by 3 · depth 33
• Finite sets lie in affine opens, over a henselian DVR GoodReductionJacobian.RelativeGroupLaw.exists_isAffineOpen_forall_mem_of_isAffineOpen_of_forall_specializes_of_henselianLocalRing 23 below · cited by 1 · depth 33
• Connected smooth closed subgroup of intermediate dimension GoodReductionJacobian.RelativeGroupLaw.exists_isClosedImmersion_connectedSpace_lt_of_range_ne_univ 24 below · cited by 1 · depth 33
• Stabiliser K(L) is a closed subscheme of A GoodReductionJacobian.RelativeGroupLaw.exists_isClosedImmersion_forall_iff_isInStabilizer 97 below · cited by 3 · depth 33
• Smooth irreducible identity component over a perfect field GoodReductionJacobian.RelativeGroupLaw.exists_isClosedImmersion_smoothOfRelativeDimension_range_eq_connectedComponent_of_perfectField 14 below · cited by 5 · depth 33
• Group law lifts along nilpotent thickenings of Artin local bases GoodReductionJacobian.RelativeGroupLaw.exists_isCommutative_comp_eq_mul_of_isPullback_of_isNilpotent_ker_of_isLocalRing 137 below · cited by 2 · depth 33
• Gluing relative group laws along a basic-open cover GoodReductionJacobian.RelativeGroupLaw.exists_isCommutative_forall_mul_comp_eq_of_charts 2 below · cited by 1 · depth 33
• Largest open domain for the difference map into A GoodReductionJacobian.RelativeGroupLaw.exists_isGreatest_opens_difference_extension_of_dense 3 below · cited by 1 · depth 33
• χ-eigen-subdatum of [n]_*mathcal O_A comes from a module sheaf GoodReductionJacobian.RelativeGroupLaw.exists_modules_hom_ofModules_eigenSubdatum_inverse 0 below · cited by 1 · depth 33
• Lifting the multiplication across a small surjection GoodReductionJacobian.RelativeGroupLaw.exists_mul_lift_of_isPullback_of_ker_mul_maximalIdeal_eq_bot 72 below · cited by 1 · depth 33
• Generic fppf quotient on a saturated open of G GoodReductionJacobian.RelativeGroupLaw.exists_opens_saturated_fppf_quotient_of_isClosedImmersion_of_isAlgClosed 35 below · cited by 1 · depth 33
• Faithfully flat descent of a relative group law GoodReductionJacobian.RelativeGroupLaw.exists_relativeGroupLaw_comp_eq_mul_of_isPullback_of_faithfullyFlat 1 below · cited by 2 · depth 33
• Retraction up to isogeny onto an abelian subvariety GoodReductionJacobian.RelativeGroupLaw.exists_schemeHomOverComp_schemeHomOverComp_eq_nsmul_of_isProper_of_isCommutative_of_isAlgClosed 130 below · cited by 1 · depth 33
• Fibre product over the unit section represents the kernel GoodReductionJacobian.RelativeGroupLaw.exists_schemeHomOver_pullback_unit_equiv_ker 0 below · cited by 1 · depth 33
• Saturated opens with fppf quotients exist near every point GoodReductionJacobian.RelativeGroupLaw.forall_exists_opens_saturated_fppf_quotient_of_isAlgClosed 0 below · cited by 1 · depth 33
• Separatedness and quasi-compactness of an fppf quotient GoodReductionJacobian.RelativeGroupLaw.isSeparated_and_quasiCompact_of_isPullback_action_of_surjective 0 below · cited by 1 · depth 33
• Full level structure descends along faithfully flat base change GoodReductionJacobian.RelativeGroupLaw.level_indep_and_span_of_isPullback_of_faithfullyFlat 2 below · cited by 1 · depth 33
• Right multiplication over the identity base equals pr₁ followed by translation GoodReductionJacobian.RelativeGroupLaw.mulRight_id_eq_fst_comp_translate 0 below · cited by 1 · depth 33
• Invariant part of [n]_*𝒪_A is trivial GoodReductionJacobian.RelativeGroupLaw.nonempty_iso_tensorUnit_of_hom_eigenSubdatum_one_of_bijective_smul_eigenOne 2 below · cited by 1 · depth 33
• Multiplication of eigen-parts of [n]_*mathcal O_A gives a tensor isomorphism GoodReductionJacobian.RelativeGroupLaw.nonempty_tensor_iso_of_hom_eigenSubdatum_of_forall_exists_bijective_smul 4 below · cited by 1 · depth 33
• Translation by an n-torsion section commutes with [n] GoodReductionJacobian.RelativeGroupLaw.translate_comp_schemeNsmul_of_mem_torsionSubset 0 below · cited by 5 · depth 33
• Translation by a product is the composite of translations GoodReductionJacobian.RelativeGroupLaw.translate_mul 0 below · cited by 6 · depth 33
• Factoring a homomorphism through a flat surjective quotient of relative group laws GoodReductionJacobian.RelativeGroupLaw.existsUnique_comp_eq_of_forall_ker_of_flat_of_surjective 2 below · cited by 3 · depth 34
• Spec H represents the n-torsion functor on all schemes GoodReductionJacobian.RelativeGroupLaw.existsUnique_comp_eq_of_isTorsionPoint_of_torsion_points_equiv 0 below · cited by 1 · depth 34
• Torsor structure under a scheme representing the n-torsion GoodReductionJacobian.RelativeGroupLaw.exists_action_isIso_shear_of_existsUnique_isTorsionPoint 0 below · cited by 1 · depth 34
• Affine étale slice for translation by a closed subgroup GoodReductionJacobian.RelativeGroupLaw.exists_affine_etale_slice_of_isAlgClosed 10 below · cited by 1 · depth 34
• Chart-wise A[n]-coaction with faithfully flat base and bijective shear GoodReductionJacobian.RelativeGroupLaw.exists_forall_affineOpens_coaction_of_isIso_shear 10 below · cited by 1 · depth 34
• Affine neighbourhood of a finite set from a translated affine open GoodReductionJacobian.RelativeGroupLaw.exists_isAffineOpen_forall_mem_of_forall_mul_mem 6 below · cited by 1 · depth 34
• Closed submonoid of k-points carries a reduced closed subgroup structure GoodReductionJacobian.RelativeGroupLaw.exists_isClosedImmersion_isReduced_range_eq_of_isClosed_of_mul_mem 3 below · cited by 3 · depth 34
• Lifting a commutative group law along a small extension GoodReductionJacobian.RelativeGroupLaw.exists_isCommutative_comp_eq_mul_of_smallExtension 136 below · cited by 1 · depth 34
• Infinitesimal q-power torsion ascends a nilpotent thickening GoodReductionJacobian.RelativeGroupLaw.exists_isNilpotent_isInfinitesimal_of_isPullback_of_isNilpotent_ker 0 below · cited by 3 · depth 34
• n-torsion kernel scheme represented by Spec H GoodReductionJacobian.RelativeGroupLaw.exists_iso_spec_schemeKer_of_forall_equiv_torsionSubset 1 below · cited by 1 · depth 34
• Normalising a lift of a relative group law at the unit section GoodReductionJacobian.RelativeGroupLaw.exists_mul_lift_comp_eq_of_exists_mul_lift 4 below · cited by 2 · depth 34
• A coboundary of the obstruction cocycle lifts the multiplication GoodReductionJacobian.RelativeGroupLaw.exists_mul_lift_of_pointDerivations_coboundary 19 below · cited by 1 · depth 34
• Relative group law from unital associative multiplication morphisms GoodReductionJacobian.RelativeGroupLaw.exists_one_eq_mul_eq_inv_eq_of_comp_eq 0 below · cited by 1 · depth 34
• Open locus of good translators over a discrete valuation ring GoodReductionJacobian.RelativeGroupLaw.exists_opens_forall_mul_base_mem_of_forall_specializes_mem 5 below · cited by 1 · depth 34
• Finite flat orbit relation on a saturated open of an étale slice GoodReductionJacobian.RelativeGroupLaw.exists_opens_saturated_finiteLocallyFree_sliceRelation_of_etale 11 below · cited by 1 · depth 34
• From étale slice quotient to fppf quotient of saturated open GoodReductionJacobian.RelativeGroupLaw.exists_opens_saturated_fppf_quotient_of_sliceQuotient 5 below · cited by 1 · depth 34
• Local lifts of the group law across a nilpotent thickening GoodReductionJacobian.RelativeGroupLaw.exists_orderedAffineCover_lift_mul_of_smooth 3 below · cited by 2 · depth 34
• Obstruction cocycle for local lifts of the group law GoodReductionJacobian.RelativeGroupLaw.exists_pointDerivations_obstruction_cocycle_of_local_lifts 18 below · cited by 1 · depth 34
• Rosenlicht's torsor lemma in functor-of-points form GoodReductionJacobian.RelativeGroupLaw.exists_schemeHomOverComp_act_eq_mul_nsmul_finrank_of_isGalois 1 below · cited by 1 · depth 34
• Rigidity: a relative group law is determined on ̄ K-points GoodReductionJacobian.RelativeGroupLaw.ext_of_forall_algebraicClosure_point_mul_eq 3 below · cited by 1 · depth 34
• Chart inverses agree in Y when multiplications do GoodReductionJacobian.RelativeGroupLaw.inv_comp_eq_inv_comp_of_charts 1 below · cited by 1 · depth 34
• Multiplication by n on an abelian scheme is finite flat GoodReductionJacobian.RelativeGroupLaw.isFinite_flat_schemeKerStr_and_schemeNsmul_of_abelianSchemePropertyBundle 739 below · cited by 4 · depth 34
• Kernel of reduction modulo J^{μ+1}=0 is killed by N^μ GoodReductionJacobian.RelativeGroupLaw.nsmul_pow_eq_one_of_isInfinitesimal_of_smooth 10 below · cited by 1 · depth 34
• Units of two charts agree in Y when multiplications do GoodReductionJacobian.RelativeGroupLaw.one_comp_eq_one_comp_of_charts 0 below · cited by 2 · depth 34
• Principal square roots over a finite product of base rings GoodReductionJacobian.RelativeGroupLaw.principalSqrt_pi_of_forall 11 below · cited by 1 · depth 34
• Formal coordinates of dimension d give relative dimension d GoodReductionJacobian.RelativeGroupLaw.smoothOfRelativeDimension_of_isFormalCoordinates 13 below · cited by 3 · depth 34
• Chartwise coaction is counital and coassociative GoodReductionJacobian.RelativeGroupLaw.coaction_counit_and_coassoc_of_points_formula 3 below · cited by 2 · depth 35
• Inversion morphisms commute with base change of relative group laws GoodReductionJacobian.RelativeGroupLaw.comp_negMor_eq_negMor_comp_of_compatible_univ 0 below · cited by 3 · depth 35
• deg[-1]=1 and inversion as composition with [-1] GoodReductionJacobian.RelativeGroupLaw.endDegree_inv_idPoint_eq_one_and_inv_eq_schemeHomOverComp_inv_idPoint 28 below · cited by 1 · depth 35
• Infinitesimal rigidity of morphisms into an abelian scheme GoodReductionJacobian.RelativeGroupLaw.eq_of_comp_eq_of_section_comp_eq_of_ker_mul_maximalIdeal_eq_bot_anyResidueField 81 below · cited by 1 · depth 35
• Étale, separated, quasi-compact target projection of a slice relation GoodReductionJacobian.RelativeGroupLaw.etale_isSeparated_quasiCompact_pullback_snd_action_slice 0 below · cited by 1 · depth 35
• Unique lifting of homomorphisms across a nilpotent thickening GoodReductionJacobian.RelativeGroupLaw.existsUnique_hom_lift_of_isFormalCoordinates_of_forall_isInfinitesimal 789 below · cited by 2 · depth 35
• Serre–Tate lifting of an isomorphism across a nilpotent thickening GoodReductionJacobian.RelativeGroupLaw.existsUnique_iso_lift_of_isFormalCoordinates_of_forall_isInfinitesimal 790 below · cited by 1 · depth 35
• Affine slice through the unit with formally unramified translation action GoodReductionJacobian.RelativeGroupLaw.exists_affine_formallyUnramified_stalkMap_action_one 6 below · cited by 1 · depth 35
• A point of an étale slice lands in the finite locus GoodReductionJacobian.RelativeGroupLaw.exists_base_mem_of_forall_isFinite_morphismRestrict_le_of_stable 3 below · cited by 1 · depth 35
• Slice restrictions of the obstruction cocycle are coboundaries GoodReductionJacobian.RelativeGroupLaw.exists_d_comap_slice_eq_of_obstruction_cocycle 15 below · cited by 1 · depth 35
• Formal coordinates are stable under base change GoodReductionJacobian.RelativeGroupLaw.exists_isFormalCoordinates_baseChange 0 below · cited by 1 · depth 35
• Re-basing a descended group law through an intermediate ring GoodReductionJacobian.RelativeGroupLaw.exists_isPullback_comp_eq_mul_eq_of_isPullback_of_comp_eq 14 below · cited by 3 · depth 35
• Symmetry of the slice orbit relation GoodReductionJacobian.RelativeGroupLaw.exists_iso_pullback_action_slice_swap 0 below · cited by 2 · depth 35
• Lifting the multiplication across a small extension GoodReductionJacobian.RelativeGroupLaw.exists_mul_lift_of_smallExtension 73 below · cited by 1 · depth 35
• Katz's N^μ-trick on affine points of a smooth group law GoodReductionJacobian.RelativeGroupLaw.exists_natural_forall_eq_nsmul_pow_of_isFormalCoordinates 5 below · cited by 2 · depth 35
• Étaleness of (n,s)↦ i(n) j'(s) spreads to a tube GoodReductionJacobian.RelativeGroupLaw.exists_opens_etale_preimage_snd_action_of_etale_nhds 0 below · cited by 1 · depth 35
• Maximal open of finiteness for a translation-stable slice action GoodReductionJacobian.RelativeGroupLaw.exists_opens_isFinite_morphismRestrict_action_slice_maximal_stable 0 below · cited by 1 · depth 35
• Unit section of a relative group law lies in one affine chart GoodReductionJacobian.RelativeGroupLaw.exists_orderedAffineCover_exists_comp_eq_one 0 below · cited by 1 · depth 35
• Maximal partial action by translation on a proper normal model GoodReductionJacobian.RelativeGroupLaw.exists_partialAction_compatible_maximal_of_isProper 15 below · cited by 1 · depth 35
• Faithful d-dimensional representation implies affineness of G GoodReductionJacobian.RelativeGroupLaw.isAffine_of_smooth_of_forall_generalLinearGroup_eq_one_imp_eq_one 8 below · cited by 1 · depth 35
• Finite kernel and non-zero degree for a factor of [M] GoodReductionJacobian.RelativeGroupLaw.isFinite_endKerStr_and_endDegree_ne_zero_of_hom_of_schemeHomOverComp_eq_nsmul 704 below · cited by 1 · depth 35
• Finiteness and flatness of both legs of an étale slice relation GoodReductionJacobian.RelativeGroupLaw.isFinite_flat_locallyOfFinitePresentation_pullback_action_slice_of_preimage_eq 1 below · cited by 1 · depth 35
• Translation bad locus avoids maximal points of the special fibre GoodReductionJacobian.RelativeGroupLaw.not_mem_closure_image_fst_preimage_mul_compl_of_forall_specializes 4 below · cited by 1 · depth 35
• Rigidity: N^μ kills J-infinitesimal points when N=0 GoodReductionJacobian.RelativeGroupLaw.nsmul_pow_eq_one_of_isInfinitesimal 2 below · cited by 2 · depth 35
• Saturation and finiteness of a slice relation over a stable open GoodReductionJacobian.RelativeGroupLaw.preimage_eq_preimage_and_isFinite_pullback_snd_action_slice_of_stable 0 below · cited by 1 · depth 35
• Joint monomorphy and equivalence for the slice relation over a saturated open GoodReductionJacobian.RelativeGroupLaw.pullback_action_slice_mono_and_equivalence_of_preimage_eq 0 below · cited by 1 · depth 35
• Formal coordinates of dimension d force relative dimension d GoodReductionJacobian.RelativeGroupLaw.smoothOfRelativeDimension_of_isFormalCoordinates_of_field 8 below · cited by 2 · depth 35
• n-divisibility of A(k) for k algebraically closed GoodReductionJacobian.RelativeGroupLaw.AlgPoints.exists_nsmul_eq_of_isAlgClosed 3 below · cited by 1 · depth 36
• Coassociativity of the chart coaction ρ_U GoodReductionJacobian.RelativeGroupLaw.assoc_map_coaction_coaction_eq_map_comul_of_points_formula 1 below · cited by 1 · depth 36
• Uniqueness of the dimension of formal coordinates GoodReductionJacobian.RelativeGroupLaw.eq_of_isFormalCoordinates 1 below · cited by 1 · depth 36
• Local-algebra torsion points factor through an open kernel chart GoodReductionJacobian.RelativeGroupLaw.exists_algHom_spec_map_comp_eq_of_isOpenImmersion_lift_of_isLocalHom 0 below · cited by 1 · depth 36
• Unit-slice restrictions of the obstruction cochain are coboundaries GoodReductionJacobian.RelativeGroupLaw.exists_d_comap_slice_eq_of_isTangentCoordsOfPairAt_slice 12 below · cited by 1 · depth 36
• Change of formal coordinates at the unit section GoodReductionJacobian.RelativeGroupLaw.exists_hom_apply_eq_apply_nilEval_of_isFormalCoordinates 3 below · cited by 2 · depth 36
• Lifting q^{nμ}φ₀ to a homomorphism over B GoodReductionJacobian.RelativeGroupLaw.exists_hom_lift_nsmul_pow_of_isFormalCoordinates 8 below · cited by 1 · depth 36
• Formal coordinates for a smooth commutative relative group law over a local base GoodReductionJacobian.RelativeGroupLaw.exists_isFormalCoordinates_of_isLocalRing 7 below · cited by 2 · depth 36
• Formal germ of a homomorphism into a smooth group scheme GoodReductionJacobian.RelativeGroupLaw.exists_isFormalCoordinates_two_isLawHom_germ_of_abelianSchemePropertyBundle_of_field 22 below · cited by 1 · depth 36
• Coboundary of the tangent cochain lifts the group law GoodReductionJacobian.RelativeGroupLaw.exists_mul_lift_of_pointDerivations_coboundary_anyResidueField 19 below · cited by 1 · depth 36
• Obstruction cocycle for local lifts of the group law GoodReductionJacobian.RelativeGroupLaw.exists_pointDerivations_obstruction_cocycle_of_local_lifts_anyResidueField 18 below · cited by 1 · depth 36
• Product local lifts over T' for A₀×_T A₀ GoodReductionJacobian.RelativeGroupLaw.exists_product_local_lifts_of_local_lifts 10 below · cited by 1 · depth 36
• Product relative group law on A×_R A GoodReductionJacobian.RelativeGroupLaw.exists_relativeGroupLaw_pullback_fst_snd_mul_hom 0 below · cited by 1 · depth 36
• Group law is additive to first order at the unit GoodReductionJacobian.RelativeGroupLaw.germ_mul_sub_fst_sub_snd_mem_maximalIdeal_sq 1 below · cited by 1 · depth 36
• Monomorphic homomorphism with reduced source is a closed immersion GoodReductionJacobian.RelativeGroupLaw.isClosedImmersion_of_mono_of_forall_schemeHomOverComp_mul_eq_of_isAlgClosed 5 below · cited by 1 · depth 36
• Commutativity of the formal group of a commutative relative group law GoodReductionJacobian.RelativeGroupLaw.isComm_of_isFormalCoordinates_of_isCommutative 4 below · cited by 1 · depth 36
• Formal coordinates transported along an isomorphism of formal groups GoodReductionJacobian.RelativeGroupLaw.isFormalCoordinates_comp_adicEval_of_hom 1 below · cited by 2 · depth 36
• Trivial kernel specialises from generic to special fibre over a DVR GoodReductionJacobian.RelativeGroupLaw.kernelTrivial_pullback_special_of_kernelTrivial_generic_of_isDiscreteValuationRing 1,045 below · cited by 1 · depth 36
• Multiplication by m is a homomorphism on T-points GoodReductionJacobian.RelativeGroupLaw.mapPt_schemeNsmul_mul 0 below · cited by 1 · depth 36
• [n] acts as n on an additive presentation of tangent vectors GoodReductionJacobian.RelativeGroupLaw.nsmul_eq_natCast_smul_of_forall_add_eq_mul 0 below · cited by 1 · depth 36
• Point derivations at (e,e) kill μ^sharp a-p₁^sharp a-p₂^sharp a GoodReductionJacobian.RelativeGroupLaw.pointDerivations_apply_mul_sub_fst_sub_snd_eq_zero_of_isAffineOpen 3 below · cited by 1 · depth 36
• Counit identity for the chart coaction ρ_U GoodReductionJacobian.RelativeGroupLaw.rid_map_counit_coaction_eq_of_points_formula 1 below · cited by 1 · depth 36
• Germ ideal of a homomorphism equals ideal of its kernel GoodReductionJacobian.RelativeGroupLaw.span_range_germ_eq_span_range_of_mapPt_eq_one_iff_of_factorsThrough_iff_nilEval_eq_zero 2 below · cited by 1 · depth 36
• Torsion characters as points of the Cartier dual GoodReductionJacobian.RelativeGroupLaw.TorsionCharacter.exists_equiv_algHom_cartierDual_of_torsionSubset_equiv 0 below · cited by 1 · depth 37
• Slice restrictions of the obstruction cocycle are coboundaries GoodReductionJacobian.RelativeGroupLaw.exists_d_comap_slice_eq_of_obstruction_cocycle_anyResidueField 15 below · cited by 1 · depth 37
• Representability of n-torsion by a finite free Hopf algebra GoodReductionJacobian.RelativeGroupLaw.exists_hopfAlgebra_equiv_torsionSubset_of_isLocalRing_of_isNoetherianRing 809 below · cited by 1 · depth 37
• Closed image of a homomorphism of algebraic group schemes GoodReductionJacobian.RelativeGroupLaw.isClosed_range_of_forall_schemeHomOverComp_mul_eq_of_isAlgClosed 1 below · cited by 1 · depth 37
• Point derivations at the unit kill μ^sharp a-p₁^sharp a-p₂^sharp a GoodReductionJacobian.RelativeGroupLaw.pointDerivations_apply_mul_sub_fst_sub_snd_eq_zero 2 below · cited by 1 · depth 37
• Hopf-algebra endomorphism induced on torsion by a group endomorphism GoodReductionJacobian.RelativeGroupLaw.exists_algHom_forall_equiv_comp_eq_comp_of_torsion_points_equiv 0 below · cited by 2 · depth 38
• Restrictions of the obstruction cochain along unit slices are coboundaries GoodReductionJacobian.RelativeGroupLaw.exists_d_comap_slice_eq_of_isTangentCoordsOfPairAt_slice_anyResidueField 12 below · cited by 1 · depth 38
• Equivariance of the chartwise coaction under (φ,φ^sharp) GoodReductionJacobian.RelativeGroupLaw.exists_ringHom_tmul_coaction_eq_coaction_appLE_of_points_formula 1 below · cited by 1 · depth 38
• Multiplication by 2 on an abelian scheme is affine, flat, surjective GoodReductionJacobian.RelativeGroupLaw.isAffineHom_flat_surjective_schemeNsmul_two_of_isFinite_flat_schemeKerStr 715 below · cited by 2 · depth 38
• Symmetry and the square relation under compatible base change GoodReductionJacobian.RelativeGroupLaw.isSymmetric_and_locIsoOnBase_pullback_of_compatible_of_pinned 3 below · cited by 1 · depth 38
• Group schemes in characteristic zero are smooth GoodReductionJacobian.RelativeGroupLaw.smooth_of_charZero 9 below · cited by 1 · depth 38
• Tangent vectors at the unit add under a relative group law GoodReductionJacobian.RelativeGroupLaw.snd_appLE_mul_tangentPoints_eq_add 0 below · cited by 1 · depth 38
• Cartier: group laws in characteristic zero give reduced schemes GoodReductionJacobian.RelativeGroupLaw.isReduced_of_charZero 4 below · cited by 1 · depth 39
• k-points of the stabiliser divide its rank GoodReductionJacobian.RelativeGroupLaw.natCard_setOf_exists_comp_eq_dvd_finrank_of_forall_iff_isInStabilizer 2 below · cited by 1 · depth 39
• Multiplication by n is a torsor under the representing n-torsion scheme GoodReductionJacobian.RelativeGroupLaw.exists_action_isIso_shear_of_existsUnique_isTorsionPoint_of_commRing 0 below · cited by 1 · depth 40
• Relative group law from morphisms m, e, ι GoodReductionJacobian.RelativeGroupLaw.exists_forall_coe_mul_eq_lift_comp_of_forall_lift_comp_eq 0 below · cited by 2 · depth 40
• Sections of a stabiliser subscheme are transitively permuted GoodReductionJacobian.RelativeGroupLaw.exists_iso_hom_comp_eq_of_forall_iff_isInStabilizer 0 below · cited by 1 · depth 40
• Unit section of a separated relative group law is a level-1 structure GoodReductionJacobian.RelativeGroupLaw.isClosedImmersion_one_and_levelOne_axioms_of_isSeparated 0 below · cited by 2 · depth 40
• Homogeneity: reducedness at the unit gives reducedness of G GoodReductionJacobian.RelativeGroupLaw.isReduced_of_isReduced_stalk_one_of_isAlgClosed 0 below · cited by 1 · depth 40
• Reducedness of the stalk at the unit (Cartier) GoodReductionJacobian.RelativeGroupLaw.isReduced_stalk_one_of_charZero 2 below · cited by 1 · depth 40
• The n-torsion kernel scheme represents n-torsion points GoodReductionJacobian.RelativeGroupLaw.isTorsionPoint_fst_schemeKer_and_existsUnique_comp_eq 0 below · cited by 1 · depth 40
• Pinned endomorphism acts by substitution of the series S GoodReductionJacobian.RelativeGroupLaw.apply_apply_mk_eq_apply_mk_subst_of_forall_apply_eq_nilEval 1 below · cited by 1 · depth 41
• Primitivity criterion: additive coboundary modulo the defining ideal GoodReductionJacobian.RelativeGroupLaw.apply_mk_mem_primitives_iff_addCoboundary_mem_of_forall_apply_eq_nilEval 4 below · cited by 1 · depth 41
• Tangent vectors at the unit extend to derivations GoodReductionJacobian.RelativeGroupLaw.forall_exists_sub_algebraMap_mem_and_exists_derivation_stalk_one 0 below · cited by 1 · depth 41
• Two classifiers of the n-torsion agree GoodReductionJacobian.RelativeGroupLaw.exists_algEquiv_forall_coe_equiv_eq_specMap_comp_of_torsion_points_equiv 0 below · cited by 1 · depth 42
• Coordinate ring of the n-torsion is B[[X₁,X₂]]/(φ₁,φ₂) GoodReductionJacobian.RelativeGroupLaw.exists_algEquiv_kerAlgebra_apply_mk_eq_nilEval_of_isFormalCoordinates_of_forall_isInfinitesimal 2 below · cited by 1 · depth 42