NYLL
Module

RigidifiedLineBundle_nonempty_pullbackAlong_one_iso_unit_of_locIsoOnBase_face.lean

Nyll.JacobianVarieties.Picard.RigidifiedLineBundle_nonempty_pullbackAlong_one_iso_unit_of_locIsoOnBase_face
1 declaration indexed from sourceView source ↗

Module documentation

Triviality of a rigidified bundle on the identity face

Use the naturality of the group identity to compare the identity face with base change. Local triviality on the face and the sections of the proper abelian scheme yield a global trivialization compatible with the rigidification.

Imports20
Imported by2

Declarations

theorem

nonempty_pullbackAlong_one_iso_unit_of_locIsoOnBase_face

L116 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.nonempty_pullbackAlong_one_iso_unit_of_locIsoOnBase_face
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.UnitOneFace
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
  IsDirectLimit.Module.instDirectLimitCoeLinearMapIdOfOfNonempty
  AdicCompletion.instIsLocalRingMaximalIdeal
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
  IsDirectLimit.Module.linearEquiv_symm_apply
  IsDirectLimit.linearEquiv_symm_apply
  IsDirectLimit.lift_of
  IsDirectLimit.Module.linearEquiv_apply
  IsDirectLimit.Module.lift_of
  IsDirectLimit.Equiv_apply
  GoodReductionJacobian.RelativeGroupLaw.baseChangePointToBase_ofBase
  GoodReductionJacobian.RelativeGroupLaw.baseChangePointToBase_coe
  GoodReductionJacobian.RelativeGroupLaw.baseChangePointOfBase_coe
  GoodReductionJacobian.RelativeGroupLaw.baseChange_inv
  GoodReductionJacobian.RelativeGroupLaw.baseChangePointOfBase_toBase
  GoodReductionJacobian.RelativeGroupLaw.baseChange_mul
  GoodReductionJacobian.RelativeGroupLaw.baseChange_one
  NeronModelInfra.fibreRestrictAlong_coe_comp_snd
  NeronModelInfra.fibreRestrictAlong_coe_comp_fst
  NeronModelInfra.fibreRestrictAlong_coe_comp_fst_assoc
attribute [-simp]
  NeronModelInfra.fibreRestrictAlong_coe_comp_snd_assoc
  GoodReductionJacobian.RelativeGroupLaw.fibre_inv
  GoodReductionJacobian.RelativeGroupLaw.fibrePointToBase_coe
  GoodReductionJacobian.RelativeGroupLaw.fibrePointOfBase_toBase
  GoodReductionJacobian.RelativeGroupLaw.fibre_mul
  GoodReductionJacobian.RelativeGroupLaw.fibrePointToBase_ofBase
  GoodReductionJacobian.RelativeGroupLaw.fibre_one
  GoodReductionJacobian.RelativeGroupLaw.fibrePointOfBase_coe
  AlgebraicGeometry.schemeFibreEndo_snd
  AlgebraicGeometry.schemeFibreEndo_fst
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
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RigidifiedLineBundle
Lean source · full declaration
theorem nonempty_pullbackAlong_one_iso_unit_of_locIsoOnBase_face
    {S : Type} [CommRing S] {A : Scheme} {f : A ⟶ Spec (CommRingCat.of S)}
    (L : RelativeGroupLaw S f) (hA : AbelianSchemePropertyBundle S f)
    (M : RigidifiedLineBundle (prodStr f f) ((L.prod L).one (𝟙 (Spec (CommRingCat.of S)))) f)
    (h₃ : LocIsoOnBase (prodStr f f)
      ((Scheme.Modules.pullback
        (pullback.lift (𝟙 _) (L.one (prodStr f f)).1
          (by rw [Category.id_comp, (L.one _).2]))).obj M.L) (𝟙_ _)) :
    Nonempty ((M.pullbackAlong (L.one (𝟙 (Spec (CommRingCat.of S))))).L ≅
      (RigidifiedLineBundle.unit (c := prodStr f f)
        (ε := (L.prod L).one (𝟙 (Spec (CommRingCat.of S))))
        (𝟙 _)).L) := by
  classical
  let c := prodStr f f
  let e : SchemeHomOver (𝟙 (Spec (CommRingCat.of S))) f := L.one (𝟙 (Spec (CommRingCat.of S)))
  let face : pullback f f ⟶ pullback c f :=
    pullback.lift (𝟙 _) (L.one (prodStr f f)).1 (by rw [Category.id_comp, (L.one _).2])
  have hone : (L.one (prodStr f f)).1 = prodStr f f ≫ e.1 := by
    have := L.one_natural (𝟙 (Spec (CommRingCat.of S)))
      (prodStr f f) (prodStr f f) (Category.comp_id _)
    rw [← this, GoodReductionJacobian.schemeHomOverComp_coe]
  have hbc : baseChangeSnd c e = pullback.fst c (𝟙 _) ≫ face := by
    apply pullback.hom_ext
    · rw [Category.assoc, pullback.lift_fst, Category.comp_id]
      unfold baseChangeSnd
      rw [pullback.map]
      erw [pullback.lift_fst]
      rw [Category.comp_id]
    · rw [Category.assoc, pullback.lift_snd, hone, ← Category.assoc, pullback.condition,
        Category.assoc]
      unfold baseChangeSnd
      erw [pullback.lift_snd]
      rfl
  have h₃' := LocIsoOnBase.pullback_of_comp_eq (g := c)
    (pullback.snd c (𝟙 _)) (pullback.fst c (𝟙 _)) (𝟙 _)
    pullback.condition h₃
  have eM : (Scheme.Modules.pullback (pullback.fst c (𝟙 _))).obj
      ((Scheme.Modules.pullback face).obj M.L) ≅
      (M.pullbackAlong e).L :=
    (Scheme.Modules.pullbackComp _ _).app M.L ≪≫ (Scheme.Modules.pullbackCongr hbc.symm).app M.L
  have eU : (Scheme.Modules.pullback (pullback.fst c (𝟙 _))).obj (𝟙_ (pullback f f).Modules) ≅
      (RigidifiedLineBundle.unit (c := prodStr f f)
        (ε := (L.prod L).one (𝟙 (Spec (CommRingCat.of S))))
        (𝟙 _)).L :=
    Scheme.Modules.pullbackTensorUnitObjIso _
  have equivB := LocIsoOnBase.equivalence (pullback.snd c (𝟙 (Spec (CommRingCat.of S))))
  have hloc : LocIsoOnBase (pullback.snd c (𝟙 _)) (M.pullbackAlong e).L
      (RigidifiedLineBundle.unit (c := prodStr f f)
        (ε := (L.prod L).one (𝟙 (Spec (CommRingCat.of S))))
        (𝟙 _)).L :=
    equivB.trans (equivB.trans
      (fun _ => ⟨⊤, trivial, ⟨(Scheme.Modules.pullback _).mapIso eM.symm⟩⟩) h₃')
      (fun _ => ⟨⊤, trivial, ⟨(Scheme.Modules.pullback _).mapIso eU⟩⟩)
  have hP : AbelianSchemePropertyBundle S c := hA.prodStr_commRing hA
  have hB : AbelianSchemePropertyBundle S (pullback.snd c (𝟙 (Spec (CommRingCat.of S)))) :=
    hP.of_isPullback (IsPullback.of_hasPullback c (𝟙 _))
  have : IsProper (pullback.snd c (𝟙 (Spec (CommRingCat.of S)))) := hB.proper
  have hH0 := hB.bijective_algebraMap_sections_pullback
  exact nonempty_iso_of_locIsoOnBase_of_pullback_iso_unit_of_forall_bijective
    (pullback.snd c (𝟙 _)) hH0 (rigSection c (𝟙 _) ((L.prod L).one (𝟙 _))) (pullback.lift_snd _ _ _)
    _ _ (M.pullbackAlong e).isInvertible (RigidifiedLineBundle.unit _).isInvertible hloc
    (M.pullbackAlong e).rigidified.some (RigidifiedLineBundle.unit (𝟙 _)).rigidified.some

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.