NYLL
Module

geometricallyConnected_of_representsRelSubPic_algEquivZeroCut.lean

Nyll.JacobianVarieties.Picard.geometricallyConnected_of_representsRelSubPic_algEquivZeroCut
26 declarations indexed from sourceView source ↗

Module documentation

Geometric connectedness of the scheme representing algebraically trivial line bundles. Algebraic equivalence connects closed points to zero, and algebraic closure descent handles fields.

Imports7
Imported by2

Declarations

def

zeroPt

L115 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.zeroPt
Documentation

The zero section as a point of the base-changed representing scheme.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
Lean source · statement
def zeroPt {K : Type u} [Field K]
    (y : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of R)) :
    Spec (CommRingCat.of K) ⟶ pullback D.toBase y
theorem

zeroPt_snd

L122 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.zeroPt_snd
Documentation

The zero point is a section of the base-change projection.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
Lean source · statement
theorem zeroPt_snd {K : Type u} [Field K]
    (y : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of R)) :
    zeroPt (D := D) y ≫ pullback.snd D.toBase y = 𝟙 _
abbrev

Fib

L132 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.Fib
Documentation

The fibre formed by a further identity base change.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Compare
variable {k : Type u} [Field k] (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
  {T' : Scheme.{u}} (hT : T' ⟶ Spec (CommRingCat.of k))
Lean source · statement
abbrev Fib (c : C ⟶ Spec (CommRingCat.of R))
def

toFibProd

L136 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.toFibProd
Documentation

Compare a composite base change with an iterated fibre product.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Compare
variable {k : Type u} [Field k] (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
  {T' : Scheme.{u}} (hT : T' ⟶ Spec (CommRingCat.of k))
Lean source · statement
def toFibProd (c : C ⟶ Spec (CommRingCat.of R)) :
    pullback c (hT ≫ y) ⟶ pullback (fibreAt c y (𝟙 (Spec (CommRingCat.of k)))) hT
def

ofFibProd

L146 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.ofFibProd
Documentation

The inverse map from the iterated fibre product.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Compare
variable {k : Type u} [Field k] (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
  {T' : Scheme.{u}} (hT : T' ⟶ Spec (CommRingCat.of k))
Lean source · statement
def ofFibProd (c : C ⟶ Spec (CommRingCat.of R)) :
    pullback (fibreAt c y (𝟙 (Spec (CommRingCat.of k)))) hT ⟶ pullback c (hT ≫ y)
theorem

toFibProd_snd

L163 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.toFibProd_snd
Documentation

The comparison preserves the outer base coordinate.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Compare
variable {k : Type u} [Field k] (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
  {T' : Scheme.{u}} (hT : T' ⟶ Spec (CommRingCat.of k))
Lean source · statement
theorem toFibProd_snd (c : C ⟶ Spec (CommRingCat.of R)) :
    toFibProd y hT c ≫ pullback.snd _ _ = pullback.snd c (hT ≫ y)
theorem

toFibProd_fst_snd

L167 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.toFibProd_fst_snd
Documentation

The comparison has the prescribed intermediate base coordinate.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Compare
variable {k : Type u} [Field k] (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
  {T' : Scheme.{u}} (hT : T' ⟶ Spec (CommRingCat.of k))
Lean source · statement
theorem toFibProd_fst_snd (c : C ⟶ Spec (CommRingCat.of R)) :
    toFibProd y hT c ≫ pullback.fst _ _ ≫ pullback.snd _ _ = pullback.snd c (hT ≫ y) ≫ hT
theorem

toFibProd_fst_fst_fst

L171 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.toFibProd_fst_fst_fst
Documentation

The comparison preserves the original curve coordinate.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Compare
variable {k : Type u} [Field k] (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
  {T' : Scheme.{u}} (hT : T' ⟶ Spec (CommRingCat.of k))
Lean source · statement
theorem toFibProd_fst_fst_fst (c : C ⟶ Spec (CommRingCat.of R)) :
    toFibProd y hT c ≫ pullback.fst _ _ ≫ pullback.fst _ _ ≫ pullback.fst c y = pullback.fst c (hT
      ≫ y)
theorem

toFibProd_fst_fst_snd

L176 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.toFibProd_fst_fst_snd
Documentation

The comparison has the original fibre base coordinate.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Compare
variable {k : Type u} [Field k] (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
  {T' : Scheme.{u}} (hT : T' ⟶ Spec (CommRingCat.of k))
Lean source · statement
theorem toFibProd_fst_fst_snd (c : C ⟶ Spec (CommRingCat.of R)) :
    toFibProd y hT c ≫ pullback.fst _ _ ≫ pullback.fst _ _ ≫ pullback.snd c y = pullback.snd c (hT
      ≫ y) ≫ hT
theorem

ofFibProd_fst

L181 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.ofFibProd_fst
Documentation

The inverse comparison recovers the original curve coordinate.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Compare
variable {k : Type u} [Field k] (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
  {T' : Scheme.{u}} (hT : T' ⟶ Spec (CommRingCat.of k))
Lean source · statement
theorem ofFibProd_fst (c : C ⟶ Spec (CommRingCat.of R)) :
    ofFibProd y hT c ≫ pullback.fst c (hT ≫ y) = pullback.fst _ _ ≫ pullback.fst _ _ ≫ pullback.fst
      c y
theorem

ofFibProd_snd

L186 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.ofFibProd_snd
Documentation

The inverse comparison preserves the outer base coordinate.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Compare
variable {k : Type u} [Field k] (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
  {T' : Scheme.{u}} (hT : T' ⟶ Spec (CommRingCat.of k))
Lean source · statement
theorem ofFibProd_snd (c : C ⟶ Spec (CommRingCat.of R)) :
    ofFibProd y hT c ≫ pullback.snd c (hT ≫ y) = pullback.snd _ _
theorem

toFibProd_ofFibProd

L191 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.toFibProd_ofFibProd
Documentation

The forward comparison followed by the inverse is the identity.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Compare
variable {k : Type u} [Field k] (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
  {T' : Scheme.{u}} (hT : T' ⟶ Spec (CommRingCat.of k))
Lean source · statement
theorem toFibProd_ofFibProd (c : C ⟶ Spec (CommRingCat.of R)) :
    toFibProd y hT c ≫ ofFibProd y hT c = 𝟙 _
theorem

ofFibProd_toFibProd

L198 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.ofFibProd_toFibProd
Documentation

The inverse comparison followed by the forward map is the identity.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Compare
variable {k : Type u} [Field k] (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
  {T' : Scheme.{u}} (hT : T' ⟶ Spec (CommRingCat.of k))
Lean source · statement
theorem ofFibProd_toFibProd (c : C ⟶ Spec (CommRingCat.of R)) :
    ofFibProd y hT c ≫ toFibProd y hT c = 𝟙 _
def

fibProdIso

L217 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.fibProdIso
Documentation

The isomorphism between composite base change and the iterated fibre product.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Compare
variable {k : Type u} [Field k] (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
  {T' : Scheme.{u}} (hT : T' ⟶ Spec (CommRingCat.of k))
Lean source · statement
def fibProdIso (c : C ⟶ Spec (CommRingCat.of R)) :
    pullback c (hT ≫ y) ≅ pullback (fibreAt c y (𝟙 (Spec (CommRingCat.of k)))) hT
theorem

connectedSpace_of_geometricallyIntegral

L226 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.connectedSpace_of_geometricallyIntegral
Documentation

A geometrically integral scheme over a field is connected.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Helpers
Lean source · statement
theorem connectedSpace_of_geometricallyIntegral {k : Type u} [Field k] {T' : Scheme.{u}}
    (hT : T' ⟶ Spec (CommRingCat.of k)) [GeometricallyIntegral hT] : ConnectedSpace ↥T'
theorem

nonempty_ofInvertible_iso_of_field

L234 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.nonempty_ofInvertible_iso_of_field
Documentation

Rigidifying an invertible module over a field preserves its isomorphism class.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Helpers
variable {k : Type u} [Field k]
Lean source · statement
theorem nonempty_ofInvertible_iso_of_field (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    (N : (pullback c y).Modules) (hN : Scheme.Modules.IsInvertible N) :
    Nonempty ((RigidifiedLineBundle.ofInvertible (ε := ε) N hN).L ≅ N)
def

toFibOne

L242 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.toFibOne
Documentation

The comparison with an additional identity fibre product.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Helpers
variable {k : Type u} [Field k]
Lean source · statement
def toFibOne (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    (c : C ⟶ Spec (CommRingCat.of R)) :
    pullback c y ⟶ pullback (fibreAt c y (𝟙 (Spec (CommRingCat.of k)))) (𝟙 (Spec (CommRingCat.of
      k)))
theorem

toFibOne_fst_fst

L251 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.toFibOne_fst_fst
Documentation

The original coordinate of the identity-fibre comparison.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Helpers
variable {k : Type u} [Field k]
Lean source · statement
theorem toFibOne_fst_fst (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    (c : C ⟶ Spec (CommRingCat.of R)) :
    toFibOne y c ≫ pullback.fst _ _ ≫ pullback.fst _ _ = 𝟙 _
theorem

toFibOne_fst_snd

L256 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.toFibOne_fst_snd
Documentation

The inner base coordinate of the identity-fibre comparison.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Helpers
variable {k : Type u} [Field k]
Lean source · statement
theorem toFibOne_fst_snd (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    (c : C ⟶ Spec (CommRingCat.of R)) :
    toFibOne y c ≫ pullback.fst _ _ ≫ pullback.snd _ _ = pullback.snd c y
theorem

toFibOne_snd

L261 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.toFibOne_snd
Documentation

The outer base coordinate of the identity-fibre comparison.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Helpers
variable {k : Type u} [Field k]
Lean source · statement
theorem toFibOne_snd (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    (c : C ⟶ Spec (CommRingCat.of R)) :
    toFibOne y c ≫ pullback.snd _ _ = pullback.snd c y
theorem

baseChangeSnd_toFibProd

L267 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.baseChangeSnd_toFibProd
Documentation

The fibre-product comparisons commute with a section of the parameter family.

Source context 20 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
section Helpers
variable {k : Type u} [Field k]
Lean source · statement
theorem baseChangeSnd_toFibProd (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    {T' : Scheme.{u}} (hT : T' ⟶ Spec (CommRingCat.of k))
    (τ : SchemeHomOver y (hT ≫ y)) (t : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) hT) (hτ : τ.1 =
      t.1)
    (c : C ⟶ Spec (CommRingCat.of R)) :
    baseChangeSnd c τ ≫ toFibProd y hT c =
      toFibOne y c ≫ baseChangeSnd (fibreAt c y (𝟙 (Spec (CommRingCat.of k)))) t
theorem

mem_connectedComponent_zero

L298 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.mem_connectedComponent_zero
Documentation

Every closed point lies in the connected component of the zero section.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
Lean source · statement
theorem mem_connectedComponent_zero (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    [LocallyOfFiniteType D.toBase] {k : Type u} [Field k] [IsAlgClosed k]
    (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    (x : ↥(pullback D.toBase y)) (hx : x ∈ closedPoints ↥(pullback D.toBase y)) :
    x ∈ connectedComponent (zeroPt (D := D) y (IsLocalRing.closedPoint k))
theorem

connectedSpace_pullback_of_isAlgClosed

L453 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.connectedSpace_pullback_of_isAlgClosed
Documentation

The representing scheme becomes connected over an algebraically closed field.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
Lean source · statement
theorem connectedSpace_pullback_of_isAlgClosed (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    [LocallyOfFiniteType D.toBase] {k : Type u} [Field k] [IsAlgClosed k]
    (y : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R)) :
    ConnectedSpace ↥(pullback D.toBase y)
theorem

connectedSpace_pullback

L467 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.Connected.connectedSpace_pullback
Documentation

The representing scheme becomes connected over any field.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace AlgebraicGeometry
namespace RelPicard
namespace Connected
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {D : RelativePic0Designation R c}
Lean source · statement
theorem connectedSpace_pullback (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    [LocallyOfFiniteType D.toBase] {K : Type u} [Field K]
    (y : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of R)) :
    ConnectedSpace ↥(pullback D.toBase y)
theorem

geometricallyConnected_of_representsRelSubPic_algEquivZeroCut'

L563 ↗
JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard.geometricallyConnected_of_representsRelSubPic_algEquivZeroCut'
Documentation

The geometric fibres of the representing scheme are connected.

Source context 25 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
attribute [local simp] Connected.zeroPt_snd
attribute [local simp] Connected.toFibProd_snd
attribute [local simp] Connected.toFibProd_fst_snd
attribute [local simp] Connected.toFibProd_fst_fst_fst
attribute [local simp] Connected.toFibProd_fst_fst_snd
attribute [local simp] Connected.ofFibProd_fst
attribute [local simp] Connected.ofFibProd_snd
attribute [local simp] Connected.toFibOne_fst_fst
attribute [local simp] Connected.toFibOne_fst_snd
attribute [local simp] Connected.toFibOne_snd
open scoped _root_.AlgebraicGeometry in
open scoped _root_.AlgebraicGeometry.RelPicard in
open AlgebraicGeometry.RelPicard.Connected in
Lean source · statement
theorem AlgebraicGeometry.RelPicard.geometricallyConnected_of_representsRelSubPic_algEquivZeroCut'
    (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (D : RelativePic0Designation R c) (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    [LocallyOfFiniteType D.toBase] :
    GeometricallyConnected D.toBase
theorem

geometricallyConnected_of_representsRelSubPic_algEquivZeroCut

L579 ↗
AlgebraicGeometry.RelPicard.geometricallyConnected_of_representsRelSubPic_algEquivZeroCut
Documentation

The scheme representing algebraically trivial line bundles is geometrically connected.

Source context 23 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PicardConnectedness
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
attribute [local simp] Connected.zeroPt_snd
attribute [local simp] Connected.toFibProd_snd
attribute [local simp] Connected.toFibProd_fst_snd
attribute [local simp] Connected.toFibProd_fst_fst_fst
attribute [local simp] Connected.toFibProd_fst_fst_snd
attribute [local simp] Connected.ofFibProd_fst
attribute [local simp] Connected.ofFibProd_snd
attribute [local simp] Connected.toFibOne_fst_fst
attribute [local simp] Connected.toFibOne_fst_snd
attribute [local simp] Connected.toFibOne_snd
open CategoryTheory CategoryTheory.Limits _root_.AlgebraicGeometry
  _root_.JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry
  _root_.AlgebraicGeometry.RelPicard
  _root_.JacobianVarieties.Picard.Proofs.PicardConnectedness.AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian in
Lean source · statement
theorem
  _root_.AlgebraicGeometry.RelPicard.geometricallyConnected_of_representsRelSubPic_algEquivZeroCut
    (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (D : RelativePic0Designation R c) (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    [LocallyOfFiniteType D.toBase] :
    GeometricallyConnected D.toBase

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