Module

Exists_trivialModDeformations_map_H1_tensor_natural.lean

Nyll.JacobianVarieties.Picard.Exists_trivialModDeformations_map_H1_tensor_natural

59 declarations indexed from sourceView source ↗

Module documentation

Trivial module deformations and first cohomology

Construct the cohomology classification on two affine charts and prove its naturality.

Imports13

Imported by2

theorem

app_map

L83 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.app_map

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Generic
variable {X Y : Scheme.{u}}

Lean source · statement

theorem app_map {M N : X.Modules} (φ : M ⟶ N) {W₁ W₂ : X.Opens} (i : W₁ ⟶ W₂) (x : Γ(M, W₂)) :
    φ.app W₁ (M.presheaf.map i.op x) = N.presheaf.map i.op (φ.app W₂ x)

def

isoSections

L88 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.isoSections

Documentation

The linear equivalence on sections induced by an isomorphism of module sheaves.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Generic
variable {X Y : Scheme.{u}}

Lean source · full declaration

def isoSections {L L' : X.Modules} (φ : L ≅ L') (U : X.Opens) : Γ(L, U) ≃ₗ[Γ(X, U)] Γ(L', U) where
  toFun := φ.hom.app U
  invFun := φ.inv.app U
  map_add' x y := map_add _ x y
  map_smul' r x := Scheme.Modules.Hom.app_smul _ r x
  left_inv x := by
    change (φ.hom.app U ≫ φ.inv.app U) x = x
    rw [← Scheme.Modules.Hom.comp_app, Iso.hom_inv_id, Scheme.Modules.Hom.id_app]; rfl
  right_inv x := by
    change (φ.inv.app U ≫ φ.hom.app U) x = x
    rw [← Scheme.Modules.Hom.comp_app, Iso.inv_hom_id, Scheme.Modules.Hom.id_app]; rfl

def

pullbackObjIsoOfEq

L101 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.pullbackObjIsoOfEq

Documentation

The comparison of pullbacks induced by an equality of scheme morphisms.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Generic
variable {X Y : Scheme.{u}}

Lean source · statement

def pullbackObjIsoOfEq {f g : X ⟶ Y} (h : f = g) (M : Y.Modules) :
    (Scheme.Modules.pullback f).obj M ≅ (Scheme.Modules.pullback g).obj M

def

pullbackObjCompIso

L106 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.pullbackObjCompIso

Documentation

The comparison from pullback along a composite to iterated pullback.

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Generic
variable {X Y : Scheme.{u}}

Lean source · statement

def pullbackObjCompIso {Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (M : Z.Modules) :
    (Scheme.Modules.pullback (f ≫ g)).obj M ≅
      (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback g).obj M)

theorem

nonempty_pullback_iso_unit

L111 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.nonempty_pullback_iso_unit

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Generic
variable {X Y : Scheme.{u}}

Lean source · statement

theorem nonempty_pullback_iso_unit (f : X ⟶ Y) {M : Y.Modules}
    (h : Nonempty (M ≅ SheafOfModules.unit Y.ringCatSheaf)) :
    Nonempty ((Scheme.Modules.pullback f).obj M ≅ SheafOfModules.unit X.ringCatSheaf)

theorem

nonempty_iso_unit_of_isIso_pullback

L116 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.nonempty_iso_unit_of_isIso_pullback

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Generic
variable {X Y : Scheme.{u}}

Lean source · statement

theorem nonempty_iso_unit_of_isIso_pullback (f : X ⟶ Y) [IsIso f] {M : Y.Modules}
    (h : Nonempty ((Scheme.Modules.pullback f).obj M ≅ SheafOfModules.unit X.ringCatSheaf)) :
    Nonempty (M ≅ SheafOfModules.unit Y.ringCatSheaf)

theorem

nonempty_iso_unit_of_isLocalRing

L125 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.nonempty_iso_unit_of_isLocalRing

Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Generic
variable {X Y : Scheme.{u}}

Lean source · statement

theorem nonempty_iso_unit_of_isLocalRing {R : Type u} [CommRing R] [IsLocalRing R]
    {N : (Spec (CommRingCat.of R)).Modules} (hN : Scheme.Modules.IsInvertible N) :
    Nonempty (N ≅ SheafOfModules.unit (Spec (CommRingCat.of R)).ringCatSheaf)

def

GluedBy

L138 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.GluedBy

Documentation

Local trivializations whose restrictions are related by the specified transition unit.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Generic
variable {X Y : Scheme.{u}}
variable {R : Type u} [CommRing R] (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · statement

def GluedBy (L : X.Modules) (t : (𝒱.cover c).A01ˣ) : Prop

theorem

gluedBy_unit_one

L145 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.gluedBy_unit_one

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Generic
variable {X Y : Scheme.{u}}
variable {R : Type u} [CommRing R] (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · statement

theorem gluedBy_unit_one : GluedBy 𝒱 c (SheafOfModules.unit X.ringCatSheaf) 1

theorem

gluedBy_of_iso

L149 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.gluedBy_of_iso

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Generic
variable {X Y : Scheme.{u}}
variable {R : Type u} [CommRing R] (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · statement

theorem gluedBy_of_iso {L L' : X.Modules} (φ : L ≅ L') {t : (𝒱.cover c).A01ˣ}
    (h : GluedBy 𝒱 c L t) :
    GluedBy 𝒱 c L' t

theorem

gluedBy_iff_of_iso

L167 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.gluedBy_iff_of_iso

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Generic
variable {X Y : Scheme.{u}}
variable {R : Type u} [CommRing R] (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · statement

theorem gluedBy_iff_of_iso {L L' : X.Modules} (φ : L ≅ L') (t : (𝒱.cover c).A01ˣ) :
    GluedBy 𝒱 c L t ↔ GluedBy 𝒱 c L' t

theorem

nonempty_iso_iff_of_gluedBy

L171 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.nonempty_iso_iff_of_gluedBy

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Generic
variable {X Y : Scheme.{u}}
variable {R : Type u} [CommRing R] (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · statement

theorem nonempty_iso_iff_of_gluedBy {L L' : X.Modules} (hL : Scheme.Modules.IsInvertible L)
    (hL' : Scheme.Modules.IsInvertible L') {t t' : (𝒱.cover c).A01ˣ} (h : GluedBy 𝒱 c L t)
    (h' : GluedBy 𝒱 c L' t') :
    Nonempty (L ≅ L') ↔ ∃ (a0 : (𝒱.cover c).A0ˣ) (a1 : (𝒱.cover c).A1ˣ),
      (t' : (𝒱.cover c).A01) =
        (𝒱.cover c).ρ0 (a0 : (𝒱.cover c).A0) * t *
          (𝒱.cover c).ρ1 ((a1⁻¹ : (𝒱.cover c).A1ˣ) : (𝒱.cover c).A1)

theorem

exists_gluedBy

L183 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.exists_gluedBy

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Generic
variable {X Y : Scheme.{u}}
variable {R : Type u} [CommRing R] (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))

Lean source · statement

theorem exists_gluedBy (t : (𝒱.cover c).A01ˣ) :
    ∃ L : X.Modules, Scheme.Modules.IsInvertible L ∧ GluedBy 𝒱 c L t

theorem

exists_chartIsos

L222 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.exists_chartIsos

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover in

Lean source · statement

theorem exists_chartIsos :
    ∃ (e0 : (A ⊗[K] (𝒱.cover c).A0) ≃ₐ[A]
        ((𝒱.pullback c A).cover (pullback.snd c (specMap K A))).A0)
      (e1 : (A ⊗[K] (𝒱.cover c).A1) ≃ₐ[A]
        ((𝒱.pullback c A).cover (pullback.snd c (specMap K A))).A1)
      (e01 : (A ⊗[K] (𝒱.cover c).A01) ≃ₐ[A]
        ((𝒱.pullback c A).cover (pullback.snd c (specMap K A))).A01),
      (∀ s, e0 ((1 : A) ⊗ₜ[K] s) = ((pullback.fst c (specMap K A)).app 𝒱.U0).hom s) ∧
      (∀ s, e1 ((1 : A) ⊗ₜ[K] s) = ((pullback.fst c (specMap K A)).app 𝒱.U1).hom s) ∧
      (∀ s, e01 ((1 : A) ⊗ₜ[K] s) = ((pullback.fst c (specMap K A)).app (𝒱.U0 ⊓ 𝒱.U1)).hom s)

def

E0

L237 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.E0

Documentation

Base extension identified with sections on the first base changed chart.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]

Lean source · statement

def E0 : (A ⊗[K] (𝒱.cover c).A0) ≃ₐ[A]
    ((𝒱.pullback c A).cover (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))).A0

def

E1

L242 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.E1

Documentation

Base extension identified with sections on the second base changed chart.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]

Lean source · statement

def E1 : (A ⊗[K] (𝒱.cover c).A1) ≃ₐ[A]
    ((𝒱.pullback c A).cover (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))).A1

def

E01

L247 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.E01

Documentation

The algebra equivalence identifying base extension with sections on the chart overlap.

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]

Lean source · statement

def E01 : (A ⊗[K] (𝒱.cover c).A01) ≃ₐ[A]
    ((𝒱.pullback c A).cover (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))).A01

theorem

E0_tmul

L251 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.E0_tmul

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]

Lean source · statement

theorem E0_tmul (s : (𝒱.cover c).A0) : E0 𝒱 c A ((1 : A) ⊗ₜ[K] s) =
    ((pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)).app 𝒱.U0).hom s

theorem

E1_tmul

L255 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.E1_tmul

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]

Lean source · statement

theorem E1_tmul (s : (𝒱.cover c).A1) : E1 𝒱 c A ((1 : A) ⊗ₜ[K] s) =
    ((pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)).app 𝒱.U1).hom s

theorem

E01_tmul

L259 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.E01_tmul

Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]

Lean source · statement

theorem E01_tmul (s : (𝒱.cover c).A01) : E01 𝒱 c A ((1 : A) ⊗ₜ[K] s) =
    ((pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)).app (𝒱.U0 ⊓ 𝒱.U1)).hom s

theorem

tmul_eq_mul

L270 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.tmul_eq_mul

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)

Lean source · statement

theorem tmul_eq_mul (a : A) {B : Type u} [CommRing B] [Algebra K B] (s : B) :
    a ⊗ₜ[K] s = (a ⊗ₜ[K] (1 : B)) * ((1 : A) ⊗ₜ[K] s)

theorem

E0_tmul_one

L274 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.E0_tmul_one

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)

Lean source · statement

theorem E0_tmul_one (a : A) : E0 𝒱 c A (a ⊗ₜ[K] 1) = algebraMap A (𝒰[A]).A0 a

theorem

E1_tmul_one

L277 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.E1_tmul_one

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)

Lean source · statement

theorem E1_tmul_one (a : A) : E1 𝒱 c A (a ⊗ₜ[K] 1) = algebraMap A (𝒰[A]).A1 a

theorem

E01_tmul_one

L280 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.E01_tmul_one

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)

Lean source · statement

theorem E01_tmul_one (a : A) : E01 𝒱 c A (a ⊗ₜ[K] 1) = algebraMap A (𝒰[A]).A01 a

theorem

E01_map_ρ0

L283 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.E01_map_ρ0

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)

Lean source · statement

theorem E01_map_ρ0 (x : A ⊗[K] (𝒱.cover c).A0) :
    E01 𝒱 c A (Algebra.TensorProduct.map (AlgHom.id K A) (𝒱.cover c).ρ0 x) =
      (𝒰[A]).ρ0 (E0 𝒱 c A x)

theorem

E01_map_ρ1

L298 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.E01_map_ρ1

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)

Lean source · statement

theorem E01_map_ρ1 (x : A ⊗[K] (𝒱.cover c).A1) :
    E01 𝒱 c A (Algebra.TensorProduct.map (AlgHom.id K A) (𝒱.cover c).ρ1 x) =
      (𝒰[A]).ρ1 (E1 𝒱 c A x)

theorem

appLE_congrHom

L318 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.appLE_congrHom

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
variable (A' : Type u) [CommRing A'] [Algebra K A'] [Algebra A A'] [IsScalarTower K A A']
local notation "σ[" A "," A' "]" =>
  RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom K (IsScalarTower.toAlgHom K A A'))

Lean source · statement

theorem appLE_congrHom {X' Y' : Scheme.{u}} {f g : X' ⟶ Y'} (h : f = g)
    (U : Y'.Opens) (V : X'.Opens)
    (e : V ≤ f ⁻¹ᵁ U) (e' : V ≤ g ⁻¹ᵁ U) : f.appLE U V e = g.appLE U V e'

theorem

baseChangeSnd_snd

L323 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.baseChangeSnd_snd

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
variable (A' : Type u) [CommRing A'] [Algebra K A'] [Algebra A A'] [IsScalarTower K A A']
local notation "σ[" A "," A' "]" =>
  RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom K (IsScalarTower.toAlgHom K A A'))

Lean source · statement

theorem baseChangeSnd_snd {T T' : Scheme.{u}} {t : T ⟶ Spec (.of K)} {t' : T' ⟶ Spec (.of K)}
    (s : SchemeHomOver t' t) : baseChangeSnd c s ≫ pullback.snd c t = pullback.snd c t' ≫ s.1

theorem

stage_le

L328 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.stage_le

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
variable (A' : Type u) [CommRing A'] [Algebra K A'] [Algebra A A'] [IsScalarTower K A A']
local notation "σ[" A "," A' "]" =>
  RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom K (IsScalarTower.toAlgHom K A A'))

Lean source · statement

theorem stage_le : p[A'] ⁻¹ᵁ (𝒱.U0 ⊓ 𝒱.U1) ≤ σ[A,A'] ⁻¹ᵁ (p[A] ⁻¹ᵁ (𝒱.U0 ⊓ 𝒱.U1))

theorem

stage_appLE_fst_app

L331 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.stage_appLE_fst_app

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
variable (A' : Type u) [CommRing A'] [Algebra K A'] [Algebra A A'] [IsScalarTower K A A']
local notation "σ[" A "," A' "]" =>
  RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom K (IsScalarTower.toAlgHom K A A'))

Lean source · statement

theorem stage_appLE_fst_app (s : (𝒱.cover c).A01) :
    ((σ[A,A']).appLE ((𝒱[A]).U0 ⊓ (𝒱[A]).U1) ((𝒱[A']).U0 ⊓ (𝒱[A']).U1)
        (Scheme.TwoAffineOpenCover.baseChangeSnd_preimage_inf 𝒱 c
          (RelPicard.LFP.stageHom K (IsScalarTower.toAlgHom K A A'))).ge).hom
      (((p[A]).app (𝒱.U0 ⊓ 𝒱.U1)).hom s) = ((p[A']).app (𝒱.U0 ⊓ 𝒱.U1)).hom s

theorem

stage_appLE_algebraMap

L346 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.stage_appLE_algebraMap

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
variable (A' : Type u) [CommRing A'] [Algebra K A'] [Algebra A A'] [IsScalarTower K A A']
local notation "σ[" A "," A' "]" =>
  RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom K (IsScalarTower.toAlgHom K A A'))

Lean source · statement

theorem stage_appLE_algebraMap (a : A) :
    ((σ[A,A']).appLE ((𝒱[A]).U0 ⊓ (𝒱[A]).U1) ((𝒱[A']).U0 ⊓ (𝒱[A']).U1)
        (Scheme.TwoAffineOpenCover.baseChangeSnd_preimage_inf 𝒱 c
          (RelPicard.LFP.stageHom K (IsScalarTower.toAlgHom K A A'))).ge).hom
      (algebraMap A (𝒰[A]).A01 a) = algebraMap A' (𝒰[A']).A01 (algebraMap A A' a)

theorem

stage_appLE_E01

L391 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.stage_appLE_E01

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section Charts
variable {K : Type u} [CommRing K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover)
    (c : C ⟶ Spec (.of K))
variable (A : Type u) [CommRing A] [Algebra K A]
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
variable (A' : Type u) [CommRing A'] [Algebra K A'] [Algebra A A'] [IsScalarTower K A A']
local notation "σ[" A "," A' "]" =>
  RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom K (IsScalarTower.toAlgHom K A A'))
local notation "σ♯[" A "," A' "]" =>
  CommRingCat.Hom.hom (Scheme.Hom.appLE
    (RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom K (IsScalarTower.toAlgHom K A A')))
    (Scheme.TwoAffineOpenCover.U0 (Scheme.TwoAffineOpenCover.pullback 𝒱 c A) ⊓
      Scheme.TwoAffineOpenCover.U1 (Scheme.TwoAffineOpenCover.pullback 𝒱 c A))
    (Scheme.TwoAffineOpenCover.U0 (Scheme.TwoAffineOpenCover.pullback 𝒱 c A') ⊓
      Scheme.TwoAffineOpenCover.U1 (Scheme.TwoAffineOpenCover.pullback 𝒱 c A'))
    (Eq.ge (Scheme.TwoAffineOpenCover.baseChangeSnd_preimage_inf 𝒱 c
      (RelPicard.LFP.stageHom K (IsScalarTower.toAlgHom K A A')))))

Lean source · statement

theorem stage_appLE_E01 (x : A ⊗[K] (𝒱.cover c).A01) :
    (σ♯[A,A']) (E01 𝒱 c A x) =
      E01 𝒱 c A' (Algebra.TensorProduct.map (IsScalarTower.toAlgHom K A A')
        (AlgHom.id K (𝒱.cover c).A01) x)

def

Nset

L445 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.Nset

Documentation

Transition units reducing to one that realize the given line bundle on the two charts.

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))

Lean source · statement

def Nset (L : (pullback c (Scheme.TwoAffineOpenCover.specMap K 𝔸[V])).Modules) :
    Set ((𝔸[V] ⊗[K] (𝒱.cover c).A01)ˣ)

def

βmod

L451 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.βmod

Documentation

The cohomology class of the infinitesimal part of a transition unit for the module.

Source context 23 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))
open Classical in

Lean source · statement

def βmod (L : (pullback c (Scheme.TwoAffineOpenCover.specMap K 𝔸[V])).Modules) :
    (𝒱.structureSheafSections c).H1 ⊗[K] V

theorem

coe_mapEquiv_symm_inv

L456 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.coe_mapEquiv_symm_inv

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))

Lean source · statement

theorem coe_mapEquiv_symm_inv {M N : Type u} [Monoid M] [Monoid N] (h : M ≃* N) (a : Nˣ) :
    (((Units.mapEquiv h.symm a)⁻¹ : Mˣ) : M) = h.symm ((a⁻¹ : Nˣ) : N)

theorem

cobd_transport

L460 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.cobd_transport

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))

Lean source · statement

theorem cobd_transport (τ τ' : (𝔸[V] ⊗[K] (𝒱.cover c).A01)ˣ)
    (a0 : (𝒰[𝔸[V]]).A0ˣ) (a1 : (𝒰[𝔸[V]]).A1ˣ)
    (h : ((u[V] τ' : (𝒰[𝔸[V]]).A01ˣ) : (𝒰[𝔸[V]]).A01) =
      (𝒰[𝔸[V]]).ρ0 (a0 : (𝒰[𝔸[V]]).A0) * (u[V] τ : (𝒰[𝔸[V]]).A01ˣ) *
        (𝒰[𝔸[V]]).ρ1 ((a1⁻¹ : (𝒰[𝔸[V]]).A1ˣ) : (𝒰[𝔸[V]]).A1)) :
    ∃ (b0 : (𝔸[V] ⊗[K] (𝒱.cover c).A0)ˣ) (b1 : (𝔸[V] ⊗[K] (𝒱.cover c).A1)ˣ),
      (τ' : 𝔸[V] ⊗[K] (𝒱.cover c).A01) =
        Algebra.TensorProduct.map (AlgHom.id K 𝔸[V]) (𝒱.cover c).ρ0
          (b0 : 𝔸[V] ⊗[K] (𝒱.cover c).A0) *
          (τ : 𝔸[V] ⊗[K] (𝒱.cover c).A01) *
        Algebra.TensorProduct.map (AlgHom.id K 𝔸[V]) (𝒱.cover c).ρ1
          ((↑(b1⁻¹) : 𝔸[V] ⊗[K] (𝒱.cover c).A1))

theorem

cobd_transport'

L482 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.cobd_transport'

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))

Lean source · statement

theorem cobd_transport' (τ τ' : (𝔸[V] ⊗[K] (𝒱.cover c).A01)ˣ) (b0 : (𝔸[V] ⊗[K] (𝒱.cover c).A0)ˣ)
    (b1 : (𝔸[V] ⊗[K] (𝒱.cover c).A1)ˣ)
    (h : (τ' : 𝔸[V] ⊗[K] (𝒱.cover c).A01) =
        Algebra.TensorProduct.map (AlgHom.id K 𝔸[V]) (𝒱.cover c).ρ0
          (b0 : 𝔸[V] ⊗[K] (𝒱.cover c).A0) *
          (τ : 𝔸[V] ⊗[K] (𝒱.cover c).A01) *
        Algebra.TensorProduct.map (AlgHom.id K 𝔸[V]) (𝒱.cover c).ρ1
          ((↑(b1⁻¹) : 𝔸[V] ⊗[K] (𝒱.cover c).A1))) :
    ∃ (a0 : (𝒰[𝔸[V]]).A0ˣ) (a1 : (𝒰[𝔸[V]]).A1ˣ),
      ((u[V] τ' : (𝒰[𝔸[V]]).A01ˣ) : (𝒰[𝔸[V]]).A01) =
      (𝒰[𝔸[V]]).ρ0 (a0 : (𝒰[𝔸[V]]).A0) * (u[V] τ : (𝒰[𝔸[V]]).A01ˣ) *
        (𝒰[𝔸[V]]).ρ1 ((a1⁻¹ : (𝒰[𝔸[V]]).A1ˣ) : (𝒰[𝔸[V]]).A1)

theorem

cls_eq_of_mem_Nset

L503 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.cls_eq_of_mem_Nset

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))

Lean source · statement

theorem cls_eq_of_mem_Nset {L : (pullback c (Scheme.TwoAffineOpenCover.specMap K 𝔸[V])).Modules}
    (hL : Scheme.Modules.IsInvertible L) {τ τ' : (𝔸[V] ⊗[K] (𝒱.cover c).A01)ˣ}
    (hτ : τ ∈ Nset 𝒱 c V L)
    (hτ' : τ' ∈ Nset 𝒱 c V L) :
    cls[V] (vp[V] (τ : 𝔸[V] ⊗[K] (𝒱.cover c).A01)) =
      cls[V] (vp[V] (τ' : 𝔸[V] ⊗[K] (𝒱.cover c).A01))

theorem

βmod_eq_of_mem

L516 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.βmod_eq_of_mem

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))

Lean source · statement

theorem βmod_eq_of_mem {L : (pullback c (Scheme.TwoAffineOpenCover.specMap K 𝔸[V])).Modules}
    (hL : Scheme.Modules.IsInvertible L) {τ : (𝔸[V] ⊗[K] (𝒱.cover c).A01)ˣ}
    (hτ : τ ∈ Nset 𝒱 c V L) :
    βmod 𝒱 c V L = cls[V] (vp[V] (τ : 𝔸[V] ⊗[K] (𝒱.cover c).A01))

theorem

Nset_iso

L524 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.Nset_iso

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))

Lean source · statement

theorem Nset_iso {L L' : (pullback c (Scheme.TwoAffineOpenCover.specMap K 𝔸[V])).Modules}
    (φ : L ≅ L') :
    Nset 𝒱 c V L = Nset 𝒱 c V L'

theorem

isNilpotent_kerIdeal

L530 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.isNilpotent_kerIdeal

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))

Lean source · statement

theorem isNilpotent_kerIdeal : IsNilpotent (TrivSqZeroExt.kerIdeal K V)

def

gJ

L534 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.gJ

Documentation

The comparison from the reduction by the square zero ideal to the original family.

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))

Lean source · statement

def gJ :
    pullback (q[𝔸[V]])
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (TrivSqZeroExt.kerIdeal K V)))) ⟶
    pullback c (𝟙 (Spec (CommRingCat.of K)))

theorem

quot_comp

L541 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.quot_comp

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))

Lean source · statement

theorem quot_comp :
    CommRingCat.ofHom (TrivSqZeroExt.fstHom K K V).toRingHom ≫
      CommRingCat.ofHom (algebraMap K 𝔸[V]) ≫
        CommRingCat.ofHom (Ideal.Quotient.mk (TrivSqZeroExt.kerIdeal K V)) =
      CommRingCat.ofHom (Ideal.Quotient.mk (TrivSqZeroExt.kerIdeal K V))

theorem

gJ_comp_i

L554 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.gJ_comp_i

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))

Lean source · statement

theorem gJ_comp_i :
    gJ c V ≫ baseChangeSnd c (SquareZero.basePointOver K V) =
      pullback.fst (q[𝔸[V]])
        (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (TrivSqZeroExt.kerIdeal K V))))

theorem

nonempty_Nset

L571 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.nonempty_Nset

Source context 23 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))
open _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible in

Lean source · full declaration

theorem nonempty_Nset (L : TrivialModDeformations c ε V) :
    (Nset 𝒱 c V
      (show (pullback c (Scheme.TwoAffineOpenCover.specMap K 𝔸[V])).Modules
        from L.1.L)).Nonempty := by
  have hJ : Nonempty ((Scheme.Modules.pullback (pullback.fst (q[𝔸[V]])
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (TrivSqZeroExt.kerIdeal K V)))))).obj L.1.L ≅
      SheafOfModules.unit (pullback (q[𝔸[V]])
          (Spec.map
            (CommRingCat.ofHom (Ideal.Quotient.mk (TrivSqZeroExt.kerIdeal K V))))).ringCatSheaf) :=
    ⟨pullbackObjIsoOfEq (gJ_comp_i c V).symm _ ≪≫ pullbackObjCompIso _ _ _ ≪≫
      (Scheme.Modules.pullback (gJ c V)).mapIso L.2.some ≪≫ Scheme.Modules.pullbackUnitIso _⟩
  obtain ⟨a, ha, e0, e1, e01, he0, he1⟩ :=
    exists_sectionsOf_equiv_lineBundle_one_add_of_pullback_quotient_isNilpotent
      (TrivSqZeroExt.kerIdeal K V) (isNilpotent_kerIdeal V) (q[𝔸[V]]) (𝒱[𝔸[V]]) L.1.isInvertible hJ
  have ha2 : IsNilpotent a := by
    refine ⟨2, ?_⟩
    have := Ideal.pow_mem_pow ha 2
    rwa [← Ideal.map_pow, TrivSqZeroExt.kerIdeal_sq, Ideal.map_bot, Ideal.mem_bot] at this
  let tL : (𝒰[𝔸[V]]).A01ˣ := ha2.isUnit_one_add.unit
  have htL : (tL : (𝒰[𝔸[V]]).A01) = 1 + a := rfl
  have hglued : GluedBy (𝒱[𝔸[V]]) (q[𝔸[V]]) L.1.L tL :=
    ⟨e0, e1, e01, he0, fun y => by rw [htL]; exact he1 y⟩
  refine ⟨(u[V]).symm tL, ?_, ?_⟩
  · have hcoe : (((u[V]).symm tL : (𝔸[V] ⊗[K] (𝒱.cover c).A01)ˣ) : 𝔸[V] ⊗[K] (𝒱.cover c).A01) =
        (E01 𝒱 c 𝔸[V]).symm (1 + a) := by rw [Units.mapEquiv_symm]; rfl
    rw [hcoe, map_add, map_one, map_add, map_one, add_eq_left]
    have hle : Ideal.map (algebraMap 𝔸[V] (𝒰[𝔸[V]]).A01) (TrivSqZeroExt.kerIdeal K V) ≤
        RingHom.ker ((red[V] : 𝔸[V] ⊗[K] (𝒱.cover c).A01 →+* (𝒱.cover c).A01).comp
          ((E01 𝒱 c 𝔸[V]).symm : (𝒰[𝔸[V]]).A01 →+* 𝔸[V] ⊗[K] (𝒱.cover c).A01)) := by
      rw [Ideal.map_le_iff_le_comap]
      intro j hj
      rw [Ideal.mem_comap, RingHom.mem_ker, RingHom.comp_apply]
      change red[V] ((E01 𝒱 c 𝔸[V]).symm (algebraMap 𝔸[V] (𝒰[𝔸[V]]).A01 j)) = 0
      rw [(E01 𝒱 c 𝔸[V]).symm.commutes j, Algebra.TensorProduct.algebraMap_apply,
        Algebra.algebraMap_self_apply,
        Algebra.TensorProduct.lift_tmul, AlgHom.id_apply, mul_one, AlgHom.comp_apply]
      change algebraMap K _ ((TrivSqZeroExt.fstHom K K V) j) = 0
      rw [TrivSqZeroExt.kerIdeal, RingHom.mem_ker] at hj
      rw [hj, map_zero]
    have := hle ha
    rwa [RingHom.mem_ker, RingHom.comp_apply] at this
  · change GluedBy (𝒱[𝔸[V]]) (q[𝔸[V]]) L.1.L ((u[V]) ((u[V]).symm tL))
    rwa [MulEquiv.apply_symm_apply]

def

βfun

L616 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.βfun

Documentation

The first cohomology class associated to a trivial module deformation.

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))

Lean source · statement

def βfun (L : TrivialModDeformations c ε V) : (𝒱.structureSheafSections c).H1 ⊗[K] V

theorem

βfun_eq_iff

L619 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.βfun_eq_iff

Source context 22 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))

Lean source · statement

theorem βfun_eq_iff (L L' : TrivialModDeformations c ε V) :
    βfun 𝒱 c ε V L = βfun 𝒱 c ε V L' ↔ Nonempty (L.1.L ≅ L'.1.L)

def

algK

L643 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.algK

Documentation

The scalar action of the square zero extension on its residue field via the first projection.

Source context 23 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))
section Reduce

Lean source · statement

def algK : Algebra 𝔸[V] K

theorem

isScalarTower_algK

L647 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.isScalarTower_algK

Source context 24 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))
section Reduce
attribute [local instance] algK

Lean source · statement

theorem isScalarTower_algK : IsScalarTower K 𝔸[V] K

theorem

lid_map_fst

L655 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.lid_map_fst

Source context 26 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))
section Reduce
attribute [local instance] algK
attribute [local instance] isScalarTower_algK
local notation "σK[" V "]" =>
  RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom K (IsScalarTower.toAlgHom K 𝔸[V] K))

Lean source · statement

theorem lid_map_fst (x : 𝔸[V] ⊗[K] (𝒱.cover c).A01) :
    Algebra.TensorProduct.lid K (𝒱.cover c).A01
      (Algebra.TensorProduct.map (IsScalarTower.toAlgHom K 𝔸[V] K)
          (AlgHom.id K (𝒱.cover c).A01) x) = red[V] x

def

jj

L669 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.jj

Documentation

The comparison between the self base change by the scalar map and by the identity.

Source context 26 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))
section Reduce
attribute [local instance] algK
attribute [local instance] isScalarTower_algK
local notation "σK[" V "]" =>
  RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom K (IsScalarTower.toAlgHom K 𝔸[V] K))

Lean source · statement

def jj :
    pullback c (Scheme.TwoAffineOpenCover.specMap K K) ⟶ pullback c (𝟙 (Spec (CommRingCat.of K)))

instance

(anonymous instance)

L674 ↗

Source context 26 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))
section Reduce
attribute [local instance] algK
attribute [local instance] isScalarTower_algK
local notation "σK[" V "]" =>
  RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom K (IsScalarTower.toAlgHom K 𝔸[V] K))

Lean source · statement

instance : IsIso (jj c)

theorem

jj_comp_i

L678 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.jj_comp_i

Source context 26 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))
section Reduce
attribute [local instance] algK
attribute [local instance] isScalarTower_algK
local notation "σK[" V "]" =>
  RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom K (IsScalarTower.toAlgHom K 𝔸[V] K))

Lean source · statement

theorem jj_comp_i : jj c ≫ baseChangeSnd c (SquareZero.basePointOver K V) = σK[V]

theorem

βfun_surjective

L682 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.βfun_surjective

Source context 26 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))
section Reduce
attribute [local instance] algK
attribute [local instance] isScalarTower_algK
local notation "σK[" V "]" =>
  RelPicard.baseChangeSnd c (RelPicard.LFP.stageHom K (IsScalarTower.toAlgHom K 𝔸[V] K))

Lean source · statement

theorem βfun_surjective : Function.Surjective (βfun 𝒱 c ε V)

theorem

red_map

L732 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.red_map

Source context 24 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))
section Natural
variable {V W}

Lean source · full declaration

theorem red_map (φ : V →ₗ[K] W) (x : 𝔸[V] ⊗[K] (𝒱.cover c).A01) :
    let : Algebra 𝔸[V] 𝔸[W] := (TrivSqZeroExt.map φ).toRingHom.toAlgebra
    let : IsScalarTower K 𝔸[V] 𝔸[W] :=
      IsScalarTower.of_algebraMap_eq fun k => ((TrivSqZeroExt.map φ).commutes k).symm
    red[W] (Algebra.TensorProduct.map (IsScalarTower.toAlgHom K 𝔸[V] 𝔸[W])
        (AlgHom.id K (𝒱.cover c).A01) x) =
      red[V] x := by
  intro baseChangeAlgebra baseChangeTower
  induction x using TensorProduct.inductionOn with
  | add x y hx hy => simp only [map_add, hx, hy]
  | tmul a s =>
    rw [Algebra.TensorProduct.map_tmul,
      Algebra.TensorProduct.lift_tmul, Algebra.TensorProduct.lift_tmul,
      AlgHom.id_apply, IsScalarTower.toAlgHom_apply]
    congr 1
    change algebraMap K _ ((TrivSqZeroExt.map φ a).fst) = algebraMap K _ a.fst
    rw [TrivSqZeroExt.fst_map]

theorem

vp_map

L750 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.vp_map

Source context 24 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))
section Natural
variable {V W}

Lean source · full declaration

theorem vp_map (φ : V →ₗ[K] W) (x : 𝔸[V] ⊗[K] (𝒱.cover c).A01) :
    let : Algebra 𝔸[V] 𝔸[W] := (TrivSqZeroExt.map φ).toRingHom.toAlgebra
    let : IsScalarTower K 𝔸[V] 𝔸[W] :=
      IsScalarTower.of_algebraMap_eq fun k => ((TrivSqZeroExt.map φ).commutes k).symm
    vp[W] (Algebra.TensorProduct.map (IsScalarTower.toAlgHom K 𝔸[V] 𝔸[W])
        (AlgHom.id K (𝒱.cover c).A01) x) =
      LinearMap.lTensor (𝒱.cover c).A01 φ (vp[V] x) := by
  intro baseChangeAlgebra baseChangeTower
  induction x using TensorProduct.inductionOn with
  | add x y hx hy => simp only [map_add, hx, hy]
  | tmul a s =>
    simp only [Algebra.TensorProduct.map_tmul, AlgHom.id_apply, IsScalarTower.toAlgHom_apply,
      TensorProduct.map_tmul, LinearMap.id_apply, LinearEquiv.coe_coe, TensorProduct.comm_tmul,
      LinearMap.lTensor_tmul]
    congr 1
    change (TrivSqZeroExt.map φ a).snd = φ a.snd
    rw [TrivSqZeroExt.snd_map]

theorem

cls_lTensor

L769 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.cls_lTensor

Source context 25 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))
section Natural
variable {V W}
omit [Module Kᵐᵒᵖ V] [IsCentralScalar K V] [Module Kᵐᵒᵖ W] [IsCentralScalar K W] in

Lean source · statement

theorem cls_lTensor (φ : V →ₗ[K] W) (y : (𝒱.cover c).A01 ⊗[K] V) :
    cls[W] (LinearMap.lTensor (𝒱.cover c).A01 φ y) = LinearMap.lTensor _ φ (cls[V] y)

theorem

βfun_map

L774 ↗

JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural.P2mTJ2.βfun_map

Source context 24 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Exists_trivialModDeformations_map_H1_tensor_natural
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.tilde.functorCompPullbackSpecIso_app
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_hom_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.relSubPicPresheafRestrictIso_inv_app_coe
  AlgebraicGeometry.RelPicard.BaseChange.restrict_P
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.injEq
  AlgebraicGeometry.RelPicard.SubPicCondition.mk.sizeOf_spec
  AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.sizeOf_spec
  GoodReductionJacobian.AvatarSchemeBridge.mk.injEq
  GoodReductionJacobian.AvatarSchemeBridge.mk.sizeOf_spec
  GoodReductionJacobian.RelativePic0Designation.mk.injEq GoodReductionJacobian.schemeHomOverComp_coe
  NeronModelInfra.schemeHomOverEquivOverHom_apply
  GoodReductionJacobian.RelativeGroupLaw.mk.sizeOf_spec
  NeronModelInfra.schemeHomOverEquivOverHom_symm_apply NeronModelInfra.overHomToSchemeHomOver_coe
  GoodReductionJacobian.RelativeGroupLaw.mk.injEq
  NeronModelInfra.overHomToSchemeHomOver_schemeHomOverToOverHom
  NeronModelInfra.schemeHomOverToOverHom_left
  NeronModelInfra.schemeHomOverToOverHom_overHomToSchemeHomOver
  AlgebraicGeometry.RelPicard.SubPicCondition.onClasses_mk
  AlgebraicGeometry.RelPicard.relSubPicPresheaf_map_coe
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
  AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra TrivSqZeroExt
noncomputable section
namespace P2mTJ2
section SquareZero
variable {K : Type u} [Field K] {C : Scheme.{u}} (𝒱 : C.TwoAffineOpenCover) (c : C ⟶ Spec (.of K))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c)
variable (V : Type u) [AddCommGroup V] [Module K V] [Module Kᵐᵒᵖ V] [IsCentralScalar K V]
variable (W : Type u) [AddCommGroup W] [Module K W] [Module Kᵐᵒᵖ W] [IsCentralScalar K W]
local notation "𝔸[" V "]" => TrivSqZeroExt K V
local notation "𝒰[" A "]" =>
  Scheme.TwoAffineOpenCover.cover (Scheme.TwoAffineOpenCover.pullback 𝒱 c A)
  (pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A))
local notation "𝒱[" A "]" => Scheme.TwoAffineOpenCover.pullback 𝒱 c A
local notation "p[" A "]" => pullback.fst c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "q[" A "]" => pullback.snd c (Scheme.TwoAffineOpenCover.specMap K A)
local notation "red[" V "]" => Algebra.TensorProduct.lift
  (AlgHom.comp (Algebra.ofId K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TrivSqZeroExt.fstHom K K V))
  (AlgHom.id K (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (fun _ _ => Commute.all _ _)
local notation "vp[" V "]" => (fun x =>
  LinearEquiv.toLinearMap
    (TensorProduct.comm K V (TwoChartCech.Cover.A01 (Scheme.TwoAffineOpenCover.cover 𝒱 c)))
    (TensorProduct.map (TrivSqZeroExt.sndHom K V) LinearMap.id x))
local notation "cls[" V "]" => LinearMap.rTensor V
  (Submodule.mkQ (LinearMap.range (TwoChartCech.Sections.cechDiff
    (TwoChartCech.Cover.structureSheaf (Scheme.TwoAffineOpenCover.cover 𝒱 c)))))
local notation "u[" V "]" => Units.mapEquiv (AlgEquiv.toMulEquiv (E01 𝒱 c 𝔸[V]))
section Natural
variable {V W}

Lean source · statement

theorem βfun_map (φ : V →ₗ[K] W) (L : TrivialModDeformations c ε V) :
    βfun 𝒱 c ε W (L.map φ) =
      LinearMap.lTensor ((𝒱.structureSheafSections c).H1) φ (βfun 𝒱 c ε V L)

theorem