JacobianVarieties.Picard.Proofs.FGProductModel.CubeDescentAux.FGStages.Idx
Finitely generated subalgebras containing the chosen initial subalgebra.
Source context 24 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FGProductModel
attribute [-instance]
AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
AlgebraicGeometry.SubalgebraStages.compactSpace_obj
AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
AlgebraicGeometry.SubalgebraStages.isCofiltered_op
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
TwoChartCech.Sections.M0_moduleA
TwoChartCech.Sections.M1_module
TwoChartCech.Cover.A01_algebra
TwoChartCech.Cover.A0_algebra
TwoChartCech.Cover.A1_commRing
TwoChartCech.Cover.A1_algebra
TwoChartCech.Sections.M01_module
TwoChartCech.Sections.M0_addCommGroup
TwoChartCech.Sections.M0_tower
TwoChartCech.Sections.M01_addCommGroup
TwoChartCech.Cover.A0_commRing
TwoChartCech.Sections.M1_tower
TwoChartCech.Sections.M01_moduleA
TwoChartCech.Sections.M0_module
TwoChartCech.Sections.M1_moduleA
TwoChartCech.Sections.M1_addCommGroup
TwoChartCech.Cover.A01_commRing
TwoChartCech.Sections.M01_tower
CoherentBaseChange.TwoTermComplex.C0_module
CoherentBaseChange.TwoTermComplex.C0_addCommGroup
CoherentBaseChange.TwoTermComplex.C1_module
CoherentBaseChange.TwoTermComplex.C1_addCommGroup
attribute [-instance]
CoherentBaseChange.TwoTermComplex.C0_free
CoherentBaseChange.TwoTermComplex.C1_finite
CoherentBaseChange.TwoTermComplex.C0_finite
CoherentBaseChange.TwoTermComplex.C1_free
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
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
DoubleComplex.instModuleE₂I
DoubleComplex.Bounded.modR
DoubleComplex.instModuleE₂II
DoubleComplex.instAddCommGroupE₂II
DoubleComplex.Bounded.abGrp
DoubleComplex.instAddCommGroupE₂I
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
attribute [-instance]
ProjSpaceCech.Twist.Mon.instDecidableEq
ProjSpaceCech.Twist.cochain.instAddCommGroup
ProjSpaceCech.Twist.cochain.instModule
instTopologicallyFGOfFiniteType
AlgebraicCurve.CurveModel.isProper
AlgebraicCurve.CurveModel.isIntegral
AlgebraicCurve.CurveModel.smooth
AlgebraicCurve.Place.instIsScalarTowerSubtypeMemValuationSubringToValuationSubring
AlgebraicCurve.Divisor.instDistribMulActionAlgEquiv
AlgebraicCurve.Place.instSMulAlgEquiv
AlgebraicCurve.Place.instIsPrincipalIdealRingSubtypeMemValuationSubringToValuationSubring
AlgebraicCurve.Place.instIsDiscreteValuationRingSubtypeMemValuationSubringToValuationSubring
AlgebraicCurve.Pic0.instDistribMulActionAlgEquiv
AlgebraicCurve.Place.instAlgebraSubtypeMemValuationSubringToValuationSubring
AlgebraicCurve.Place.instMulActionAlgEquiv
AlgebraicCurve.Pic0.instSMulAlgEquiv
AlgebraicCurve.CurveModel.locallyOfFiniteType_gluedToBase
AlgebraicCurve.CurveModel.isFractionRing_overlap
AlgebraicCurve.CurveModel.isLocallyNoetherian_glued
AlgebraicCurve.CurveModel.jacobsonSpace_glued
AlgebraicCurve.CurveModel.isOpenImmersion_ι₀
AlgebraicCurve.CurveModel.isIntegral_glued
AlgebraicCurve.CurveModel.quasiSeparated_gluedToBase
AlgebraicCurve.CurveModel.compactSpace_glued
AlgebraicCurve.CurveModel.isIntegral_adjoin_chartRing
AlgebraicCurve.CurveModel.isFractionRing_overlap_functionField
AlgebraicCurve.CurveModel.isProper_gluedToBase
AlgebraicCurve.CurveModel.isOpenImmersion_ιU
AlgebraicCurve.CurveModel.isOpenImmersion_f₀
AlgebraicCurve.CurveModel.isOpenImmersion_fInf
AlgebraicCurve.CurveModel.isOpenImmersion_ιInf
AlgebraicCurve.CurveModel.algebra_overlap_functionField
AlgebraicCurve.CurveModel.quasiCompact_gluedToBase
AlgebraicCurve.CurveModel.algebraAdjoin
AlgebraicCurve.CurveModel.isDedekindDomain_chartRing
AlgebraicCurve.CurveModel.isIntegralClosure
AlgebraicCurve.CurveModel.finite_chartRing
AlgebraicCurve.CurveModel.centre_isPrime
AlgebraicCurve.CurveModel.isFractionRing_chartRing
AlgebraicCurve.CurveModel.finiteType_chartRing
attribute [-instance]
AlgebraicCurve.CurveModel.isNoetherianRing_chartRing
AlgebraicCurve.CurveModel.isScalarTower_base_adjoin
AlgebraicCurve.CurveModel.isScalarTower_adjoin
AlgebraicCurve.CurveModel.chartRing_finitePresentation
AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
AdicCompletion.instIsLocalRingMaximalIdeal
AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.instSMulFamilies
AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.instModulePreGlue
AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.instModuleFamilies
SheafOfModules.isIso_ihomModelToIhom
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'
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
attribute [-simp]
AlgebraicGeometry.SubalgebraStages.specCone_π_app
AlgebraicGeometry.SubalgebraStages.specLeg_specHom
AlgebraicGeometry.SubalgebraStages.specLeg_specTrans
AlgebraicGeometry.SubalgebraStages.cone_pt
AlgebraicGeometry.SubalgebraStages.trans_fst
AlgebraicGeometry.SubalgebraStages.diagram_obj
AlgebraicGeometry.SubalgebraStages.leg_snd
AlgebraicGeometry.SubalgebraStages.diagram_map
AlgebraicGeometry.SubalgebraStages.specTrans_refl
AlgebraicGeometry.SubalgebraStages.trans_snd
AlgebraicGeometry.SubalgebraStages.specTrans_specHom
AlgebraicGeometry.SubalgebraStages.specCone_pt
AlgebraicGeometry.SubalgebraStages.cone_π_app
AlgebraicGeometry.SubalgebraStages.specDiagram_map
AlgebraicGeometry.SubalgebraStages.specDiagram_obj
AlgebraicGeometry.SubalgebraStages.leg_fst
AlgebraicGeometry.SubalgebraStages.leg_trans
AlgebraicGeometry.Scheme.OrderedAffineCover.mk.injEq
AlgebraicGeometry.OModulePresheaf.mk.sizeOf_spec
AlgebraicGeometry.Scheme.OrderedAffineCover.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.mk.injEq
AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.injEq
AlgebraicGeometry.Scheme.TwoAffineOpenCover.mk.sizeOf_spec
AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U1
AlgebraicGeometry.Scheme.TwoAffineOpenCover.pullback_U0
TwoChartCech.Sections.mk.injEq
TwoChartCech.Cover.mk.injEq
TwoChartCech.GrothendieckComplex.mk.injEq
TwoChartCech.Sections.mk.sizeOf_spec
TwoChartCech.Cover.mk.sizeOf_spec
TwoChartCech.Cover.lineBundle_r0_apply
TwoChartCech.GrothendieckComplex.mk.sizeOf_spec
TwoChartCech.Cover.lineBundle_r1_apply
CoherentBaseChange.TwoTermComplex.mk.sizeOf_spec
CoherentBaseChange.TwoTermComplex.mk.injEq
AlgebraicGeometry.OModulePresheaf.prod_obj
AlgebraicGeometry.OModulePresheaf.restrOpen_obj
AlgebraicGeometry.OModulePresheaf.DevissageStep.mk.injEq
AlgebraicGeometry.OModulePresheaf.pushforward_obj
attribute [-simp]
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.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.Leray.restrictToPreimage_U
AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_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
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
attribute [-simp]
ProjSpaceCech.GradedModule.Presentation.mk.sizeOf_spec
ProjSpaceCech.GradedModule.Hom.shift_toLinearMap
ProjSpaceCech.GradedModule.Hom.mk.sizeOf_spec
ProjSpaceCech.GradedModule.Hom.mk.injEq
AlgebraicGeometry.schemeFibreEndo_snd
AlgebraicGeometry.schemeFibreEndo_fst
AlgebraicCurve.CurveModel.mk.injEq
AlgebraicCurve.CurveModel.mk.sizeOf_spec
AlgebraicCurve.Place.mk.injEq
AlgebraicCurve.Divisor.degree_single
AlgebraicCurve.Divisor.smul_single
AlgebraicCurve.Place.smul_toValuationSubring
AlgebraicCurve.Place.heightOneSpectrum_asIdeal
AlgebraicCurve.Place.coe_algebraMap
AlgebraicCurve.Place.ord_one
AlgebraicCurve.Place.coe_smulRingEquiv_apply
AlgebraicCurve.Pic0.coe_degZeroSMulHom
AlgebraicCurve.Place.deg_smul
AlgebraicCurve.Pic0.mk_zero
AlgebraicCurve.Place.mk.sizeOf_spec
AlgebraicCurve.Divisor.degree_smul
AlgebraicCurve.Pic0.mk_add
AlgebraicCurve.Place.ord_zero
AlgebraicCurve.Place.ofHeightOneSpectrum_toValuationSubring
AlgebraicCurve.CurveModel.coe_gInf
AlgebraicCurve.CurveModel.coe_tInvChart
AlgebraicCurve.CurveModel.ιInf_gluedToBase_assoc
AlgebraicCurve.CurveModel.ιInf_gluedToBase
AlgebraicCurve.CurveModel.primeOfι₀_asIdeal
AlgebraicCurve.CurveModel.coe_tChart
AlgebraicCurve.CurveModel.ι₀_gluedToBase_assoc
AlgebraicCurve.CurveModel.primeOfιInf_asIdeal
AlgebraicCurve.CurveModel.ι₀_gluedToBase
AlgebraicCurve.CurveModel.coe_tma
AlgebraicCurve.CurveModel.coe_primeEquivChartPlaces
AlgebraicCurve.Place.congrEquiv_symm_apply
AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
AlgebraicCurve.Place.congrEquiv_apply
AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
attribute [-simp]
AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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.Modules.glueComponent_glueMk
AlgebraicGeometry.Scheme.Modules.UnitCocycle.mk.injEq
AlgebraicGeometry.Scheme.Modules.UnitCocycle.mk.sizeOf_spec
AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
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
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
PresheafOfModules.freeεIso_hom_app
PresheafOfModules.freeμIso_hom_app
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.Polarisation
open _root_.AlgebraicGeometry.RelPicard
noncomputable section
namespace CubeDescentAux
namespace FGStages
variable {A₀ : Type} [CommRing A₀] {A : Type} [CommRing A] [Algebra A₀ A] (B : Subalgebra A₀ A)Lean source · statement
abbrev Idx : Type