All.lean
Nyll.JacobianVarieties.Picard.All
0 declarations indexed from sourceView source ↗
Imports353
- Nyll.JacobianVarieties.Picard.ConormAlgebraicPoints
- Nyll.JacobianVarieties.Picard.AbelJacobiDivisionDisplacement
- Nyll.JacobianVarieties.Picard.AlgebraicPointsEquivariance
- Nyll.JacobianVarieties.Picard.DivisionPointDivisors
- Nyll.JacobianVarieties.Picard.AbelJacobiFamily
- Nyll.AlgebraicCurves.Geometry.Picard.AlgEquivZeroCut
- Nyll.AlgebraicCurves.Geometry.Picard.AlgEquivZeroGroupCut
- Nyll.AlgebraicCurves.Geometry.Picard.CechObstruction
- Nyll.AlgebraicCurves.Geometry.Picard.ChartSections
- Nyll.JacobianVarieties.Picard.Designation
- Nyll.JacobianVarieties.Picard.JacobianSchemeData
- Nyll.AlgebraicCurves.Geometry.Picard.Functor
- Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.All
- Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver
- Nyll.JacobianVarieties.Picard.AbelianSchemePropertyBundle_exists_isInvertible_coeff_pos_forall_eulerChar_tensorPow_eq
- Nyll.JacobianVarieties.Picard.AbelianSchemePropertyBundle_exists_isInvertible_finiteBySections
- Nyll.JacobianVarieties.Picard.BaseChange_points_mul_poincare_compat
- Nyll.JacobianVarieties.Picard.CurveModel_exists_representsRelSubPic_abelJacobi_of_isAlgClosed
- Nyll.JacobianVarieties.Picard.CurveModel_finrank_cotangentSpace_zeroSection_eq_genusFF_of_representsRelSubPic
- Nyll.JacobianVarieties.Picard.CurveModel_nonempty_iso_unit_of_eulerChar_sectionsOf_eq_of_ratFunc
- Nyll.JacobianVarieties.Picard.CurveModel_smoothOfRelativeDimension_genusFF_of_representsRelSubPic
- Nyll.JacobianVarieties.Picard.EulerChar_fibre_sectionTwist_tensor_idealModule_eq_one
- Nyll.JacobianVarieties.Picard.Exists_abelJacobi_of_representsRelSubPic
- Nyll.JacobianVarieties.Picard.Exists_chart_subsingleton_H1_fibre
- Nyll.JacobianVarieties.Picard.Exists_finiteBySections_tensorPow_thetaBundle_of_isAlgClosed
- Nyll.JacobianVarieties.Picard.Exists_finite_etale_hasChartSections_of_finiteMapData
- Nyll.JacobianVarieties.Picard.Exists_isAffineOpen_of_representsRelSubPic_algEquivZeroCut_of_finiteMapData
- Nyll.JacobianVarieties.Picard.Exists_isFinite_proj_of_representsRelSubPic_algEquivZeroCut_of_finiteMapData
- Nyll.JacobianVarieties.Picard.Exists_iso_fibre_pullback_fibreModule_tensor_sectionTwist_iso
- Nyll.JacobianVarieties.Picard.Exists_openChart_relSubPicPresheaf_algEquivZeroCut_of_relEffCartierDiv
- Nyll.JacobianVarieties.Picard.Exists_openCharts_relSubPicPresheaf_algEquivZeroCut_of_finiteMapData_of_isReduced
- Nyll.JacobianVarieties.Picard.Exists_opens_range_subset_iff_forall_subsingleton_H1_fibre
- Nyll.JacobianVarieties.Picard.Exists_pic0_equiv_points_abelJacobi_of_curveModel
- Nyll.JacobianVarieties.Picard.Exists_pic0_equiv_points_nontrivial_H0_iff_ell_pos
- Nyll.JacobianVarieties.Picard.Exists_pic0_equiv_points_nontrivial_H0_pullback_iff_ell_pos
- Nyll.JacobianVarieties.Picard.Exists_pic0_equiv_points_of_representsRelSubPic_of_abelJacobi
- Nyll.JacobianVarieties.Picard.Exists_pullbackSection_thetaBundle_eq_zero_iff
- Nyll.JacobianVarieties.Picard.Exists_pullbackSection_thetaBundle_poincare_eq_zero_iff
- Nyll.JacobianVarieties.Picard.Exists_relEffCartierDiv_lineBundle_iso_of_forall_fibre
- Nyll.JacobianVarieties.Picard.Exists_relEffCartierDiv_twistModule_iso_of_subsingleton_H1
- Nyll.JacobianVarieties.Picard.Exists_relativeGroupLaw_abelJacobi_of_representsRelSubPic
- Nyll.JacobianVarieties.Picard.Exists_representsRelSubPic_algEquivZeroCut_of_finiteMapData_of_isReduced
- Nyll.JacobianVarieties.Picard.Exists_representsRelSubPic_algEquivZeroCut_of_isAlgClosed
- Nyll.JacobianVarieties.Picard.Exists_representsRelSubPic_baseChange
- Nyll.JacobianVarieties.Picard.Exists_representsRelSubPic_of_finite_etale_descent_of_finiteMapData
- Nyll.JacobianVarieties.Picard.Exists_shortExact_pushforward_tensor_idealOfSection_of_forall_fibre
- Nyll.JacobianVarieties.Picard.Exists_thetaSection_ne_zero_and_stabilizer_trivial
- Nyll.JacobianVarieties.Picard.Exists_trivialModDeformations_map_H1_tensor_natural
- Nyll.JacobianVarieties.Picard.Exists_twoAffineOpenCover_fibre_finrank_H0_eq_and_finrank_H1_eq
- Nyll.JacobianVarieties.Picard.Exists_twoAffineOpenCover_fibre_finrank_H0_eq_and_subsingleton_H1_iff
- Nyll.JacobianVarieties.Picard.Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField
- Nyll.JacobianVarieties.Picard.FibrewiseAlgEquivZero_ofInvertible_normModule_curveChange
- Nyll.JacobianVarieties.Picard.Finrank_H0_fibre_eq_one_of_subsingleton_H1
- Nyll.JacobianVarieties.Picard.Finrank_H0_unit_fibre_eq_one
- Nyll.JacobianVarieties.Picard.Finrank_H1_unit_fibre_eq_of_eulerChar_chart
- Nyll.JacobianVarieties.Picard.Forall_subsingleton_H1_and_finrank_H0_fibreModule_of_iso
- Nyll.JacobianVarieties.Picard.HasChartSections_forall_geometricFibre_riemannRoch_imp_eq
- Nyll.JacobianVarieties.Picard.IsAlgEquivZero_baseChange
- Nyll.JacobianVarieties.Picard.IsAlgEquivZero_exists_iso_pointsSubBasepointModule
- Nyll.JacobianVarieties.Picard.IsAlgEquivZero_iff_eulerChar_sectionsOf_eq
- Nyll.JacobianVarieties.Picard.IsAlgEquivZero_nonempty_iso_tensorUnit_of_ne_zero
- Nyll.JacobianVarieties.Picard.IsAlgEquivZero_nonempty_pullback_iso_pullback_unit_and_eulerChar_eq_one_of_curveModel_ratFunc
- Nyll.JacobianVarieties.Picard.IsAlgEquivZero_nonempty_pullback_iso_tensorUnit_of_finrank_H1_eq_zero
- Nyll.JacobianVarieties.Picard.IsAlgEquivZero_of_iso_pointSubBasepoint
- Nyll.JacobianVarieties.Picard.IsAlgEquivZero_of_iso_pointsSubBasepoint
- Nyll.JacobianVarieties.Picard.IsAlgEquivZero_pointSubBasepoint
- Nyll.JacobianVarieties.Picard.IsAlgEquivZero_pullback_ofInvertible_of_iso_normModule_morphismRestrict
- Nyll.JacobianVarieties.Picard.IsAlgEquivZero_tensorPow
- Nyll.JacobianVarieties.Picard.IsClosed_setOf_exists_fibreModule_iso_unit
- Nyll.JacobianVarieties.Picard.IsDeformationClassMap_apply_baseTransport_eq_H1baseChangeMap
- Nyll.JacobianVarieties.Picard.IsDeformationClassMap_cechH1ToH1_germ_eq_of_two_covers
- Nyll.JacobianVarieties.Picard.IsDeformationClassMap_exists_cechH1ToH1_germ_eq_traceAlong_of_classifies_normModule_pullback_of_field
- Nyll.JacobianVarieties.Picard.IsDeformationClassMap_exists_cechH1ToH1_germ_eq_traceAlong_of_classifies_normModule_pullback_of_mono
- Nyll.JacobianVarieties.Picard.IsDeformationClassMap_exists_crossSections
- Nyll.JacobianVarieties.Picard.IsDeformationClassMap_injective
- Nyll.JacobianVarieties.Picard.IsDeformationClassMap_map_mul
- Nyll.JacobianVarieties.Picard.IsDeformationClassMap_natural
- Nyll.JacobianVarieties.Picard.IsDeformationClassMap_surjective
- Nyll.JacobianVarieties.Picard.IsFinite_toBase_of_geometricFibre_genus_eq_zero
- Nyll.JacobianVarieties.Picard.IsInvertible_thetaBundle
- Nyll.JacobianVarieties.Picard.IsLFPInj_relPicardPresheaf
- Nyll.JacobianVarieties.Picard.IsLFPInj_relSubPicPresheaf_algEquivZeroCut
- Nyll.JacobianVarieties.Picard.IsLFPSurj_relPicardPresheaf
- Nyll.JacobianVarieties.Picard.IsLFPSurj_relSubPicPresheaf_algEquivZeroCut
- Nyll.JacobianVarieties.Picard.IsLocallyFreeOfRank_pushforward_of_forall_fibre
- Nyll.JacobianVarieties.Picard.IsLocallyFreeOfRank_pushforward_of_forall_fibre_of_finiteType
- Nyll.JacobianVarieties.Picard.IsLocallyFreeOfRank_pushforward_thickening_sectionTwist_and_nonempty_det_iso
- Nyll.JacobianVarieties.Picard.IsOpen_setOf_forall_fibre_subsingleton_H1
- Nyll.JacobianVarieties.Picard.IsOpen_setOf_isAlgEquivZero_fibre
- Nyll.JacobianVarieties.Picard.IsProper_and_geometricallyConnected_of_representsRelSubPic_algEquivZeroCut_of_finiteMapData
- Nyll.JacobianVarieties.Picard.IsPullback_baseChangeSnd_curveChange
- Nyll.JacobianVarieties.Picard.IsSeparated_of_representsRelSubPic_algEquivZeroCut_of_finiteMapData
- Nyll.JacobianVarieties.Picard.IsSheafFor_relSubPicPresheaf_algEquivZeroCut_finiteEtale_of_finiteMapData
- Nyll.JacobianVarieties.Picard.IsSheafFor_relSubPicPresheaf_algEquivZeroCut_finite_faithfullyFlat_of_bijective_sections
- Nyll.JacobianVarieties.Picard.IsSheaf_relSubPicPresheaf_algEquivZeroCut_zariski_of_bijective_sections
- Nyll.JacobianVarieties.Picard.IsSheaf_relSubPicPresheaf_algEquivZeroCut_zariski_of_finiteMapData
- Nyll.JacobianVarieties.Picard.LFP_exists_fg_nonempty_iso_pullbackAlong
- Nyll.JacobianVarieties.Picard.LocallyOfFiniteType_of_representsRelSubPic_algEquivZeroCut_of_finiteMapData
- Nyll.JacobianVarieties.Picard.Nonempty_ajFamily_fibre_iso
- Nyll.JacobianVarieties.Picard.Nonempty_det_pushforward_iso_det_pushforward_tensor_idealOfSection_tensor_pullback
- Nyll.JacobianVarieties.Picard.Nonempty_invModule_prodKerGraph_tensor_module_pow_iso_pointsSubBasepointModule
- Nyll.JacobianVarieties.Picard.Nonempty_iso_tensorUnit_of_fibrewiseAlgEquivZero_of_genus_eq_zero
- Nyll.JacobianVarieties.Picard.Nonempty_pullback_fst_thetaBundle_iso_baseChange
- Nyll.JacobianVarieties.Picard.Nonempty_pullback_sectionIdeal_pow_module_iso
- Nyll.JacobianVarieties.Picard.Nonempty_pullback_thetaBundle_iso
- Nyll.JacobianVarieties.Picard.Nonempty_pushforward_pullback_iso_of_forall_fibre
- Nyll.JacobianVarieties.Picard.Nonempty_thetaBundle_baseChange_iso_thetaBundle_toR
- Nyll.JacobianVarieties.Picard.Nonempty_thetaBundle_iso_of_iso
- Nyll.JacobianVarieties.Picard.Nonempty_thetaBundle_tensor_pointSubBasepoint_tensor_pullback_iso
- Nyll.JacobianVarieties.Picard.Nonempty_thetaBundle_tensor_pointsSubBasepoint_tensor_foldr_pullback_iso
- Nyll.JacobianVarieties.Picard.Nonempty_thetaBundle_tensor_pullbackAlong_tensor_iso_of_fibrewiseAlgEquivZero
- Nyll.JacobianVarieties.Picard.Nonempty_translate_thetaBundle_tensor_iso
- Nyll.JacobianVarieties.Picard.Nonempty_transport_sectionTwist_baseChange_iso
- Nyll.JacobianVarieties.Picard.Pullback_map_counit_app_ne_zero_of_forall_fibre
- Nyll.JacobianVarieties.Picard.RelEffCartierDiv_I_eq_of_lineBundle_iso_tensor_pullback_of_forall_fibre
- Nyll.JacobianVarieties.Picard.RelEffCartierDiv_comap_mapOnProdOver_I_ofPoint_and_mul_prod_pow
- Nyll.JacobianVarieties.Picard.RelEffCartierDiv_eq_of_isAlgEquivZero_of_nonempty_tensor_lineBundle_iso_lineBundle
- Nyll.JacobianVarieties.Picard.RelEffCartierDiv_eq_of_isAlgEquivZero_pullback_mapOnProdOver_of_nonempty_tensor_lineBundle_iso_lineBundle
- Nyll.JacobianVarieties.Picard.RelEffCartierDiv_eq_pullbackAlong_of_twistModule_iso
- Nyll.JacobianVarieties.Picard.RelEffCartierDiv_exists_I_eq_ker_and_pullbackAlong_eq_and_saturated_of_isDiscreteValuationRing
- Nyll.JacobianVarieties.Picard.RelEffCartierDiv_exists_I_eq_of_flat_of_comap_mapOnProdOver_eq_of_isDiscreteValuationRing
- Nyll.JacobianVarieties.Picard.RelEffCartierDiv_exists_nonempty_tensor_lineBundle_iso_lineBundle
- Nyll.JacobianVarieties.Picard.RelEffCartierDiv_forall_exists_comap_pullbackFst_eq_I_and_forall_exists_I_eq_comap_pullbackFst
- Nyll.JacobianVarieties.Picard.RelEffCartierDiv_isAlgEquivZero_twistModule_fibre
- Nyll.JacobianVarieties.Picard.RelEffCartierDiv_isInvertible_I_ofPoint_of_range_subset
- Nyll.JacobianVarieties.Picard.RelEffCartierDiv_isInvertible_I_of_smoothOfRelativeDimension_one
- Nyll.JacobianVarieties.Picard.RelEffCartierDiv_nonempty_pullback_curveChange_ofPoint_comp_lineBundle_iso_and_idealModule_iso_of_isInvertible
- Nyll.JacobianVarieties.Picard.RelativeGroupLaw_coeff_eq_endDegree_mul_coeff_of_forall_eulerChar_tensorPow_eq
- Nyll.JacobianVarieties.Picard.RelativeGroupLaw_coeff_eq_zero_of_not_isFinite_endKerStr_of_forall_eulerChar_tensorPow_eq
- Nyll.JacobianVarieties.Picard.RelativeGroupLaw_endDegree_nsmul_idPoint_eq_pow_of_natCast_ne_zero
- Nyll.JacobianVarieties.Picard.RelativeGroupLaw_exists_isHomogeneous_eval_eq_endDegree_of_abelianSchemePropertyBundle
- Nyll.JacobianVarieties.Picard.RelativeGroupLaw_exists_isInvertible_nonempty_pullback_inv_iso_coeff_pos_forall_eulerChar_tensorPow_eq
- Nyll.JacobianVarieties.Picard.RelativeGroupLaw_exists_polynomial_eval_eq_endDegree_zpow_mul_of_abelianSchemePropertyBundle
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_classifies_rigidify_pullback_map_comp_of_classifies_pullback_curveChange_inv_of_classifies_rigidify_pullback_map
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_classify_tensor
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_comp_mul_eq_mul_comp_of_classifies_rigidify_normModule
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_comp_mul_eq_mul_comp_of_transform
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_deformationClass_kerPoints_bijective_additive_natural
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_eq_one_of_nsmul_pow_eq_one_of_forall_fibre_pow_torsionFree
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_existsUnique_addMonoidHom_pts_comp_fst_eq_comp_of_mul_comp_of_baseChangeIso
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_existsUnique_addMonoidHom_pts_comp_fst_eq_comp_of_semilinear_mul_comp_of_baseChangeIso
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_existsUnique_addMonoidHom_pts_eq_comp_of_mul_comp
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_existsUnique_hom_of_transform
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_exists_hom_classifies_normModule_pullback_and_schemeHomOverComp_eq_of_comp_eq
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_exists_hom_classifies_rigidify_normModule_pullback_curveChange
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_exists_hom_classifies_rigidify_pullback_curveChange
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_exists_hom_classifies_rigidify_pullback_map_of_comp_eq_comp
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_exists_inverse_pair_of_iso_of_sections
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_exists_inverse_pair_of_sections
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_exists_normHom_abelJacobi
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_exists_nsmul_eq_one_not_dvd_of_forall_fibre_exists_pow_eq_one
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_exists_schemeHomOver_poincare_pullbackAlong_iso_ofPoint_lineBundle_tensor_ofPoint_idealModule_of_isLocalRing
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_exists_schemeHomOver_poincare_pullbackAlong_iso_rigidify_pullback_foldr_ofPoint_of_sum_eq_zero
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_flat_mul_fst_snd
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_kerPointsToRigKer_bijective
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_kerPointsToRigKer_mul
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_kerPoints_baseChange_surjective_and_fibre
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_kerPoints_mul_mem_and_comp_mem
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_mul_comp_eq_of_classifies_rigidify_normModule_of_ofPoint
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_mul_comp_eq_of_classifies_rigidify_pullback_of_ofPoint_of_isIso
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_poincare_pullbackAlong_comp_iso_rigidify_normModule_of_range_subset
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_poincare_pullbackAlong_iso_rigidify_normModule_baseChange
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_poincare_pullbackAlong_iso_rigidify_normModule_baseChange_of_forall
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_poincare_pullbackAlong_mul_iso
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_poincare_pullbackAlong_one_iso
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_poincare_pullbackAlong_postComp_iso_pullback_of_rigidify_of_field
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_poincare_pullbackAlong_postComp_pullbackHom_iso_pullback_of_rigidify
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_poincare_pullbackAlong_pow_iso_tensorPow
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_poincare_pullbackAlong_schemeHomOverComp_pullbackHom_iso_rigidify
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_pullbackAlong_mul_iso
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_pullbackAlong_mul_iso_tensor_ofInvertible_norm_pullback_poincare
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_pullbackAlong_one_iso
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_pullback_zeroSection_norm_pullback_poincare_iso_unit_of_mem_of_ringKrullDim_le_one
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_postComp_eq_postComp_of_rigidify_pullback_curveChange_of_transport_of_hom_comp_eq
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_postComp_mul_of_classify_rel
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_postComp_transport_comp_fst_eq_comp_transport_of_baseChangeIso
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_pullbackHom_baseChange_fst
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_pullbackHom_inv_comp_pullbackHom_hom_of_iso
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_relativeGroupLaw_mul_eq_baseChange_mul_of_nonempty_poincare_iso_ofR
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_schemeHomOverComp_eq_one_of_dualNumber_of_classifies_rigidify_normModule_of_finrank_eq_char
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_schemeHomOverComp_mul_eq_mul_and_zeroSection_comp_of_classifies_normModule_pullback
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_schemeHomOverComp_mul_eq_mul_of_forall_postComp_classify_eq
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_schemeHomOverComp_pullbackHom_eq_of_transport_of_hom_comp_eq
- Nyll.JacobianVarieties.Picard.RigKerDualNumber_existsUnique_kerPoint_baseChange_comp_fst_eq
- Nyll.JacobianVarieties.Picard.RigKerDualNumber_exists_isFrameOn_and_map_eq_oneAddEpsMul_smul
- Nyll.JacobianVarieties.Picard.RigKerDualNumber_kerPointsToRigKer_baseTransport
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_descent_finite_faithfullyFlat_of_bijective_sections
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_descent_of_isAffineHom_of_flat_of_surjective_of_bijective_sections
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_fg_subalgebra_isPullback_prodStr_model
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_gluing_openCover_of_bijective_sections
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_isClosedImmersion_chart_iff_affineOpens_of_isNoetherianRing
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_isClosedImmersion_forall_nonempty_pullbackAlong_iso_unit_iff_of_isNoetherianRing
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_isClosedImmersion_iff_of_forall_affineOpens_chart
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_isClosedImmersion_lfp_chart_iff_affineOpens_of_locallyOfFinitePresentation
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_isClosedImmersion_lfp_chart_iff_of_descent
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_isClosedImmersion_lfp_iff_of_forall_affineOpens_chart
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_isClosedImmersion_locallyOfFinitePresentation_forall_iff_of_locallyOfFinitePresentation
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_isNoetherianRing_model_of_fg_subalgebra_model_of_locIsoOnBase_unit_faces
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_isNoetherianRing_model_of_locIsoOnBase_unit_faces
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_noetherian_descent_affineOpens
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_noetherian_descent_affineOpens_of_isPullback_of_isPullback
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_of_squareZero_of_twoAffineOpenCover
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_exists_rigidified_cube_pullback_of_isPullback
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_fibrewiseAlgEquivZero_of_iso_pointsSubBasepointModule
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_fibrewiseAlgEquivZero_of_pullbackAlong_openCover
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_fibrewiseAlgEquivZero_of_pullback_finite_faithfullyFlat
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_nonempty_iso_of_pullback_finite_faithfullyFlat_of_bijective_sections
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_nonempty_iso_of_pullback_of_isAffineHom_of_flat_of_surjective_of_bijective_sections
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_nonempty_iso_unit_iff_forall_openCover
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_nonempty_iso_unit_of_locIsoOnBase_unit_faces
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_nonempty_iso_unit_of_locIsoOnBase_unit_faces_of_isNoetherianRing
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_nonempty_iso_unit_pullback_rigSection_of_squareZero_of_pullback_iso
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_nonempty_ofInvertible_L_iso_of_field
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_nonempty_pullbackAlong_iso_unit_of_smallExtension_of_locIsoOnBase_faces
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_nonempty_pullbackAlong_one_iso_unit_of_locIsoOnBase_face
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_nonempty_pullback_rigSection_pullbackAlong_iso_tensorUnit
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_subsingleton_iso_map_pullback_rigSection_comp_eq
- Nyll.JacobianVarieties.Picard.Scheme_Modules_IsInvertible_nonempty_iso_unit_of_dualNumber_of_reduction
- Nyll.JacobianVarieties.Picard.Scheme_Modules_forall_nonempty_pullback_translate_tensor_iso
- Nyll.JacobianVarieties.Picard.Scheme_Modules_nonempty_iso_tensorUnit_of_pullback_three_slices
- Nyll.JacobianVarieties.Picard.Scheme_Modules_nonempty_iso_tensorUnit_of_pullback_three_slices_of_smoothOfRelativeDimension_one
- Nyll.JacobianVarieties.Picard.Scheme_Modules_nonempty_pullback_mul_mul_tensor_iso
- Nyll.JacobianVarieties.Picard.Scheme_Modules_nonempty_pullback_zpow_iso_tensorPow_of_symmetric
- Nyll.JacobianVarieties.Picard.ShortExact_map_pushforward_thickening
- Nyll.JacobianVarieties.Picard.Smooth_of_representsRelSubPic_algEquivZeroCut_of_finiteMapData
- Nyll.JacobianVarieties.Picard.Subsingleton_H1_and_finrank_H0_fibre_poincare_tensor_sectionTwist
- Nyll.JacobianVarieties.Picard.Subsingleton_H1_and_finrank_H0_fibre_poincare_tensor_sectionTwist_of_isAlgClosed
- Nyll.JacobianVarieties.Picard.Subsingleton_H1_fibre_of_subsingleton_H1_residueField_chart
- Nyll.JacobianVarieties.Picard.Surjective_of_poincare_pullbackAlong_iso_twistModule
- Nyll.JacobianVarieties.Picard.abelJacobi_comp_eq_mul_abelJacobi_of_iso_of_classify
- Nyll.JacobianVarieties.Picard.baseChangeSnd_comp_restrictHom_eq_of_baseChangeSnd_comp
- Nyll.JacobianVarieties.Picard.baseChange_relativeGroupLaw_mul_compat
- Nyll.JacobianVarieties.Picard.comap_sectionIdeal_eq_top_and_finrank_eq_zero_of_forall_notMem_support
- Nyll.JacobianVarieties.Picard.eulerChar_fibre_lineBundle_tensor_idealModule_eq_one_of_supportedIn
- Nyll.JacobianVarieties.Picard.eulerChar_fibre_sectionTwist_tensor_idealModule_eq_one_of_supportedIn
- Nyll.JacobianVarieties.Picard.eulerChar_pullback_fibreModule_tensor_sectionTwist_tensor_idealModule_eq
- Nyll.JacobianVarieties.Picard.eulerChar_pullback_firstLine_sectionTwist_tensor_idealModule_eq
- Nyll.JacobianVarieties.Picard.eulerChar_sectionsOf_pullback_foldr_sectionTwist_tensor_eq_add_sum
- Nyll.JacobianVarieties.Picard.existsUnique_eq_appLE_add_eps_mul_appLE_of_isAffineOpen
- Nyll.JacobianVarieties.Picard.exists_algEquiv_sections_stage_baseChange_of_isAffineOpen
- Nyll.JacobianVarieties.Picard.exists_crossSections_of_isFrameOn_of_map_eq_oneAddEpsMul_smul
- Nyll.JacobianVarieties.Picard.exists_fibreIso_hom_comp_eq
- Nyll.JacobianVarieties.Picard.exists_fibre_eulerChar_eq_and_isClopen_setOf_fibre_eulerChar_eq
- Nyll.JacobianVarieties.Picard.exists_finite_etale_hasChartSections_of_field
- Nyll.JacobianVarieties.Picard.exists_forall_basis_pushforward_dualNumberThickening_of_forall_basis
- Nyll.JacobianVarieties.Picard.exists_forall_finrank_H1_unit_fibreAt_eq_of_finrank_H0_eq_one
- Nyll.JacobianVarieties.Picard.exists_injective_forall_subsingleton_H1_sectionsOf_tensor_of_isAlgEquivZero_of_lt_card
- Nyll.JacobianVarieties.Picard.exists_isAffineOpen_and_isInvertible_sectionIdeal_and_isInvertible_pullbackAlong_and_sectionTwist_of_isOpenImmersion_of_supportedIn
- Nyll.JacobianVarieties.Picard.exists_isDeformationClassMap
- Nyll.JacobianVarieties.Picard.exists_isFrameOn_and_map_eq_oneAddEpsMul_smul_of_nonempty_pullback_iso_unit
- Nyll.JacobianVarieties.Picard.exists_isFrameOn_normModule_and_map_eq_oneAddEpsMul_trace_smul
- Nyll.JacobianVarieties.Picard.exists_openChart_openImmersion_relSubPicPresheaf_algEquivZeroCut_of_fibrewise_zeroScheme
- Nyll.JacobianVarieties.Picard.exists_openChart_openImmersion_relSubPicPresheaf_algEquivZeroCut_of_polarisation_of_fibrewise_zeroScheme
- Nyll.JacobianVarieties.Picard.exists_openCharts_relSubPicPresheaf_algEquivZeroCut_of_polarisation_supportedIn_of_fibrewise_zeroScheme
- Nyll.JacobianVarieties.Picard.exists_openCharts_relSubPicPresheaf_algEquivZeroCut_of_relEffCartierDiv_supportedIn_of_fibrewise_zeroScheme
- Nyll.JacobianVarieties.Picard.exists_opens_range_subset_iff_forall_subsingleton_H1_fibre_of_twoAffineOpenCover
- Nyll.JacobianVarieties.Picard.exists_opens_range_subset_iff_forall_support_zeroSchemeIdeal_subset_of_forall_fibre
- Nyll.JacobianVarieties.Picard.exists_relEffCartierDiv_I_eq_zeroSchemeIdeal_chartModule_fibre_of_smooth
- Nyll.JacobianVarieties.Picard.exists_relEffCartierDiv_lineBundle_iso_of_forall_fibre_of_supportedIn
- Nyll.JacobianVarieties.Picard.exists_relEffCartierDiv_supportedIn_rigidify_iso_of_subsingleton_H1_of_support_subset
- Nyll.JacobianVarieties.Picard.exists_relEffCartierDiv_supportedIn_twistModule_iso_of_subsingleton_H1_of_zeroScheme
- Nyll.JacobianVarieties.Picard.exists_relJacobian_of_smoothOfRelativeDimension_one
- Nyll.JacobianVarieties.Picard.exists_relJacobian_of_smoothOfRelativeDimension_one_of_finiteMapData
- Nyll.JacobianVarieties.Picard.exists_representsRelSubPic_algEquivZeroCut_of_chartData
- Nyll.JacobianVarieties.Picard.exists_representsRelSubPic_algEquivZeroCut_of_finiteMapData_of_isDiscreteValuationRing
- Nyll.JacobianVarieties.Picard.exists_representsRelSubPic_algEquivZeroCut_of_forall_prime_exists_localizationAway
- Nyll.JacobianVarieties.Picard.exists_representsRelSubPic_algEquivZeroCut_of_openCharts_of_bijective_sections
- Nyll.JacobianVarieties.Picard.exists_representsRelSubPic_of_finite_etale_descent_of_bijective_sections_of_forall_orbit
- Nyll.JacobianVarieties.Picard.exists_twoSidedChartData
- Nyll.JacobianVarieties.Picard.exists_twoSidedPool_of_oneSided_of_iso
- Nyll.JacobianVarieties.Picard.fibrewiseAlgEquivZero_of_isAlgEquivZero_pullback_closedFibre_of_pullbackAlong_iso_tensorPow_poincare
- Nyll.JacobianVarieties.Picard.finrank_H0_fibre_eq_one_of_subsingleton_H1_of_supportedIn
- Nyll.JacobianVarieties.Picard.finrank_H0_fibre_eq_one_of_subsingleton_H1_of_supportedIn_lineBundle
- Nyll.JacobianVarieties.Picard.finrank_H0_unit_fibreAt_eq_one_of_bijective_algebraMap
- Nyll.JacobianVarieties.Picard.forall_exists_twoAffineOpenCover_linearEquiv_sectionsOf_fibreModule
- Nyll.JacobianVarieties.Picard.geometricallyConnected_of_representsRelSubPic_algEquivZeroCut
- Nyll.JacobianVarieties.Picard.isAlgEquivZero_fibre_of_range_subset_singleton_of_smooth
- Nyll.JacobianVarieties.Picard.isAlgEquivZero_foldr_ofPoint_of_sum_filter_eq_zero
- Nyll.JacobianVarieties.Picard.isAlgEquivZero_tensor_of_pullback_baseChangeSnd_iso_of_tensor_iso_unit
- Nyll.JacobianVarieties.Picard.isClosed_setOf_exists_fibreModule_iso_unit_of_flat
- Nyll.JacobianVarieties.Picard.isClosed_setOf_forall_fibre_le_finrank_H0_of_twoAffineOpenCover
- Nyll.JacobianVarieties.Picard.isClosed_setOf_forall_fibre_le_finrank_H1_of_twoAffineOpenCover
- Nyll.JacobianVarieties.Picard.isFinite_and_finrank_subscheme_comap_sectionIdeal_pow_and_comap_I
- Nyll.JacobianVarieties.Picard.isInvertible_and_nonempty_pullback_iso_foldr_sectionTwist_tensor_of_range_subset
- Nyll.JacobianVarieties.Picard.isInvertible_comap_sectionIdeal_and_finrank_eq_one_of_ideal_eq_bot
- Nyll.JacobianVarieties.Picard.isInvertible_comap_sectionIdeal_pow_and_comap_I_of_isOpenImmersion
- Nyll.JacobianVarieties.Picard.isIso_baseChangeHom_pushforward_of_forall_fibre_of_twoAffineOpenCover
- Nyll.JacobianVarieties.Picard.isLFPInj_relSubPicPresheaf_algEquivZeroCut_of_twoAffineOpenCover
- Nyll.JacobianVarieties.Picard.isLFPSurj_relSubPicPresheaf_algEquivZeroCut_of_isOpen_setOf_isAlgEquivZero
- Nyll.JacobianVarieties.Picard.isLocallyFreeOfRank_pushforward_of_forall_fibre_of_finiteType_of_twoAffineOpenCover
- Nyll.JacobianVarieties.Picard.isLocallyFreeOfRank_pushforward_of_forall_fibre_of_twoAffineOpenCover
- Nyll.JacobianVarieties.Picard.isOpen_setOf_forall_fibre_subsingleton_H1_of_twoAffineOpenCover
- Nyll.JacobianVarieties.Picard.isOpen_setOf_isAlgEquivZero_fibre_of_twoStrata
- Nyll.JacobianVarieties.Picard.isProper_and_geometricallyConnected_baseChange_toBase_of_representsRelSubPic_of_field
- Nyll.JacobianVarieties.Picard.isSeparated_of_representsRelSubPic_algEquivZeroCut_of_bijective_sections
- Nyll.JacobianVarieties.Picard.map01_oneAddEpsMul
- Nyll.JacobianVarieties.Picard.nonempty_normModule_curveChange_dualNumber_iso_unit_of_finrank_eq_char_of_forall_isClosed_eq
- Nyll.JacobianVarieties.Picard.nonempty_poincare_pullbackAlong_iso_lineBundle_tensor_idealModule_of_abelJacobi_baseChange
- Nyll.JacobianVarieties.Picard.nonempty_pullback_fibreModule_tensor_sectionTwist_tensor_idealModule_iso_of_supportedIn_of_disjoint
- Nyll.JacobianVarieties.Picard.nonempty_pullback_iso_pullback_unit_of_isAlgEquivZero_baseChange_of_curveModel_ratFunc
- Nyll.JacobianVarieties.Picard.nonempty_pullback_sectionIdeal_pow_module_iso_of_smoothLocus
- Nyll.JacobianVarieties.Picard.nonempty_pullback_sectionTwist_iso_of_range_subset
- Nyll.JacobianVarieties.Picard.preimage_range_subset_connectedComponentIn_fibre_baseChange
- Nyll.JacobianVarieties.Picard.preimage_range_subset_diff_connectedComponentIn_fibre_baseChange_of_not_smooth
- Nyll.JacobianVarieties.Picard.pullbackHom_points_eq_pic0_congr_of_iso
- Nyll.JacobianVarieties.Picard.pullback_map_counit_app_ne_zero_of_forall_fibre_of_twoAffineOpenCover
- Nyll.JacobianVarieties.Picard.relEffCartierDiv_I_eq_of_lineBundle_iso_tensor_pullback_of_supportedIn
- Nyll.JacobianVarieties.Picard.relEffCartierDiv_eq_pullbackAlong_of_rigidify_iso_of_supportedIn_of_support_subset
- Nyll.JacobianVarieties.Picard.relEffCartierDiv_eq_pullbackAlong_of_twistModule_iso_of_supportedIn_of_zeroScheme
- Nyll.JacobianVarieties.Picard.relativeGroupLaw_baseChange_eq
- Nyll.JacobianVarieties.Picard.schemeHomOver_ext_of_forall_algebraicClosure_point
- Nyll.JacobianVarieties.Picard.schemeHomOver_ext_of_forall_algebraicClosure_point_of_isReduced
- Nyll.JacobianVarieties.Picard.smooth_of_representsRelSubPic_algEquivZeroCut_of_twoAffineOpenCover
- Nyll.JacobianVarieties.Picard.subsingleton_H1_fibre_of_subsingleton_H1_fibre_extension
- Nyll.JacobianVarieties.Picard.support_zeroSchemeIdeal_fibre_subset_of_support_zeroSchemeIdeal_fibre_subset_extension
- Nyll.JacobianVarieties.Picard.surjective_toBase_of_representsRelSubPic_algEquivZeroCut
- Nyll.AlgebraicCurves.Geometry.Picard.Pullback
- Nyll.AlgebraicCurves.Geometry.Picard.RelSubPic.All
- Nyll.AlgebraicCurves.Geometry.Picard.RelativeGroupLaw
- Nyll.AlgebraicCurves.Geometry.Picard.RelativeGroupLawGrpObj
- Nyll.JacobianVarieties.Picard.Representation
- Nyll.AlgebraicCurves.Geometry.Picard.StageHom
- Nyll.JacobianVarieties.Picard.ThetaBundle
- Nyll.JacobianVarieties.Picard.PicDualNumberDeformationClassSpec
- Nyll.JacobianVarieties.Picard.RelSubPicGlue
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPicPullback
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPicPresheaf
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPicGroup
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPicBaseChange
- Nyll.JacobianVarieties.Picard.RepresentsRelSubPicKerPoints
- Nyll.JacobianVarieties.Picard.Existence
- Nyll.JacobianVarieties.Picard.RelativeDimension
- Nyll.JacobianVarieties.Picard.RigidifiedLineBundleTwistCoherence
- Nyll.JacobianVarieties.Picard.CurveSectionComparisonCoherence
- Nyll.JacobianVarieties.Picard.GenusDimension
- Nyll.JacobianVarieties.Picard.SectionComparisonBaseChange
- Nyll.JacobianVarieties.Picard.UnpointedAbelJacobi
- Nyll.JacobianVarieties.Picard.UnpointedComparisonHom
- Nyll.JacobianVarieties.Picard.UnpointedDescent
- Nyll.JacobianVarieties.Picard.UnpointedDimension
- Nyll.JacobianVarieties.Picard.UnpointedExistence
- Nyll.JacobianVarieties.Picard.UnpointedGroup
- Nyll.JacobianVarieties.Picard.UnpointedJacobian
- Nyll.JacobianVarieties.Picard.UnpointedPointedComparison
- Nyll.JacobianVarieties.Picard.UnpointedPointedGroup
- Nyll.JacobianVarieties.Picard.ChartSectionsBaseChange
- Nyll.JacobianVarieties.Picard.SeparableChartSections
- Nyll.JacobianVarieties.Picard.AbelJacobiPointClassBaseChange
- Nyll.JacobianVarieties.Picard.UnpointedAlbanese
- Nyll.JacobianVarieties.Picard.TorsionAlgebraicPoints
- Nyll.JacobianVarieties.Picard.ConstantExtensionFixedDivisors
- Nyll.JacobianVarieties.Picard.CurveModelDivisibility
- Nyll.JacobianVarieties.Picard.TorsionCardinality
Imported by1
This module has no indexed declarations. Its imports and full source are available here.