AlgebraicGeometry.RelPicard.exists_openCharts_relSubPicPresheaf_algEquivZeroCut_of_finiteMapData_of_isReduced
Source context 38 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.OpenPicardCharts
attribute [-instance]
AlgebraicGeometry.FGSubalgebra.instIsDirectedLe
attribute [-instance]
instQuasiSeparatedSpaceCarrierCarrierCommRingCatObjOppositeSchemeSpecDiagram
attribute [-instance]
AlgebraicGeometry.FGSubalgebra.instIsCofilteredOpposite
AlgebraicGeometry.FGSubalgebra.instIsAffineObjOppositeSchemeSpecDiagram
AlgebraicGeometry.FGSubalgebra.instNonempty
AlgebraicGeometry.FGSubalgebra.instNonemptySubtypeLeSubalgebraValFG
attribute [-instance]
instCompactSpaceCarrierCarrierCommRingCatObjOppositeSchemeSpecDiagram
attribute [-instance]
AlgebraicGeometry.FGSubalgebra.instIsDirectedSubtypeLeSubalgebraValFG
AlgebraicGeometry.FGSubalgebra.instIsAffineHomMapOppositeSchemeSpecDiagram
AlgebraicGeometry.FGSubalgebra.instIsFiltered
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instNeg
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulInt
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAddCommGroup
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAdd
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSub
attribute [-instance]
instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
attribute [-instance]
instSMulCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
attribute [-instance]
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulNat
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instZero
AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
AlgebraicGeometry.Scheme.Modules.pullback_monoidal
AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
PresheafOfModules.PullbackMonoidal.pullback_monoidal PresheafOfModules.PullbackMonoidal.isIso_δ
PresheafOfModules.pushforward_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_η
PresheafOfModules.free_monoidal PresheafOfModules.restrictScalars_laxMonoidal
PresheafOfModules.PullbackMonoidal.isIso_δ_gS PresheafOfModules.pullback_oplaxMonoidal
attribute [-instance]
instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
attribute [-instance]
PresheafOfModules.pullback_monoidal' AlgebraicCurve.IsCurveOver.instNontrivialKaehler
AlgebraicCurve.IsCurveOver.instFreeKaehler AlgebraicCurve.IsCurveOver.toHasPrincipalDivisors
AlgebraicCurve.IsCurveOver.instFiniteResidue
attribute [-instance]
AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
AlgebraicCurve.Place.instIsLocalHomRestrictInclusion AlgebraicCurve.Place.instIsPrimeCenter
AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
AlgebraicCurve.SemilinearAut.instDistribMulActionSubtypeProdRingAutMemSubgroupPic0
AlgebraicCurve.SemilinearAut.instDistribMulActionSubtypeProdRingAutMemSubgroupDivisor
AlgebraicCurve.Pic0.instModuleZModTorsion
AlgebraicCurve.SemilinearAut.instSMulSubtypeProdRingAutMemSubgroupPlace
AlgebraicCurve.SemilinearAut.instDistribMulActionTorsion
AlgebraicCurve.SemilinearAut.instSMulSubtypeProdRingAutMemSubgroupPic0
AlgebraicCurve.SemilinearAut.instSMulTorsion
AlgebraicCurve.SemilinearAut.instMulActionSubtypeProdRingAutMemSubgroupPlace
AlgebraicCurve.SemilinearAut.instSMulCommClassZModTorsion
AlgebraicCurve.SemilinearAut.instMulSemiringActionSubtypeProdRingAutMemSubgroup
AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
AlgebraicCurve.instHasLocalResidue_of_hasCanonicalLocalResidueK
AlgebraicCurve.instHasCanonicalLocalResidueK_of_hasCanonicalLocalResidueKStar
AlgebraicCurve.Place.kw_ffgc_finiteDimensional_adicCompletion
AlgebraicCurve.Place.kw_ffgc_isScalarTower_integersIntegersCompletion
ModularCurve.KwF4gRRTate.instAlgebraKAdicCompletionIntegers
AlgebraicCurve.Place.kw_ffgc_continuousSMul_adicCompletionComap
AlgebraicCurve.Place.kw_ffgc_isScalarTower_integersCompletionCompletion
attribute [-instance]
instLiesOverSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegersCompletionIdealAsIdeal
attribute [-instance]
AlgebraicCurve.instHasCanonicalLocalResidueK AlgebraicCurve.Place.instAlgebra_restrictResidueField
AlgebraicCurve.Place.instIsScalarTower_restrictResidueField AlgebraicCurve.instHasLocalResidue
AlgebraicCurve.HasSeparableResidue.of_perfectField_of_isCurveOver
AlgebraicCurve.HasSeparableResidue.of_perfectField
AlgebraicCurve.Place.instIsLocalHom_restrictSubringHom
AlgebraicCurve.instHasCanonicalLocalResidueKStar ModularCurve.KwNo6Pin.isLocalRing_completion
SheafOfModules.isIso_ihomModelToIhom AlgebraicGeometry.OModulePresheaf.isScalarTower
AlgebraicGeometry.Scheme.OrderedAffineCover.instLinearOrder
AlgebraicGeometry.OModulePresheaf.module AlgebraicGeometry.Scheme.OrderedAffineCover.instFintype
AlgebraicGeometry.Scheme.OrderedAffineCover.instFintypeIdx
AlgebraicGeometry.OModulePresheaf.addCommGroup
AlgebraicGeometry.Scheme.OrderedAffineCover.instDecidableEqIdx
AlgebraicGeometry.OModulePresheaf.moduleSections
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
AlgebraicGeometry.OModulePresheaf.instSubsingletonObjZero
AlgebraicGeometry.OModulePresheaf.Leray.relAltC_scalarTower
AlgebraicGeometry.OModulePresheaf.Leray.ker_relAltd_modΓ
AlgebraicGeometry.OModulePresheaf.Leray.relAltC_modΓ
AlgebraicGeometry.OModulePresheaf.Leray.biC_abGrp
AlgebraicGeometry.OModulePresheaf.Leray.relAltH_modΓ
AlgebraicGeometry.OModulePresheaf.Leray.ker_relAltd_smul
AlgebraicGeometry.OModulePresheaf.Leray.relAltH_scalarTower
AlgebraicGeometry.OModulePresheaf.Leray.relAltH_smul
AlgebraicGeometry.OModulePresheaf.Leray.biC_module DoubleComplex.instModuleE₂I
DoubleComplex.Bounded.modR DoubleComplex.instModuleE₂II DoubleComplex.instAddCommGroupE₂II
DoubleComplex.Bounded.abGrp
attribute [-instance]
DoubleComplex.instAddCommGroupE₂I AlgebraicGeometry.ChowDatum.hι_closed
AlgebraicGeometry.ChowDatumProj.hιN_closed AlgebraicGeometry.ChowDatumProj.hp_proper
AlgebraicGeometry.ChowDatum.hp_isoU AlgebraicGeometry.ChowDatum.hp_proper
AlgebraicGeometry.ProjSpace.algebraAway AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
AlgebraicGeometry.ChowDatumProj.hp_isoU AlgebraicGeometry.ProjSpace.isProper_π
AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial ProjSpaceCech.GradedModule.H.module
ProjSpaceCech.GradedModule.H.addCommGroup ProjSpaceCech.GradedModule.sec.instAdd
ProjSpaceCech.GradedModule.sec.instNeg ProjSpaceCech.GradedModule.acg
ProjSpaceCech.GradedModule.Frac.setoid ProjSpaceCech.GradedModule.modR
ProjSpaceCech.GradedModule.sec.instModule ProjSpaceCech.GradedModule.sec.instAddCommGroup
ProjSpaceCech.GradedModule.sec.instZero ProjSpaceCech.GradedModule.Presentation.fJ
ProjSpaceCech.GradedModule.sec.instSMul ProjSpaceCech.Twist.H.module ProjSpaceCech.Idx.instFintype
ProjSpaceCech.Twist.H.addCommGroup ProjSpaceCech.Idx.instDecidableEq
ProjSpaceCech.Twist.Mon.instDecidableEq ProjSpaceCech.Twist.cochain.instAddCommGroup
ProjSpaceCech.Twist.cochain.instModule AlgebraicGeometry.FGSubalgebra.tensorStage_directedSystem
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
AlgebraicGeometry.RelEffCartierDiv.isClosedImmersion_subschemeι_resProdMap
AlgebraicGeometry.RelEffCartierDiv.isOpenImmersion_resProdMap
attribute [-simp]
AlgebraicGeometry.FGSubalgebra.cocone_ι_app_apply AlgebraicGeometry.RelPicard.fst_toProdSpec
AlgebraicGeometry.RelPicard.toProdSpec_fst_assoc
AlgebraicGeometry.RelPicard.pointsSubBasepointModule_cons
AlgebraicGeometry.RelPicard.pointsSubBasepointModule_nil
AlgebraicGeometry.RelPicard.fst_toProdSpec_assoc AlgebraicGeometry.RelPicard.toProdSpec_fst
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.sub_app
AlgebraicGeometry.Scheme.IdealSheafData.sres_sresTop
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.add_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.sizeOf_spec
AlgebraicGeometry.Scheme.IdealSheafData.coe_resLE
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.smul_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_ofLE_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.ideal_range
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zero_app
AlgebraicGeometry.Scheme.IdealSheafData.sres_sres
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.comp_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.neg_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.id_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_mulRight_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.nsmul_app
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.injEq
AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zsmul_app PresheafOfModules.freeεIso_hom_app
PresheafOfModules.freeμIso_hom_app AlgebraicCurve.coe_cechH0Equiv_apply
AlgebraicCurve.cechH1ToH1_mk AlgebraicCurve.lSpaceOn_univ AlgebraicCurve.lSpaceOn_empty
AlgebraicCurve.Place.congrEquiv_symm_apply
AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
AlgebraicCurve.RationalFunctionField.deg_placeOfPoint AlgebraicCurve.Divisor.mapRestrict_single
AlgebraicCurve.Divisor.pushforward_single AlgebraicCurve.Place.coe_restrictInclusion
AlgebraicCurve.Place.mem_fiber
attribute [-simp]
AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
AlgebraicCurve.Pic0.coe_pullbackDegZeroHom AlgebraicCurve.Place.placeOfPrime_toValuationSubring
AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
AlgebraicCurve.Divisor.degree_pushforwardAlong AlgebraicCurve.Pic0.coe_degZeroCorrespondence
AlgebraicCurve.Place.mem_fiberAlong AlgebraicCurve.SemilinearAut.toRingAut_inv
AlgebraicCurve.SemilinearAut.smul_def AlgebraicCurve.SemilinearAut.smul_single
AlgebraicCurve.SemilinearAut.smul_toValuationSubring AlgebraicCurve.SemilinearAut.baseAut_inv
AlgebraicCurve.SemilinearAut.baseAut_ofAlgAut AlgebraicCurve.SemilinearAut.toRingAut_ofAlgAut
AlgebraicCurve.SemilinearAut.toRingAut_one AlgebraicCurve.SemilinearAut.deg_smul
AlgebraicCurve.SemilinearAut.degree_smul AlgebraicCurve.SemilinearAut.coe_degZeroSMulHom
attribute [-simp]
AlgebraicCurve.SemilinearAut.baseAut_mul
AlgebraicCurve.SemilinearAut.coe_smulValuationSubringEquiv_apply
AlgebraicCurve.SemilinearAut.baseAut_one AlgebraicCurve.SemilinearAut.ofAlgAut_smul
AlgebraicCurve.SemilinearAut.coe_torsion_smul AlgebraicCurve.SemilinearAut.toRingAut_mul
AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
attribute [-simp]
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
AlgebraicCurve.Place.differentialCoeff_zero AlgebraicCurve.Place.differentialCoeff_dCoord
AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec AlgebraicCurve.IntegralBasisInLSpace.mk.injEq
AlgebraicCurve.TranscendenceTower.mk.injEq AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
AlgebraicCurve.Place.CanonicalLocalResidueDataK.mk.sizeOf_spec
AlgebraicCurve.Place.CanonicalLocalResidueDataK.mk.injEq AlgebraicCurve.adeleSingle_coe
AlgebraicCurve.kaehlerResidueTermKFam_apply AlgebraicCurve.Place.LocalResidueData.mk.injEq
AlgebraicCurve.Place.LocalResidueData.mk.sizeOf_spec
AlgebraicCurve.Place.kw_ffgc_adicCompletionComapIntegers_coe
AlgebraicCurve.Place.CanonicalLocalResidueDataS.mk.sizeOf_spec
AlgebraicCurve.Place.mem_simplePoleSubmodule AlgebraicCurve.Place.coe_uniformizerSubring
ModularCurve.Lg37.Lg37CompletionSection.mk.injEq
AlgebraicCurve.Place.CoefficientFieldSection.mk.injEq
AlgebraicCurve.Place.CanonicalLocalResidueDataS.mk.injEq
ModularCurve.Lg37.Lg37CompletionSection.mk.sizeOf_spec
AlgebraicCurve.Place.CoefficientFieldSection.mk.sizeOf_spec AlgebraicCurve.Place.poleSubmodule_one
AlgebraicCurve.Place.mem_poleSubmodule
AlgebraicGeometry.Scheme.Modules.toUnitSection_ofUnitSection
AlgebraicGeometry.Scheme.Modules.pullbackSection_def
AlgebraicGeometry.Scheme.Modules.ofUnitSection_toUnitSection
PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
SheafOfModules.ihomSectionsEquivFamily_unit
AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
AlgebraicGeometry.Scheme.Modules.familyOfHom_app
attribute [-simp]
AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
AlgebraicGeometry.Scheme.Modules.tensorSections_zero_right
AlgebraicGeometry.Scheme.Modules.map_unitSection
AlgebraicGeometry.Scheme.Modules.tensorSectionsBilin_apply
AlgebraicGeometry.Scheme.Modules.tensorPowSection_zero
AlgebraicGeometry.Scheme.Modules.tensorSections_zero_left
AlgebraicGeometry.Scheme.Modules.tensorPow_zero AlgebraicGeometry.Scheme.Modules.tensorPow_succ
AlgebraicGeometry.Scheme.OrderedAffineCover.mk.injEq
AlgebraicGeometry.OModulePresheaf.mk.sizeOf_spec
AlgebraicGeometry.Scheme.OrderedAffineCover.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.mk.injEq
AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq AlgebraicGeometry.OModulePresheaf.Hom.id_app
AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
AlgebraicGeometry.OModulePresheaf.AffHom.id_app
AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq AlgebraicGeometry.OModulePresheaf.prod_obj
attribute [-simp]
AlgebraicGeometry.OModulePresheaf.restrOpen_obj
AlgebraicGeometry.OModulePresheaf.DevissageStep.mk.injEq
AlgebraicGeometry.OModulePresheaf.pushforward_obj AlgebraicGeometry.OModulePresheaf.im_obj
AlgebraicGeometry.OModulePresheaf.pow_obj AlgebraicGeometry.OModulePresheaf.fstHom_app
AlgebraicGeometry.OModulePresheaf.ker_obj AlgebraicGeometry.OModulePresheaf.coker_obj
AlgebraicGeometry.OModulePresheaf.DevissageStep.mk.sizeOf_spec
AlgebraicGeometry.Scheme.OrderedAffineCover.preimage_U
AlgebraicGeometry.OModulePresheaf.sndHom_app
AlgebraicGeometry.OModulePresheaf.Leray.restrictToPreimage_U DoubleComplex.Bounded.mk.injEq
DoubleComplex.Bounded.mk.sizeOf_spec DoubleComplex.Convergence.mk.injEq
DoubleComplex.Convergence.mk.sizeOf_spec DoubleComplex.SubQuot.mk.sizeOf_spec
DoubleComplex.SubQuot.mk.injEq AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
AlgebraicGeometry.ChowDatum.mk.sizeOf_spec AlgebraicGeometry.ChowDatumProj.mk.injEq
AlgebraicGeometry.ChowDatum.mk.injEq ProjSpaceCech.GradedModule.mk.injEq
ProjSpaceCech.GradedModule.mk.sizeOf_spec ProjSpaceCech.GradedModule.Frac.mk.sizeOf_spec
ProjSpaceCech.GradedModule.Presentation.mk.injEq ProjSpaceCech.GradedModule.Frac.mk.injEq
ProjSpaceCech.GradedModule.Presentation.mk.sizeOf_spec
ProjSpaceCech.GradedModule.Hom.shift_toLinearMap ProjSpaceCech.GradedModule.Hom.mk.sizeOf_spec
ProjSpaceCech.GradedModule.Hom.mk.injEq TwoChartCech.Mumford.dK_apply
TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
AlgebraicGeometry.RelPicard.algEquivZeroGroupCut_toSubPicCondition
AlgebraicGeometry.RelPicard.SubPicGroupCondition.mk.injEq
attribute [-simp]
AlgebraicGeometry.RelPicard.SubPicGroupCondition.mk.sizeOf_spec
GoodReductionJacobian.relativeGroupLawOfGrpObj_inv
GoodReductionJacobian.relativeGroupLawOfGrpObj_mul
GoodReductionJacobian.overHomEquivSchemeHomOver_apply_coe
GoodReductionJacobian.relativeGroupLawOfGrpObj_one
GoodReductionJacobian.overHomEquivSchemeHomOver_symm_apply_left
AlgebraicGeometry.RelPicard.LFP.stageHom_val AlgebraicGeometry.RelPicard.rigSection_snd
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.ofInvertible_L
AlgebraicGeometry.RelPicard.rigSection_snd_assoc
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
AlgebraicGeometry.RelPicard.BaseChange.restrict_P
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
AlgebraicGeometry.RelEffCartierDiv.IsUniversal.lift_comp
AlgebraicGeometry.RelEffCartierDiv.functor_map_fst
AlgebraicGeometry.RelEffCartierDiv.IsUniversal.homEquiv_apply
AlgebraicGeometry.RelEffCartierDiv.IsUniversal.lift_pullbackAlong
AlgebraicGeometry.RelEffCartierDiv.IsUniversal.homEquiv_symm_apply
AlgebraicGeometry.RelEffCartierDiv.IsUniversal.lift_comp_assoc
AlgebraicGeometry.RelEffCartierDiv.supportedIn_top
AlgebraicGeometry.RelEffCartierDiv.mem_supportedIn_iff
AlgebraicGeometry.RelEffCartierDiv.supportedIn_top_eq
AlgebraicGeometry.RelEffCartierDiv.restrictAlong_extendAlong
AlgebraicGeometry.RelEffCartierDiv.extendAlong_I AlgebraicGeometry.RelEffCartierDiv.resProdMap_snd
AlgebraicGeometry.RelEffCartierDiv.restrictAlong_I
AlgebraicGeometry.RelEffCartierDiv.extendAlong_restrictAlong
AlgebraicGeometry.RelEffCartierDiv.resProdMap_fst_assoc
AlgebraicGeometry.RelEffCartierDiv.resProdMap_snd_assoc
AlgebraicGeometry.RelEffCartierDiv.resProdMap_fst
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicCurve hiding genus
open _root_.AlgebraicGeometry.AffineLimit
with_weak_namespace _root_.AlgebraicGeometry.RelPicardLean source · statement
theorem exists_openCharts_relSubPicPresheaf_algEquivZeroCut_of_finiteMapData_of_isReduced
(R : Type u) [CommRing R] [IsNoetherianRing R] [_root_.IsReduced R]
{C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
[IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
(h𝔉 : ∀ m₀ : ℕ, ∃ 𝔉 : SmoothProperCurve.FiniteMapData c ε, m₀ ≤ 𝔉.m)
(n g r : ℕ) (hgr : 2 * g < r)
(γ : Fin n → Fin (r - g) → SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
(hγ : HasChartSections c γ) :
∃ (X : ULift.{u} (Fin n) → Scheme.{u})
(f : ∀ i, uliftYoneda.{u + 1}.obj (X i)
⟶ (relSubPicPresheaf c ε (algEquivZeroCut c ε)).overTotal),
(∀ i, MorphismProperty.presheafULift.{u + 1} @IsOpenImmersion (f i)) ∧
Presheaf.IsLocallySurjective Scheme.zariskiTopology (Limits.Sigma.desc f)