All.lean
Nyll.AlgebraicCurves.Geometry.Picard.All
0 declarations indexed from sourceView source ↗
Imports45
- Nyll.AlgebraicCurves.Geometry.Picard.AlgEquivZeroCut
- Nyll.AlgebraicCurves.Geometry.Picard.AlgEquivZeroGroupCut
- Nyll.AlgebraicCurves.Geometry.Picard.BaseChangeFunctor
- Nyll.AlgebraicCurves.Geometry.Picard.CechObstruction
- Nyll.AlgebraicCurves.Geometry.Picard.ChartSections
- Nyll.AlgebraicCurves.Geometry.Picard.Functor
- Nyll.AlgebraicCurves.Geometry.Picard.PolarisationRosati
- Nyll.AlgebraicCurves.Geometry.Picard.PolarisedAbelianScheme
- Nyll.AlgebraicCurves.Geometry.Picard.CommRing_Pic_exists_boundaryHom_conductorSquare_exact
- Nyll.AlgebraicCurves.Geometry.Picard.Exists_twoAffineOpenCover_fibre_linearEquiv_sectionsOf_of_isPullback
- Nyll.AlgebraicCurves.Geometry.Picard.IsAlgEquivZero_eulerChar_sectionsOf_tensor_eq
- Nyll.AlgebraicCurves.Geometry.Picard.IsPullback_baseChangeSnd
- Nyll.AlgebraicCurves.Geometry.Picard.Nonempty_pullback_sectionTwist_iso
- Nyll.AlgebraicCurves.Geometry.Picard.Polarisation_LocIsoOnBase_equivalence
- Nyll.AlgebraicCurves.Geometry.Picard.Polarisation_LocIsoOnBase_pullback_of_comp_eq
- Nyll.AlgebraicCurves.Geometry.Picard.Polarisation_exists_locIsoOnBase_pullback_unit_stage_of_locIsoOnBase_pullback_unit_of_isDirectLimit
- Nyll.AlgebraicCurves.Geometry.Picard.Polarisation_locIsoOnBase_faces_pullback_cube_iff_of_isPullback
- Nyll.AlgebraicCurves.Geometry.Picard.Polarisation_locIsoOnBase_iff_nonempty_iso_of_isLocalRing
- Nyll.AlgebraicCurves.Geometry.Picard.Polarisation_nonempty_iso_of_locIsoOnBase_of_pullback_iso_unit_of_forall_bijective
- Nyll.AlgebraicCurves.Geometry.Picard.RigidifiedLineBundle_exists_iso_map_pullback_rigSection_comp_eq
- Nyll.AlgebraicCurves.Geometry.Picard.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq
- Nyll.AlgebraicCurves.Geometry.Picard.RigidifiedLineBundle_iso_eq_of_map_pullback_rigSection_comp_eq_of_surjective
- Nyll.AlgebraicCurves.Geometry.Picard.RigidifiedLineBundle_nonempty_iso_of_pullbackAlong_openCover_of_bijective_sections
- Nyll.AlgebraicCurves.Geometry.Picard.RigidifiedLineBundle_nonempty_iso_unit_of_forall_pullbackAlong_point
- Nyll.AlgebraicCurves.Geometry.Picard.SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback
- Nyll.AlgebraicCurves.Geometry.Picard.SmallExtension_isPicDeformationCocycle_of_appTop_eq_unitAutSection
- Nyll.AlgebraicCurves.Geometry.Picard.SmallExtension_isPicDeformationCocycle_of_iso
- Nyll.AlgebraicCurves.Geometry.Picard.SmallExtension_isPicDeformationCocycle_unit_pullbackUnitIso_zero
- Nyll.AlgebraicCurves.Geometry.Picard.SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range
- Nyll.AlgebraicCurves.Geometry.Picard.SmallExtension_sub_mem_range_d_of_isPicDeformationCocycle_of_isPicDeformationCocycle
- Nyll.AlgebraicCurves.Geometry.Picard.Subsingleton_H1_and_finrank_H0_fibre_tensor_sectionTwist_of_fibrewiseAlgEquivZero
- Nyll.AlgebraicCurves.Geometry.Picard.Subsingleton_H1_and_finrank_H0_fibre_tensor_sectionTwist_of_fibrewiseAlgEquivZero_of_isAlgClosed
- Nyll.AlgebraicCurves.Geometry.Picard.exists_comp_eq_of_isOpenImmersion_of_abelianSchemePropertyBundle
- Nyll.AlgebraicCurves.Geometry.Picard.isInvertible_sectionIdeal_of_range_subset
- Nyll.AlgebraicCurves.Geometry.Picard.Pullback
- Nyll.AlgebraicCurves.Geometry.Picard.RelSubPic.All
- Nyll.AlgebraicCurves.Geometry.Picard.RelativeGroupLaw
- Nyll.AlgebraicCurves.Geometry.Picard.RelativeGroupLawGrpObj
- Nyll.AlgebraicCurves.Geometry.Picard.StageHom
- Nyll.AlgebraicCurves.Geometry.Picard.SubPicCondition
- Nyll.AlgebraicCurves.Geometry.Picard.Unrigidified
- Nyll.AlgebraicCurves.Geometry.Picard.UnrigidifiedAlgEquivZero
- Nyll.AlgebraicCurves.Geometry.Picard.UnrigidifiedBaseChange
- Nyll.AlgebraicCurves.Geometry.Picard.UnrigidifiedGroup
- Nyll.AlgebraicCurves.Geometry.Picard.UnrigidifiedGroupComparison
Imported by1
This module has no indexed declarations. Its imports and full source are available here.