NYLL
Module

IsDeformationClassMap_apply_baseTransport_eq_H1baseChangeMap.lean

Nyll.JacobianVarieties.Picard.IsDeformationClassMap_apply_baseTransport_eq_H1baseChangeMap
13 declarations indexed from sourceView source ↗

Module documentation

Base transport of dual-number deformation classes

Compare the dual-number cover maps and their induced first-cohomology classes.

Imports11
Imported by2

Declarations

def

fεhom

L65 ↗
JacobianVarieties.Picard.Proofs.DeformationBaseTransport.T1Sol.fεhom
Documentation

The comparison morphism between the two iterated dual-number base changes.

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationBaseTransport
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace T1Sol
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K] (𝒲 : C.TwoAffineOpenCover)
Lean source · statement
def fεhom :
    Limits.pullback (baseChange R c K) (specMap K (DualNumber K)) ⟶ Limits.pullback c (specMap R
      (DualNumber K))
theorem

fεhom_fst

L71 ↗
JacobianVarieties.Picard.Proofs.DeformationBaseTransport.T1Sol.fεhom_fst
Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationBaseTransport
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace T1Sol
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K] (𝒲 : C.TwoAffineOpenCover)
Lean source · statement
theorem fεhom_fst :
    fεhom c K ≫ pullback.fst c (specMap R (DualNumber K)) =
      pullback.fst (baseChange R c K) (specMap K (DualNumber K)) ≫ pullback.fst c (specMap R K)
theorem

fεhom_snd

L82 ↗
JacobianVarieties.Picard.Proofs.DeformationBaseTransport.T1Sol.fεhom_snd
Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationBaseTransport
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace T1Sol
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K] (𝒲 : C.TwoAffineOpenCover)
Lean source · statement
theorem fεhom_snd :
    fεhom c K ≫ pullback.snd c (specMap R (DualNumber K)) =
      pullback.snd (baseChange R c K) (specMap K (DualNumber K))
def

fε

L94 ↗
JacobianVarieties.Picard.Proofs.DeformationBaseTransport.T1Sol.fε
Documentation

The comparison morphism with its compatible two-affine-cover data.

Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationBaseTransport
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace T1Sol
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K] (𝒲 : C.TwoAffineOpenCover)
Lean source · full declaration
def fε :
    Scheme.TwoAffineOpenCover.HomOver (RingHom.id (DualNumber K)) (𝒲.pullback c (DualNumber K))
      (pullback.snd c (specMap R (DualNumber K)))
      ((𝒲.pullback c K).pullback (baseChange R c K) (DualNumber K))
      (pullback.snd (baseChange R c K) (specMap K (DualNumber K))) where
  hom := fεhom c K
  comm := by
    rw [fεhom_snd, CommRingCat.ofHom_id, Spec.map_id, Category.comp_id]
  U0_le := by
    rw [Scheme.TwoAffineOpenCover.pullback_U0, Scheme.TwoAffineOpenCover.pullback_U0,
      Scheme.TwoAffineOpenCover.pullback_U0, ← Scheme.Hom.comp_preimage, ←
        Scheme.Hom.comp_preimage, fεhom_fst]
  U1_le := by
    rw [Scheme.TwoAffineOpenCover.pullback_U1, Scheme.TwoAffineOpenCover.pullback_U1,
      Scheme.TwoAffineOpenCover.pullback_U1, ← Scheme.Hom.comp_preimage, ←
        Scheme.Hom.comp_preimage, fεhom_fst]
theorem

fε_hom

L111 ↗
JacobianVarieties.Picard.Proofs.DeformationBaseTransport.T1Sol.fε_hom
Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationBaseTransport
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace T1Sol
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K] (𝒲 : C.TwoAffineOpenCover)
Lean source · statement
theorem fε_hom : (fε c K 𝒲).hom = fεhom c K
theorem

thickening_hom

L113 ↗
JacobianVarieties.Picard.Proofs.DeformationBaseTransport.T1Sol.thickening_hom
Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationBaseTransport
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace T1Sol
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K] (𝒲 : C.TwoAffineOpenCover)
Lean source · statement
theorem thickening_hom {C' : Scheme.{u}} {R' : Type u} [CommRing R'] (c' : C' ⟶ Spec (.of R'))
    (A : Type u) [CommRing A]
    [Algebra R' A] (𝒱 : C'.TwoAffineOpenCover) :
    (dualNumberThickening A 𝒱 c').hom =
      RelPicard.baseChangeSnd c' (RelPicard.LFP.stageHom R' (IsScalarTower.toAlgHom R' A
        (DualNumber A)))
theorem

baseChange_hom

L120 ↗
JacobianVarieties.Picard.Proofs.DeformationBaseTransport.T1Sol.baseChange_hom
Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationBaseTransport
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace T1Sol
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K] (𝒲 : C.TwoAffineOpenCover)
Lean source · statement
theorem baseChange_hom {C' : Scheme.{u}} {R' : Type u} [CommRing R'] (c' : C' ⟶ Spec (.of R'))
    (A : Type u) [CommRing A]
    [Algebra R' A] (𝒱 : C'.TwoAffineOpenCover) :
    (Scheme.TwoAffineOpenCover.HomOver.baseChange 𝒱 c' A).hom = pullback.fst c' (specMap R' A)
theorem

fε_comm_thickening

L126 ↗
JacobianVarieties.Picard.Proofs.DeformationBaseTransport.T1Sol.fε_comm_thickening
Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationBaseTransport
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace T1Sol
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K] (𝒲 : C.TwoAffineOpenCover)
Lean source · statement
theorem fε_comm_thickening :
    fεhom c K ≫ (dualNumberThickening K 𝒲 c).hom =
      (dualNumberThickening K (𝒲.pullback c K) (baseChange R c K)).hom ≫
        (Scheme.TwoAffineOpenCover.HomOver.baseChange (𝒲.pullback c K) (baseChange R c K) K).hom
theorem

map01_comm_sq

L164 ↗
JacobianVarieties.Picard.Proofs.DeformationBaseTransport.T1Sol.map01_comm_sq
Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationBaseTransport
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace T1Sol
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K] (𝒲 : C.TwoAffineOpenCover)
Lean source · statement
theorem map01_comm_sq
    {R₁ R₂ R₃ R₄ : Type u} [CommRing R₁] [CommRing R₂] [CommRing R₃] [CommRing R₄]
    {τ₁ : R₁ →+* R₂} {τ₂ : R₂ →+* R₄} {τ₃ : R₁ →+* R₃} {τ₄ : R₃ →+* R₄}
    {X₁ X₂ X₃ X₄ : Scheme.{u}} {𝒱₁ : X₁.TwoAffineOpenCover} {𝒱₂ : X₂.TwoAffineOpenCover}
    {𝒱₃ : X₃.TwoAffineOpenCover} {𝒱₄ : X₄.TwoAffineOpenCover}
    {c₁ : X₁ ⟶ Spec (.of R₁)} {c₂ : X₂ ⟶ Spec (.of R₂)} {c₃ : X₃ ⟶ Spec (.of R₃)} {c₄ : X₄ ⟶ Spec
      (.of R₄)}
    (tX : Scheme.TwoAffineOpenCover.HomOver τ₁ 𝒱₁ c₁ 𝒱₂ c₂) (fX : Scheme.TwoAffineOpenCover.HomOver
      τ₂ 𝒱₂ c₂ 𝒱₄ c₄)
    (fK : Scheme.TwoAffineOpenCover.HomOver τ₃ 𝒱₁ c₁ 𝒱₃ c₃) (tY : Scheme.TwoAffineOpenCover.HomOver
      τ₄ 𝒱₃ c₃ 𝒱₄ c₄)
    (h : fX.hom ≫ tX.hom = tY.hom ≫ fK.hom) (x : (𝒱₁.cover c₁).A01) :
    fX.map01 (tX.map01 x) = tY.map01 (fK.map01 x)
theorem

fεhom_def

L188 ↗
JacobianVarieties.Picard.Proofs.DeformationBaseTransport.T1Sol.fεhom_def
Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationBaseTransport
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace T1Sol
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K] (𝒲 : C.TwoAffineOpenCover)
Lean source · statement
theorem fεhom_def :
    fεhom c K = (BaseChange.κ c K (specMap K (DualNumber K))).hom ≫
      RelPicard.baseChangeSnd c (BaseTransport.idOver (RigKerDualNumber.tower_dualNumber K K))
theorem

fε_comm_thickening'

L193 ↗
JacobianVarieties.Picard.Proofs.DeformationBaseTransport.T1Sol.fε_comm_thickening'
Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationBaseTransport
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace T1Sol
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K] (𝒲 : C.TwoAffineOpenCover)
Lean source · statement
theorem fε_comm_thickening' :
    (fε c K 𝒲).hom ≫ (dualNumberThickening K 𝒲 c).hom =
      (dualNumberThickening K (𝒲.pullback c K) (baseChange R c K)).hom ≫
        (Scheme.TwoAffineOpenCover.HomOver.baseChange (𝒲.pullback c K) (baseChange R c K) K).hom
theorem

fε_map01_oneAddEpsMul

L200 ↗
JacobianVarieties.Picard.Proofs.DeformationBaseTransport.T1Sol.fε_map01_oneAddEpsMul
Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationBaseTransport
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
namespace T1Sol
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K] (𝒲 : C.TwoAffineOpenCover)
Lean source · statement
theorem fε_map01_oneAddEpsMul (f : ((𝒲.pullback c K).cover (pullback.snd c (specMap R K))).A01) :
    (fε c K 𝒲).map01 (oneAddEpsMul K 𝒲 c f) =
      oneAddEpsMul K (𝒲.pullback c K) (baseChange R c K)
        ((Scheme.TwoAffineOpenCover.HomOver.baseChange (𝒲.pullback c K) (baseChange R c K) K).map01
          f)
theorem

apply_baseTransport_eq_H1baseChangeMap

L226 ↗
AlgebraicGeometry.RelPicard.IsDeformationClassMap.apply_baseTransport_eq_H1baseChangeMap
Source context 7 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DeformationBaseTransport
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
  PresheafOfModules.InternalHom.IsSheafAux.appAt_toPresheafHom
  SheafOfModules.ihomSectionsEquivFamily_unit
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_apply SheafOfModules.ihomEval_unit_app
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_right
  AlgebraicGeometry.Scheme.Modules.ihomEval_zero_left
  AlgebraicGeometry.Scheme.Modules.homOfFamily_app_apply SheafOfModules.unit_ihomSectionsEquivFamily
  AlgebraicGeometry.Scheme.Modules.familyOfHom_app
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_hom_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictUnitIso_inv_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomOfFamily_app_apply
  AlgebraicGeometry.Scheme.Modules.restrictHomEquivFamily_symm_apply
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
open T1Sol in
Lean source · statement
theorem
  _root_.AlgebraicGeometry.RelPicard.IsDeformationClassMap.apply_baseTransport_eq_H1baseChangeMap
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙 (Spec
      (.of R))) c)
    (K : Type u) [CommRing K] [Algebra R K] (𝒲 : C.TwoAffineOpenCover)
    {δ : RigKerDualNumber c ε K → H1StructureSheaf c K 𝒲}
    {δ' : RigKerDualNumber (baseChange R c K) (sectionBaseChange K ε) K →
      H1StructureSheaf (baseChange R c K) K (𝒲.pullback c K)}
    (hδ : IsDeformationClassMap c ε K 𝒲 δ)
    (hδ' : IsDeformationClassMap (baseChange R c K) (sectionBaseChange K ε) K (𝒲.pullback c K) δ')
    (m : RigKerDualNumber c ε K) :
    δ' (RigKerDualNumber.baseTransport K c ε K m) =
      Scheme.TwoAffineOpenCover.H1baseChangeMap (𝒲.pullback c K) (baseChange R c K) K (δ m)

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