AlgebraicGeometry.SmoothProperCurve.exists_twoChartPoleDatum_of_section_invModule
Source context 54 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Models.Gluing.Proofs
namespace SmoothProperCurve_exists_twoChartPoleDatum_of_section_invModule
attribute [-instance] AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instNeg
attribute [-instance] AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulInt
attribute [-instance] AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAddCommGroup
attribute [-instance] AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAdd
attribute [-instance] AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSub
attribute [-instance]
instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
attribute [-instance]
instSMulCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
attribute [-instance] AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulNat
attribute [-instance] AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instZero
attribute [-instance] AlgebraicGeometry.ChowDatum.hι_closed
attribute [-instance] AlgebraicGeometry.ChowDatumProj.hιN_closed
attribute [-instance] AlgebraicGeometry.ChowDatumProj.hp_proper
attribute [-instance] AlgebraicGeometry.ChowDatum.hp_isoU
attribute [-instance] AlgebraicGeometry.ChowDatum.hp_proper
attribute [-instance] AlgebraicGeometry.ProjSpace.algebraAway
attribute [-instance] AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
attribute [-instance] AlgebraicGeometry.ChowDatumProj.hp_isoU
attribute [-instance] AlgebraicGeometry.ProjSpace.isProper_π
attribute [-instance] AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
attribute [-instance] PresheafOfModules.PullbackMonoidal.isIso_δ
attribute [-instance] PresheafOfModules.pushforward_laxMonoidal
attribute [-instance] PresheafOfModules.PullbackMonoidal.isIso_η
attribute [-instance] PresheafOfModules.free_monoidal
attribute [-instance] PresheafOfModules.restrictScalars_laxMonoidal
attribute [-instance] PresheafOfModules.PullbackMonoidal.isIso_δ_gS
attribute [-instance] PresheafOfModules.pullback_oplaxMonoidal
attribute [-instance]
instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
attribute [-instance] PresheafOfModules.pullback_monoidal'
attribute [-instance] AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
attribute [-instance] AlgebraicGeometry.Scheme.Modules.pullback_monoidal
attribute [-instance] AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
attribute [-instance] AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
attribute [-instance] AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
attribute [-instance] AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
attribute [-instance] AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.subsingleton_of_degree_zero
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.isIso_subschemeIota_snd_of_degree_one
attribute [-instance] AlgebraicGeometry.isIso_ker_graphOver_subschemeIota_snd
attribute [-instance] AlgebraicGeometry.isClosedImmersion_graphOver
AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp] 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.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
AlgebraicGeometry.Scheme.Modules.ProjPresentation.mk.injEq
AlgebraicGeometry.Scheme.Modules.ProjPresentation.mk.sizeOf_spec
AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec AlgebraicGeometry.ChowDatum.mk.sizeOf_spec
AlgebraicGeometry.ChowDatumProj.mk.injEq AlgebraicGeometry.ChowDatum.mk.injEq
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
attribute [-simp] 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
AlgebraicGeometry.prodKerGraph_one AlgebraicGeometry.fibrePowOver.proj_comp
AlgebraicGeometry.prodKerGraph_zero AlgebraicGeometry.RelEffCartierDiv.empty_I
AlgebraicGeometry.fibrePowOver.proj_comp_assoc AlgebraicGeometry.graphOver_fst_assoc
AlgebraicGeometry.RelEffCartierDiv.toPoint_comp
AlgebraicGeometry.RelEffCartierDiv.toPoint_comp_assoc AlgebraicGeometry.graphOver_fst
AlgebraicGeometry.RelEffCartierDiv.ofPoint_I AlgebraicGeometry.graphOver_snd
AlgebraicGeometry.graphOver_snd_assoc AlgebraicCurve.SymmetricPowerPackage.mk.sizeOf_spec
AlgebraicCurve.SymmetricPowerPackage.mk.injEq
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.SmoothProperCurve hiding specMap
open _root_.NeronModelInfra
open _root_.CategoryTheory.MonoidalCategoryLean source · full declaration
theorem _root_.AlgebraicGeometry.SmoothProperCurve.exists_twoChartPoleDatum_of_section_invModule
(R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
{C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsProper c]
[SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (m : ℕ) (hm : 1 ≤ m)
(s : 𝟙_ C.Modules ⟶ (ε.1.ker ^ m).invModule)
(hs : ∀ x ∈ Set.range ε.1.base, x ∉ (Scheme.Modules.zeroSchemeIdeal s).support) :
∃ (U V : C.Opens) (_ : U ⊔ V = ⊤)
(_ : ∀ x : C, x ∈ U ↔ x ∉ Set.range ε.1.base)
(f : Γ(C, U)) (g : Γ(C, V))
(_ : U ⊓ V = C.basicOpen f) (_ : U ⊓ V = C.basicOpen g)
(_ : (C.presheaf.map (homOfLE (inf_le_left : U ⊓ V ≤ U)).op).hom f *
(C.presheaf.map (homOfLE (inf_le_right : U ⊓ V ≤ V)).op).hom g = 1),
(letI := Scheme.TwoAffineOpenCover.algebraOfHom c V;
Module.Free R (Γ(C, V) ⧸ Ideal.span {g}) ∧ Module.finrank R (Γ(C, V) ⧸ Ideal.span {g}) =
m) ∧
(∀ (K : Type u) [Field K] [Algebra R K],
letI := Scheme.TwoAffineOpenCover.algebraOfHom
(pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))
((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)) ⁻¹ᵁ U);
Transcendental K (((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)).app U).hom f)) ∧
(∀ (K : Type u) [Field K] [Algebra R K],
letI := Scheme.TwoAffineOpenCover.algebraOfHom
(pullback.snd c (Scheme.TwoAffineOpenCover.specMap R K))
((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)) ⁻¹ᵁ V);
Transcendental K (((pullback.fst c (Scheme.TwoAffineOpenCover.specMap R K)).app V).hom
g)) := by
obtain ⟨U, V, hcov, hUε, hVZ, f, g, hf, hg, hfg, hgen⟩ :=
AlgebraicGeometry.SmoothProperCurve.exists_twoChart_of_section_invModule R c ε m hm s hs
have hεV : ∀ x ∈ Set.range ε.1.base, x ∈ V := fun x hx => (hVZ x).mpr (hs x hx)
have hT := AlgebraicGeometry.SmoothProperCurve.transcendental_app_of_twoChart_of_section_mem
R c ε U V hcov hUε hεV f g hf hg hfg
have hV : IsAffineOpen V :=
(AlgebraicGeometry.Scheme.Opens.isAffineOpen_and_finite_aeval_of_twoChart_right c U V f g
hcov hf hfg hT.2).1
exact ⟨U, V, hcov, hUε, f, g, hf, hg, hfg,
AlgebraicGeometry.SmoothProperCurve.free_and_finrank_quotient_span_of_generates_ker_pow
R c ε m hm V hV hεV g hgen, hT.1, hT.2⟩