NYLL
Module

exists_crossSections_of_isFrameOn_of_map_eq_oneAddEpsMul_smul.lean

Nyll.JacobianVarieties.Picard.exists_crossSections_of_isFrameOn_of_map_eq_oneAddEpsMul_smul
31 declarations indexed from sourceView source ↗

Module documentation

Cross sections for frames on dual number thickenings

Imports20
  • Mathlib.Algebra.Category.Ring.Basic
  • Mathlib.Algebra.Algebra.Hom
  • Mathlib.Algebra.Algebra.Tower
  • Mathlib.Algebra.DualNumber
  • Mathlib.AlgebraicGeometry.Scheme
  • Mathlib.AlgebraicGeometry.AffineScheme
  • Mathlib.AlgebraicGeometry.Modules.Sheaf
  • Mathlib.AlgebraicGeometry.Morphisms.Basic
  • Mathlib.AlgebraicGeometry.Morphisms.Affine
  • Mathlib.AlgebraicGeometry.Morphisms.Separated
  • Mathlib.CategoryTheory.Category.Preorder
  • Mathlib.CategoryTheory.ConcreteCategory.Basic
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  • Mathlib.CategoryTheory.Opposites
  • Mathlib.Order.Lattice
  • Mathlib.Tactic.DefEqTransformations
  • Mathlib.Tactic.LinearCombination
  • Mathlib.Tactic.Ring.Basic
  • Nyll.JacobianVarieties.Picard.PicDualNumberDeformationClassSpec
  • Nyll.JacobianVarieties.Picard.existsUnique_eq_appLE_add_eps_mul_appLE_of_isAffineOpen
Imported by3

Declarations

abbrev

XA

L70 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.XA
Documentation

The curve after extension of scalars to the coefficient ring.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Thick
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (A : Type u) [CommRing
  A] [Algebra R A]
Lean source · statement
abbrev XA : Scheme.{u}
abbrev

XD

L73 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.XD
Documentation

The curve after extension of scalars to the dual number ring.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Thick
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (A : Type u) [CommRing
  A] [Algebra R A]
Lean source · statement
abbrev XD : Scheme.{u}
abbrev

σ

L76 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.σ
Documentation

The morphism from the dual number thickening to the original base change.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Thick
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (A : Type u) [CommRing
  A] [Algebra R A]
Lean source · statement
abbrev σ : XD c A ⟶ XA c A
abbrev

ι

L82 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.ι
Documentation

The homomorphism on sections induced by the thickening projection.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Thick
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (A : Type u) [CommRing
  A] [Algebra R A]
variable {c A}
Lean source · statement
abbrev ι {U : (XA c A).Opens} {U' : (XD c A).Opens} (h : σ c A ⁻¹ᵁ U = U') :
    Γ(XA c A, U) →+* Γ(XD c A, U')
def

eps

L86 ↗
CoverCross.eps
Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Thick
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (A : Type u) [CommRing
  A] [Algebra R A]
variable {c A}
Lean source · statement
def _root_.CoverCross.eps (U' : (XD c A).Opens) : Γ(XD c A, U')
theorem

eps_mul_eps

L93 ↗
CoverCross.eps_mul_eps
Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Thick
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (A : Type u) [CommRing
  A] [Algebra R A]
variable {c A}
Lean source · statement
theorem _root_.CoverCross.eps_mul_eps (U' : (XD c A).Opens) :
    eps (c := c) (A := A) U' * eps U' = 0
theorem

map_eps

L104 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.map_eps
Documentation

Restriction preserves the nilpotent parameter on the thickening.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Thick
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (A : Type u) [CommRing
  A] [Algebra R A]
variable {c A}
Lean source · statement
theorem map_eps {U' V' : (XD c A).Opens} (hV : V' ≤ U') :
    ((XD c A).presheaf.map (homOfLE hV).op).hom (eps U') = eps V'
theorem

map_ι

L113 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.map_ι
Documentation

The map from base sections commutes with restriction.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Thick
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (A : Type u) [CommRing
  A] [Algebra R A]
variable {c A}
Lean source · statement
theorem map_ι {U V : (XA c A).Opens} {U' V' : (XD c A).Opens} (hU : σ c A ⁻¹ᵁ U = U')
    (hV : σ c A ⁻¹ᵁ V = V')
    (hVU : V ≤ U) (hVU' : V' ≤ U') (a : Γ(XA c A, U)) :
    ((XD c A).presheaf.map (homOfLE hVU').op).hom (ι hU a) = ι hV (((XA c A).presheaf.map (homOfLE
      hVU).op).hom a)
theorem

mul_split

L123 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.mul_split
Documentation

Multiplication of split sections uses the square zero relation.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Thick
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (A : Type u) [CommRing
  A] [Algebra R A]
variable {c A}
Lean source · statement
theorem mul_split {U : (XA c A).Opens} {U' : (XD c A).Opens} (h : σ c A ⁻¹ᵁ U = U')
    (x y x' y' : Γ(XA c A, U)) :
    (ι h x + eps U' * ι h y) * (ι h x' + eps U' * ι h y') =
      ι h (x * x') + eps U' * ι h (x * y' + x' * y)
def

cst

L132 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.cst
Documentation

The constant coordinate of a section on the dual number thickening.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Thick
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (A : Type u) [CommRing
  A] [Algebra R A]
variable {c A}
Lean source · statement
def cst {U : (XA c A).Opens} (hUa : IsAffineOpen U) {U' : (XD c A).Opens} (h : σ c A ⁻¹ᵁ U = U')
    (u : Γ(XD c A, U')) : Γ(XA c A, U)
def

lin

L137 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.lin
Documentation

The linear coordinate of a section on the dual number thickening.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Thick
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (A : Type u) [CommRing
  A] [Algebra R A]
variable {c A}
Lean source · statement
def lin {U : (XA c A).Opens} (hUa : IsAffineOpen U) {U' : (XD c A).Opens} (h : σ c A ⁻¹ᵁ U = U')
    (u : Γ(XD c A, U')) : Γ(XA c A, U)
theorem

split_eq

L142 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.split_eq
Documentation

The constant and linear coordinates reconstruct a section.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Thick
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (A : Type u) [CommRing
  A] [Algebra R A]
variable {c A}
Lean source · statement
theorem split_eq {U : (XA c A).Opens} (hUa : IsAffineOpen U) {U' : (XD c A).Opens}
    (h : σ c A ⁻¹ᵁ U = U')
    (u : Γ(XD c A, U')) : u = ι h (cst hUa h u) + eps U' * ι h (lin hUa h u)
theorem

split_unique

L148 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.split_unique
Documentation

The constant and linear coordinates are uniquely determined.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Thick
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (A : Type u) [CommRing
  A] [Algebra R A]
variable {c A}
Lean source · statement
theorem split_unique {U : (XA c A).Opens} (hUa : IsAffineOpen U) {U' : (XD c A).Opens}
    (h : σ c A ⁻¹ᵁ U = U')
    {a b a' b' : Γ(XA c A, U)} (e : ι h a + eps U' * ι h b = ι h a' + eps U' * ι h b') : a = a' ∧ b
      = b'
theorem

map_map

L167 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.map_map
Documentation

Successive restrictions of module sections equal their composite.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Frames
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem map_map {U V W : X.Opens} (h1 : V ≤ U) (h2 : W ≤ V) (s : Γ(M, U)) :
    M.presheaf.map (homOfLE h2).op (M.presheaf.map (homOfLE h1).op s) =
      M.presheaf.map (homOfLE (h2.trans h1)).op s
theorem

map_map_ring

L174 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.map_map_ring
Documentation

Successive restrictions of ring sections equal their composite.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Frames
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem map_map_ring {U V W : X.Opens} (h1 : V ≤ U) (h2 : W ≤ V) (r : Γ(X, U)) :
    (X.presheaf.map (homOfLE h2).op).hom ((X.presheaf.map (homOfLE h1).op).hom r) =
      (X.presheaf.map (homOfLE (h2.trans h1)).op).hom r
theorem

map_homOfLE_refl

L181 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.map_homOfLE_refl
Documentation

Restriction along the identity inclusion fixes a module section.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Frames
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem map_homOfLE_refl {U : X.Opens} (s : Γ(M, U)) :
    M.presheaf.map (homOfLE (le_refl U)).op s = s
theorem

restrict_smul_eq

L188 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.restrict_smul_eq
Documentation

An equality relating scalar multiples of sections restricts to smaller opens.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Frames
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem restrict_smul_eq {U U' W T : X.Opens} (hWU : W ≤ U) (hWU' : W ≤ U') (hTW : T ≤ W)
    {s : Γ(M, U)} {t : Γ(M, U')} {u : Γ(X, W)}
    (h : u • M.presheaf.map (homOfLE hWU).op s = M.presheaf.map (homOfLE hWU').op t) :
    (X.presheaf.map (homOfLE hTW).op).hom u • M.presheaf.map (homOfLE (hTW.trans hWU)).op s =
      M.presheaf.map (homOfLE (hTW.trans hWU')).op t
theorem

exists_units_of_isFrameOn

L198 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.exists_units_of_isFrameOn
Documentation

Two frames on an overlap differ by a unit.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Frames
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem exists_units_of_isFrameOn {U U' W : X.Opens} (hWU : W ≤ U) (hWU' : W ≤ U')
    {s : Γ(M, U)} {s' : Γ(M, U')} (hs : Scheme.Modules.IsFrameOn s U) (hs' :
      Scheme.Modules.IsFrameOn s' U') :
    ∃ v w : Γ(X, W), v • M.presheaf.map (homOfLE hWU).op s = M.presheaf.map (homOfLE hWU').op s' ∧
      w • M.presheaf.map (homOfLE hWU').op s' = M.presheaf.map (homOfLE hWU).op s ∧ v * w = 1
theorem

cross_identity

L213 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.cross_identity
Documentation

Transition units satisfy the compatibility identity across the first cover.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Frames
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem cross_identity {P0 P1 Q : X.Opens} {e0 : Γ(M, P0)} {e1 : Γ(M, P1)} {e' : Γ(M, Q)}
    (hF0 : Scheme.Modules.IsFrameOn e0 P0) (g : Γ(X, P0 ⊓ P1))
    (hg : M.presheaf.map (homOfLE inf_le_right).op e1 = g • M.presheaf.map (homOfLE inf_le_left).op
      e0)
    (u0 : Γ(X, P0 ⊓ Q))
    (hu0 : u0 • M.presheaf.map (homOfLE inf_le_left).op e0 = M.presheaf.map (homOfLE
      inf_le_right).op e')
    (u1 : Γ(X, P1 ⊓ Q))
    (hu1 : u1 • M.presheaf.map (homOfLE inf_le_left).op e1 = M.presheaf.map (homOfLE
      inf_le_right).op e') :
    (X.presheaf.map (homOfLE (inf_le_inf_right Q inf_le_left : (P0 ⊓ P1) ⊓ Q ≤ P0 ⊓ Q)).op).hom u0 =
      (X.presheaf.map (homOfLE (inf_le_inf_right Q inf_le_right : (P0 ⊓ P1) ⊓ Q ≤ P1 ⊓ Q)).op).hom
        u1 *
      (X.presheaf.map (homOfLE (inf_le_left : (P0 ⊓ P1) ⊓ Q ≤ P0 ⊓ P1)).op).hom g
theorem

cross_identity'

L240 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.cross_identity'
Documentation

Transition units satisfy the compatibility identity across the second cover.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Frames
variable {X : Scheme.{u}} {M : X.Modules}
Lean source · statement
theorem cross_identity' {P Q0 Q1 : X.Opens} {e : Γ(M, P)} {e0' : Γ(M, Q0)} {e1' : Γ(M, Q1)}
    (hF : Scheme.Modules.IsFrameOn e P) (g' : Γ(X, Q0 ⊓ Q1))
    (hg' : M.presheaf.map (homOfLE inf_le_right).op e1' = g' • M.presheaf.map (homOfLE
      inf_le_left).op e0')
    (u0 : Γ(X, P ⊓ Q0))
    (hu0 : u0 • M.presheaf.map (homOfLE inf_le_left).op e = M.presheaf.map (homOfLE
      inf_le_right).op e0')
    (u1 : Γ(X, P ⊓ Q1))
    (hu1 : u1 • M.presheaf.map (homOfLE inf_le_left).op e = M.presheaf.map (homOfLE
      inf_le_right).op e1') :
    (X.presheaf.map (homOfLE (inf_le_inf_left P inf_le_right : P ⊓ (Q0 ⊓ Q1) ≤ P ⊓ Q1)).op).hom u1 =
      (X.presheaf.map (homOfLE (inf_le_right : P ⊓ (Q0 ⊓ Q1) ≤ Q0 ⊓ Q1)).op).hom g' *
      (X.presheaf.map (homOfLE (inf_le_inf_left P inf_le_left : P ⊓ (Q0 ⊓ Q1) ≤ P ⊓ Q0)).op).hom u0
theorem

pre_inf

L277 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.pre_inf
Documentation

The thickening projection preserves the specified intersections of opens.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Transport
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)} {A : Type u} [CommRing
  A] [Algebra R A]
Lean source · statement
theorem pre_inf {U V : (XA c A).Opens} {U' V' : (XD c A).Opens} (hU : σ c A ⁻¹ᵁ U = U')
    (hV : σ c A ⁻¹ᵁ V = V') :
    σ c A ⁻¹ᵁ (U ⊓ V) = U' ⊓ V'
theorem

map_split_expr

L283 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.map_split_expr
Documentation

Restriction preserves a split constant plus nilpotent expression.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Transport
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)} {A : Type u} [CommRing
  A] [Algebra R A]
Lean source · statement
theorem map_split_expr {U T : (XA c A).Opens} {U' T' : (XD c A).Opens} (hU : σ c A ⁻¹ᵁ U = U')
    (hT : σ c A ⁻¹ᵁ T = T') (hTU : T ≤ U) (hTU' : T' ≤ U') (a b : Γ(XA c A, U)) :
    ((XD c A).presheaf.map (homOfLE hTU').op).hom (ι hU a + eps U' * ι hU b) =
      ι hT (((XA c A).presheaf.map (homOfLE hTU).op).hom a) + eps T' * ι hT (((XA c A).presheaf.map
        (homOfLE hTU).op).hom b)
theorem

map_split

L291 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.map_split
Documentation

Both coordinates of a split section commute with restriction.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Transport
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)} {A : Type u} [CommRing
  A] [Algebra R A]
Lean source · statement
theorem map_split {U T : (XA c A).Opens} (hUa : IsAffineOpen U) {U' T' : (XD c A).Opens}
    (hU : σ c A ⁻¹ᵁ U = U')
    (hT : σ c A ⁻¹ᵁ T = T') (hTU : T ≤ U) (hTU' : T' ≤ U') (u : Γ(XD c A, U')) :
    ((XD c A).presheaf.map (homOfLE hTU').op).hom u =
      ι hT (((XA c A).presheaf.map (homOfLE hTU).op).hom (cst hUa hU u)) +
        eps T' * ι hT (((XA c A).presheaf.map (homOfLE hTU).op).hom (lin hUa hU u))
theorem

cst_mul_cst

L301 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.cst_mul_cst
Documentation

The constant coordinate of a product is the product of constant coordinates.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Transport
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)} {A : Type u} [CommRing
  A] [Algebra R A]
Lean source · statement
theorem cst_mul_cst {U : (XA c A).Opens} (hUa : IsAffineOpen U) {U' : (XD c A).Opens}
    (hU : σ c A ⁻¹ᵁ U = U')
    {u w : Γ(XD c A, U')} (huw : u * w = 1) : cst hUa hU u * cst hUa hU w = 1
theorem

coords_of_eq

L320 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.coords_of_eq
Documentation

A transition equality determines both coordinates of the first factor.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Main
Lean source · statement
theorem coords_of_eq {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)} {A : Type u}
    [CommRing A]
    [Algebra R A] {T : (XA c A).Opens} (hTa : IsAffineOpen T) {T' : (XD c A).Opens} (hT : σ c A ⁻¹ᵁ
      T = T')
    {a0 b0 a1 b1 f : Γ(XA c A, T)}
    (h : ι hT a0 + eps T' * ι hT b0 = (ι hT a1 + eps T' * ι hT b1) * (1 + eps T' * ι hT f)) :
    a0 = a1 ∧ b0 = a1 * f + b1
theorem

coords_of_eq'

L332 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.coords_of_eq'
Documentation

A transition equality determines both coordinates of the second factor.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Main
Lean source · statement
theorem coords_of_eq' {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)} {A : Type u}
    [CommRing A]
    [Algebra R A] {T : (XA c A).Opens} (hTa : IsAffineOpen T) {T' : (XD c A).Opens} (hT : σ c A ⁻¹ᵁ
      T = T')
    {a0 b0 a1 b1 f : Γ(XA c A, T)}
    (h : ι hT a1 + eps T' * ι hT b1 = (1 + eps T' * ι hT f) * (ι hT a0 + eps T' * ι hT b0)) :
    a1 = a0 ∧ b1 = a0 * f + b0
theorem

map_oneAddEpsMul

L345 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.map_oneAddEpsMul
Documentation

Restricting an infinitesimal unit restricts its coefficient.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Main
Lean source · full declaration
theorem map_oneAddEpsMul {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
    {A : Type u} [CommRing A]
    [Algebra R A] (𝒲 : C.TwoAffineOpenCover)
    (hW01 : σ c A ⁻¹ᵁ ((𝒲.pullback c A).U0 ⊓ (𝒲.pullback c A).U1) =
      (𝒲.pullback c (DualNumber A)).U0 ⊓ (𝒲.pullback c (DualNumber A)).U1)
    {T : (XA c A).Opens} {T' : (XD c A).Opens} (hT : σ c A ⁻¹ᵁ T = T')
    (hTU : T ≤ (𝒲.pullback c A).U0 ⊓ (𝒲.pullback c A).U1)
    (hTU' : T' ≤ (𝒲.pullback c (DualNumber A)).U0 ⊓ (𝒲.pullback c (DualNumber A)).U1)
    (f : Γ(XA c A, (𝒲.pullback c A).U0 ⊓ (𝒲.pullback c A).U1)) :
    ((XD c A).presheaf.map (homOfLE hTU').op).hom
        (show Γ(XD c A, (𝒲.pullback c (DualNumber A)).U0 ⊓ (𝒲.pullback c (DualNumber A)).U1)
          from oneAddEpsMul A 𝒲 c f) =
      1 + eps T' * ι hT (((XA c A).presheaf.map (homOfLE hTU).op).hom f) := by
  have e : (show Γ(XD c A, (𝒲.pullback c (DualNumber A)).U0 ⊓ (𝒲.pullback c (DualNumber A)).U1)
      from oneAddEpsMul A 𝒲 c f) = 1 + eps _ * ι hW01 f := rfl
  rw [e, map_add, map_one, map_mul, map_eps, map_ι hW01 hT hTU hTU']
theorem

coefficient_transition

L362 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.coefficient_transition
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Main
Lean source · statement
theorem coefficient_transition {S : Type*} [CommRing S]
    {a₀ a₁ b₀ b₁ r₀ r₁ f : S}
    (h₀ : a₀ * r₀ = 1) (h₁ : a₁ * r₁ = 1)
    (hconst : a₀ = a₁) (hlinear : b₀ = a₁ * f + b₁) :
    b₀ * r₀ = b₁ * r₁ + f
theorem

coefficient_transition_restrict

L371 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.coefficient_transition_restrict
Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Main
Lean source · statement
theorem coefficient_transition_restrict
    {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
    {A : Type u} [CommRing A] [Algebra R A]
    {U₀ U₁ T : (XA c A).Opens}
    (hU₀a : IsAffineOpen U₀) (hU₁a : IsAffineOpen U₁) (hTa : IsAffineOpen T)
    {U₀' U₁' T' : (XD c A).Opens}
    (hU₀ : σ c A ⁻¹ᵁ U₀ = U₀') (hU₁ : σ c A ⁻¹ᵁ U₁ = U₁')
    (hT : σ c A ⁻¹ᵁ T = T')
    (hT₀ : T ≤ U₀) (hT₁ : T ≤ U₁) (hT₀' : T' ≤ U₀') (hT₁' : T' ≤ U₁')
    {u₀ w₀ : Γ(XD c A, U₀')} {u₁ w₁ : Γ(XD c A, U₁')}
    (huw₀ : u₀ * w₀ = 1) (huw₁ : u₁ * w₁ = 1) (f : Γ(XA c A, T))
    (htransition : ((XD c A).presheaf.map (homOfLE hT₀').op).hom u₀ =
      ((XD c A).presheaf.map (homOfLE hT₁').op).hom u₁ *
        (1 + eps T' * ι hT f)) :
    ((XA c A).presheaf.map (homOfLE hT₀).op).hom
        (lin hU₀a hU₀ u₀ * cst hU₀a hU₀ w₀) =
      ((XA c A).presheaf.map (homOfLE hT₁).op).hom
        (lin hU₁a hU₁ u₁ * cst hU₁a hU₁ w₁) + f
theorem

main

L403 ↗
JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross.main
Documentation

Construct cross sections comparing the two chosen systems of local frames.

Source context 9 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FrameCrossSections
attribute [-instance]
  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.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
universe u
open  CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra AlgebraicGeometry.Scheme.TwoAffineOpenCover
noncomputable section
namespace CoverCross
section Main
Lean source · full declaration
theorem main
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R))
    (A : Type u) [CommRing A] [Algebra R A]
    [IsSeparated (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A))]
    (𝒲 𝒲' : C.TwoAffineOpenCover)
    (N : (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R (DualNumber A))).Modules)
    (e0 : Γ(N, (𝒲.pullback c (DualNumber A)).U0)) (e1 : Γ(N, (𝒲.pullback c (DualNumber A)).U1))
    (f : ((𝒲.pullback c A).cover (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A))).A01)
    (hF0 : Scheme.Modules.IsFrameOn e0 (𝒲.pullback c (DualNumber A)).U0)
    (hF1 : Scheme.Modules.IsFrameOn e1 (𝒲.pullback c (DualNumber A)).U1)
    (hM : N.presheaf.map (homOfLE inf_le_right).op e1 =
      (show Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R (DualNumber A)),
          (𝒲.pullback c (DualNumber A)).U0 ⊓ (𝒲.pullback c (DualNumber A)).U1) from oneAddEpsMul A
            𝒲 c f) •
        N.presheaf.map (homOfLE inf_le_left).op e0)
    (e0' : Γ(N, (𝒲'.pullback c (DualNumber A)).U0)) (e1' : Γ(N, (𝒲'.pullback c (DualNumber A)).U1))
    (f' : ((𝒲'.pullback c A).cover (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A))).A01)
    (hF0' : Scheme.Modules.IsFrameOn e0' (𝒲'.pullback c (DualNumber A)).U0)
    (hF1' : Scheme.Modules.IsFrameOn e1' (𝒲'.pullback c (DualNumber A)).U1)
    (hM' : N.presheaf.map (homOfLE inf_le_right).op e1' =
      (show Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R (DualNumber A)),
          (𝒲'.pullback c (DualNumber A)).U0 ⊓ (𝒲'.pullback c (DualNumber A)).U1) from oneAddEpsMul
            A 𝒲' c f') •
        N.presheaf.map (homOfLE inf_le_left).op e0') :
    let X' := Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A)
    let W0 := (𝒲.pullback c A).U0
    let W1 := (𝒲.pullback c A).U1
    let V0 := (𝒲'.pullback c A).U0
    let V1 := (𝒲'.pullback c A).U1
    ∃ (g00 : Γ(X', W0 ⊓ V0)) (g01 : Γ(X', W0 ⊓ V1)) (g10 : Γ(X', W1 ⊓ V0)) (g11 : Γ(X', W1 ⊓ V1)),
      ((XA c A).presheaf.map (homOfLE (inf_le_inf_right V0 inf_le_left  : (W0 ⊓ W1) ⊓ V0 ≤ W0 ⊓
        V0)).op).hom g00
        = ((XA c A).presheaf.map (homOfLE (inf_le_inf_right V0 inf_le_right : (W0 ⊓ W1) ⊓ V0 ≤ W1 ⊓
          V0)).op).hom g10
          + ((XA c A).presheaf.map (homOfLE (inf_le_left : (W0 ⊓ W1) ⊓ V0 ≤ W0 ⊓ W1)).op).hom f ∧
      ((XA c A).presheaf.map (homOfLE (inf_le_inf_right V1 inf_le_left  : (W0 ⊓ W1) ⊓ V1 ≤ W0 ⊓
        V1)).op).hom g01
        = ((XA c A).presheaf.map (homOfLE (inf_le_inf_right V1 inf_le_right : (W0 ⊓ W1) ⊓ V1 ≤ W1 ⊓
          V1)).op).hom g11
          + ((XA c A).presheaf.map (homOfLE (inf_le_left : (W0 ⊓ W1) ⊓ V1 ≤ W0 ⊓ W1)).op).hom f ∧
      ((XA c A).presheaf.map (homOfLE (inf_le_inf_left W0 inf_le_right : W0 ⊓ (V0 ⊓ V1) ≤ W0 ⊓
        V1)).op).hom g01
        = ((XA c A).presheaf.map (homOfLE (inf_le_inf_left W0 inf_le_left  : W0 ⊓ (V0 ⊓ V1) ≤ W0 ⊓
          V0)).op).hom g00
          + ((XA c A).presheaf.map (homOfLE (inf_le_right : W0 ⊓ (V0 ⊓ V1) ≤ V0 ⊓ V1)).op).hom f' ∧
      ((XA c A).presheaf.map (homOfLE (inf_le_inf_left W1 inf_le_right : W1 ⊓ (V0 ⊓ V1) ≤ W1 ⊓
        V1)).op).hom g11
        = ((XA c A).presheaf.map (homOfLE (inf_le_inf_left W1 inf_le_left  : W1 ⊓ (V0 ⊓ V1) ≤ W1 ⊓
          V0)).op).hom g10
          + ((XA c A).presheaf.map (homOfLE (inf_le_right : W1 ⊓ (V0 ⊓ V1) ≤ V0 ⊓ V1)).op).hom f'
            := by
  intro X' W0 W1 V0 V1
  simp only [X']
  have pW0 : σ c A ⁻¹ᵁ W0 = (𝒲.pullback c (DualNumber A)).U0 := baseChangeSnd_preimage_U0 𝒲 c _
  have pW1 : σ c A ⁻¹ᵁ W1 = (𝒲.pullback c (DualNumber A)).U1 := baseChangeSnd_preimage_U1 𝒲 c _
  have pV0 : σ c A ⁻¹ᵁ V0 = (𝒲'.pullback c (DualNumber A)).U0 := baseChangeSnd_preimage_U0 𝒲' c _
  have pV1 : σ c A ⁻¹ᵁ V1 = (𝒲'.pullback c (DualNumber A)).U1 := baseChangeSnd_preimage_U1 𝒲' c _
  have pW01 := pre_inf pW0 pW1
  have pV01 := pre_inf pV0 pV1
  have p00 := pre_inf pW0 pV0
  have p01 := pre_inf pW0 pV1
  have p10 := pre_inf pW1 pV0
  have p11 := pre_inf pW1 pV1
  have pT0 := pre_inf pW01 pV0
  have pT1 := pre_inf pW01 pV1
  have pS0 := pre_inf pW0 pV01
  have pS1 := pre_inf pW1 pV01
  have : (XA c A).IsSeparated := by
    refine ⟨?_⟩
    have hcomp : IsSeparated
        (pullback.snd c (specMap R A) ≫ terminal.from (Spec (.of A))) := inferInstance
    exact (terminal.comp_from (pullback.snd c (specMap R A))) ▸ hcomp
  have aW0 : IsAffineOpen W0 := (𝒲.pullback c A).isAffineOpen_U0
  have aW1 : IsAffineOpen W1 := (𝒲.pullback c A).isAffineOpen_U1
  have aV0 : IsAffineOpen V0 := (𝒲'.pullback c A).isAffineOpen_U0
  have aV1 : IsAffineOpen V1 := (𝒲'.pullback c A).isAffineOpen_U1
  have aW01 : IsAffineOpen (W0 ⊓ W1) := (𝒲.pullback c A).isAffineOpen_inf
  have aV01 : IsAffineOpen (V0 ⊓ V1) := (𝒲'.pullback c A).isAffineOpen_inf
  have af00 := aW0.inf aV0
  have af01 := aW0.inf aV1
  have af10 := aW1.inf aV0
  have af11 := aW1.inf aV1
  have afT0 := aW01.inf aV0
  have afT1 := aW01.inf aV1
  have afS0 := aW0.inf aV01
  have afS1 := aW1.inf aV01
  obtain ⟨u00, w00, hu00, -, huw00⟩ := exists_units_of_isFrameOn (M := N)
    (inf_le_left : (𝒲.pullback c (DualNumber A)).U0 ⊓ (𝒲'.pullback c (DualNumber A)).U0 ≤
      (𝒲.pullback c (DualNumber A)).U0) (inf_le_right : (𝒲.pullback c (DualNumber A)).U0 ⊓
      (𝒲'.pullback c (DualNumber A)).U0 ≤ (𝒲'.pullback c (DualNumber A)).U0) hF0 hF0'
  obtain ⟨u01, w01, hu01, -, huw01⟩ := exists_units_of_isFrameOn (M := N)
    (inf_le_left : (𝒲.pullback c (DualNumber A)).U0 ⊓ (𝒲'.pullback c (DualNumber A)).U1 ≤
      (𝒲.pullback c (DualNumber A)).U0) (inf_le_right : (𝒲.pullback c (DualNumber A)).U0 ⊓
      (𝒲'.pullback c (DualNumber A)).U1 ≤ (𝒲'.pullback c (DualNumber A)).U1) hF0 hF1'
  obtain ⟨u10, w10, hu10, -, huw10⟩ := exists_units_of_isFrameOn (M := N)
    (inf_le_left : (𝒲.pullback c (DualNumber A)).U1 ⊓ (𝒲'.pullback c (DualNumber A)).U0 ≤
      (𝒲.pullback c (DualNumber A)).U1) (inf_le_right : (𝒲.pullback c (DualNumber A)).U1 ⊓
      (𝒲'.pullback c (DualNumber A)).U0 ≤ (𝒲'.pullback c (DualNumber A)).U0) hF1 hF0'
  obtain ⟨u11, w11, hu11, -, huw11⟩ := exists_units_of_isFrameOn (M := N)
    (inf_le_left : (𝒲.pullback c (DualNumber A)).U1 ⊓ (𝒲'.pullback c (DualNumber A)).U1 ≤
      (𝒲.pullback c (DualNumber A)).U1) (inf_le_right : (𝒲.pullback c (DualNumber A)).U1 ⊓
      (𝒲'.pullback c (DualNumber A)).U1 ≤ (𝒲'.pullback c (DualNumber A)).U1) hF1 hF1'
  refine ⟨lin af00 p00 u00 * cst af00 p00 w00,
    lin af01 p01 u01 * cst af01 p01 w01,
    lin af10 p10 u10 * cst af10 p10 w10,
    lin af11 p11 u11 * cst af11 p11 w11, ?_, ?_, ?_, ?_⟩
  · refine coefficient_transition_restrict af00 af10 afT0 p00 p10 pT0
      (inf_le_inf_right V0 inf_le_left) (inf_le_inf_right V0 inf_le_right)
      (inf_le_inf_right (𝒲'.pullback c (DualNumber A)).U0 inf_le_left)
      (inf_le_inf_right (𝒲'.pullback c (DualNumber A)).U0 inf_le_right)
      huw00 huw10
      (((XA c A).presheaf.map (homOfLE
        (inf_le_left : (W0 ⊓ W1) ⊓ V0 ≤ W0 ⊓ W1)).op).hom f) ?_
    have h := cross_identity (M := N) hF0 (oneAddEpsMul A 𝒲 c f) hM
      u00 hu00 u10 hu10
    rw [map_oneAddEpsMul 𝒲 pW01 pT0
      (inf_le_left : (W0 ⊓ W1) ⊓ V0 ≤ W0 ⊓ W1)
      (inf_le_left : ((𝒲.pullback c (DualNumber A)).U0 ⊓
        (𝒲.pullback c (DualNumber A)).U1) ⊓ (𝒲'.pullback c (DualNumber A)).U0 ≤
          (𝒲.pullback c (DualNumber A)).U0 ⊓ (𝒲.pullback c (DualNumber A)).U1) f] at h
    exact h
  · refine coefficient_transition_restrict af01 af11 afT1 p01 p11 pT1
      (inf_le_inf_right V1 inf_le_left) (inf_le_inf_right V1 inf_le_right)
      (inf_le_inf_right (𝒲'.pullback c (DualNumber A)).U1 inf_le_left)
      (inf_le_inf_right (𝒲'.pullback c (DualNumber A)).U1 inf_le_right)
      huw01 huw11
      (((XA c A).presheaf.map (homOfLE
        (inf_le_left : (W0 ⊓ W1) ⊓ V1 ≤ W0 ⊓ W1)).op).hom f) ?_
    have h := cross_identity (M := N) hF0 (oneAddEpsMul A 𝒲 c f) hM
      u01 hu01 u11 hu11
    rw [map_oneAddEpsMul 𝒲 pW01 pT1
      (inf_le_left : (W0 ⊓ W1) ⊓ V1 ≤ W0 ⊓ W1)
      (inf_le_left : ((𝒲.pullback c (DualNumber A)).U0 ⊓
        (𝒲.pullback c (DualNumber A)).U1) ⊓ (𝒲'.pullback c (DualNumber A)).U1 ≤
          (𝒲.pullback c (DualNumber A)).U0 ⊓ (𝒲.pullback c (DualNumber A)).U1) f] at h
    exact h
  · refine coefficient_transition_restrict af01 af00 afS0 p01 p00 pS0
      (inf_le_inf_left W0 inf_le_right) (inf_le_inf_left W0 inf_le_left)
      (inf_le_inf_left (𝒲.pullback c (DualNumber A)).U0 inf_le_right)
      (inf_le_inf_left (𝒲.pullback c (DualNumber A)).U0 inf_le_left)
      huw01 huw00
      (((XA c A).presheaf.map (homOfLE
        (inf_le_right : W0 ⊓ (V0 ⊓ V1) ≤ V0 ⊓ V1)).op).hom f') ?_
    have h := cross_identity' (M := N) hF0 (oneAddEpsMul A 𝒲' c f') hM'
      u00 hu00 u01 hu01
    rw [map_oneAddEpsMul 𝒲' pV01 pS0
      (inf_le_right : W0 ⊓ (V0 ⊓ V1) ≤ V0 ⊓ V1)
      (inf_le_right : (𝒲.pullback c (DualNumber A)).U0 ⊓
        ((𝒲'.pullback c (DualNumber A)).U0 ⊓ (𝒲'.pullback c (DualNumber A)).U1) ≤
          (𝒲'.pullback c (DualNumber A)).U0 ⊓ (𝒲'.pullback c (DualNumber A)).U1) f'] at h
    exact h.trans (mul_comm
      (1 + eps ((𝒲.pullback c (DualNumber A)).U0 ⊓
        ((𝒲'.pullback c (DualNumber A)).U0 ⊓ (𝒲'.pullback c (DualNumber A)).U1)) *
        ι pS0 (((XA c A).presheaf.map (homOfLE
          (inf_le_right : W0 ⊓ (V0 ⊓ V1) ≤ V0 ⊓ V1)).op).hom f'))
      (((XD c A).presheaf.map (homOfLE
        (inf_le_inf_left (𝒲.pullback c (DualNumber A)).U0 inf_le_left)).op).hom u00))
  · refine coefficient_transition_restrict af11 af10 afS1 p11 p10 pS1
      (inf_le_inf_left W1 inf_le_right) (inf_le_inf_left W1 inf_le_left)
      (inf_le_inf_left (𝒲.pullback c (DualNumber A)).U1 inf_le_right)
      (inf_le_inf_left (𝒲.pullback c (DualNumber A)).U1 inf_le_left)
      huw11 huw10
      (((XA c A).presheaf.map (homOfLE
        (inf_le_right : W1 ⊓ (V0 ⊓ V1) ≤ V0 ⊓ V1)).op).hom f') ?_
    have h := cross_identity' (M := N) hF1 (oneAddEpsMul A 𝒲' c f') hM'
      u10 hu10 u11 hu11
    rw [map_oneAddEpsMul 𝒲' pV01 pS1
      (inf_le_right : W1 ⊓ (V0 ⊓ V1) ≤ V0 ⊓ V1)
      (inf_le_right : (𝒲.pullback c (DualNumber A)).U1 ⊓
        ((𝒲'.pullback c (DualNumber A)).U0 ⊓ (𝒲'.pullback c (DualNumber A)).U1) ≤
          (𝒲'.pullback c (DualNumber A)).U0 ⊓ (𝒲'.pullback c (DualNumber A)).U1) f'] at h
    exact h.trans (mul_comm
      (1 + eps ((𝒲.pullback c (DualNumber A)).U1 ⊓
        ((𝒲'.pullback c (DualNumber A)).U0 ⊓ (𝒲'.pullback c (DualNumber A)).U1)) *
        ι pS1 (((XA c A).presheaf.map (homOfLE
          (inf_le_right : W1 ⊓ (V0 ⊓ V1) ≤ V0 ⊓ V1)).op).hom f'))
      (((XD c A).presheaf.map (homOfLE
        (inf_le_inf_left (𝒲.pullback c (DualNumber A)).U1 inf_le_left)).op).hom u10))
theorem

exists_crossSections_of_isFrameOn_of_map_eq_oneAddEpsMul_smul

L600 ↗
AlgebraicGeometry.RelPicard.exists_crossSections_of_isFrameOn_of_map_eq_oneAddEpsMul_smul
Documentation

Two frame presentations of an infinitesimal transition admit compatible cross sections.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicGeometry.RelPicard
open _root_.JacobianVarieties.Picard.Proofs.FrameCrossSections
universe u
open  _root_.CategoryTheory _root_.CategoryTheory.Limits _root_.Opposite _root_.AlgebraicGeometry
  _root_.AlgebraicGeometry.RelPicard
  _root_.NeronModelInfra _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.JacobianVarieties.Picard.Proofs.FrameCrossSections.CoverCross in
Lean source · full declaration
theorem exists_crossSections_of_isFrameOn_of_map_eq_oneAddEpsMul_smul
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R))
    (A : Type u) [CommRing A] [Algebra R A]
    [IsSeparated (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A))]
    (𝒲 𝒲' : C.TwoAffineOpenCover)
    (N : (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R (DualNumber A))).Modules)
    (e₀ : Γ(N, (𝒲.pullback c (DualNumber A)).U0)) (e₁ : Γ(N, (𝒲.pullback c (DualNumber A)).U1))
    (g : ((𝒲.pullback c A).cover (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A))).A01)
    (h₀ : Scheme.Modules.IsFrameOn e₀ (𝒲.pullback c (DualNumber A)).U0)
    (h₁ : Scheme.Modules.IsFrameOn e₁ (𝒲.pullback c (DualNumber A)).U1)
    (hg : N.presheaf.map (homOfLE inf_le_right).op e₁ =
      (show Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R (DualNumber A)),
          (𝒲.pullback c (DualNumber A)).U0 ⊓ (𝒲.pullback c (DualNumber A)).U1) from oneAddEpsMul A
            𝒲 c g) •
        N.presheaf.map (homOfLE inf_le_left).op e₀)
    (e₀' : Γ(N, (𝒲'.pullback c (DualNumber A)).U0)) (e₁' : Γ(N, (𝒲'.pullback c (DualNumber A)).U1))
    (g' : ((𝒲'.pullback c A).cover (pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A))).A01)
    (h₀' : Scheme.Modules.IsFrameOn e₀' (𝒲'.pullback c (DualNumber A)).U0)
    (h₁' : Scheme.Modules.IsFrameOn e₁' (𝒲'.pullback c (DualNumber A)).U1)
    (hg' : N.presheaf.map (homOfLE inf_le_right).op e₁' =
      (show Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R (DualNumber A)),
          (𝒲'.pullback c (DualNumber A)).U0 ⊓ (𝒲'.pullback c (DualNumber A)).U1) from oneAddEpsMul
            A 𝒲' c g') •
        N.presheaf.map (homOfLE inf_le_left).op e₀') :
    let X' := Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A)
    let W0 := (𝒲.pullback c A).U0
    let W1 := (𝒲.pullback c A).U1
    let V0 := (𝒲'.pullback c A).U0
    let V1 := (𝒲'.pullback c A).U1
    ∃ (g00 : Γ(X', W0 ⊓ V0)) (g01 : Γ(X', W0 ⊓ V1)) (g10 : Γ(X', W1 ⊓ V0)) (g11 : Γ(X', W1 ⊓ V1)),
      ((XA c A).presheaf.map (homOfLE (inf_le_inf_right V0 inf_le_left  : (W0 ⊓ W1) ⊓ V0 ≤ W0 ⊓
        V0)).op).hom g00
        = ((XA c A).presheaf.map (homOfLE (inf_le_inf_right V0 inf_le_right : (W0 ⊓ W1) ⊓ V0 ≤ W1 ⊓
          V0)).op).hom g10
          + ((XA c A).presheaf.map (homOfLE (inf_le_left : (W0 ⊓ W1) ⊓ V0 ≤ W0 ⊓ W1)).op).hom g ∧
      ((XA c A).presheaf.map (homOfLE (inf_le_inf_right V1 inf_le_left  : (W0 ⊓ W1) ⊓ V1 ≤ W0 ⊓
        V1)).op).hom g01
        = ((XA c A).presheaf.map (homOfLE (inf_le_inf_right V1 inf_le_right : (W0 ⊓ W1) ⊓ V1 ≤ W1 ⊓
          V1)).op).hom g11
          + ((XA c A).presheaf.map (homOfLE (inf_le_left : (W0 ⊓ W1) ⊓ V1 ≤ W0 ⊓ W1)).op).hom g ∧
      ((XA c A).presheaf.map (homOfLE (inf_le_inf_left W0 inf_le_right : W0 ⊓ (V0 ⊓ V1) ≤ W0 ⊓
        V1)).op).hom g01
        = ((XA c A).presheaf.map (homOfLE (inf_le_inf_left W0 inf_le_left  : W0 ⊓ (V0 ⊓ V1) ≤ W0 ⊓
          V0)).op).hom g00
          + ((XA c A).presheaf.map (homOfLE (inf_le_right : W0 ⊓ (V0 ⊓ V1) ≤ V0 ⊓ V1)).op).hom g' ∧
      ((XA c A).presheaf.map (homOfLE (inf_le_inf_left W1 inf_le_right : W1 ⊓ (V0 ⊓ V1) ≤ W1 ⊓
        V1)).op).hom g11
        = ((XA c A).presheaf.map (homOfLE (inf_le_inf_left W1 inf_le_left  : W1 ⊓ (V0 ⊓ V1) ≤ W1 ⊓
          V0)).op).hom g10
          + ((XA c A).presheaf.map (homOfLE (inf_le_right : W1 ⊓ (V0 ⊓ V1) ≤ V0 ⊓ V1)).op).hom g' :=
  CoverCross.main c A 𝒲 𝒲' N e₀ e₁ g h₀ h₁ hg e₀' e₁' g' h₀' h₁' hg'

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