AlgebraicGeometry.RelPicard.RepresentsRelSubPic.postComp_transport_comp_fst_eq_comp_transport_of_baseChangeIso
Source context 13 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.RelPicard
attribute [-instance] SheafOfModules.isIso_ihomModelToIhom
attribute [-simp]
AlgebraicGeometry.Scheme.Modules.tensorSections_zero_right
AlgebraicGeometry.Scheme.Modules.map_unitSection
AlgebraicGeometry.Scheme.Modules.tensorSectionsBilin_apply
AlgebraicGeometry.Scheme.Modules.tensorPowSection_zero
AlgebraicGeometry.Scheme.Modules.tensorSections_zero_left
AlgebraicGeometry.Scheme.Modules.tensorPow_zero
AlgebraicGeometry.Scheme.Modules.tensorPow_succ
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
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.SmoothProperCurve
universe uLean source · statement
theorem RepresentsRelSubPic.postComp_transport_comp_fst_eq_comp_transport_of_baseChangeIso
{R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
{ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
{D : RelativePic0Designation R c} (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
(R' : Type u) [CommRing R'] [Algebra R R']
(hR : RepresentsRelSubPic (baseChange R c R') (sectionBaseChange R' ε)
(algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε)) (D.baseChange R'))
(hPR : Nonempty (hR.poincare.L ≅ (BaseChange.ofR c ε R'
(h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R R'), pullback.condition⟩)).L))
(W : C ≅ C) (hW' : W.inv ≫ c = c)
(W' : pullback c (specMap R R') ≅ pullback c (specMap R R'))
(hW'₁ : W'.hom ≫ pullback.fst c (specMap R R') = pullback.fst c (specMap R R') ≫ W.hom)
(hW'₂' : W'.inv ≫ baseChange R c R' = baseChange R c R')
(θ : SchemeHomOver D.toBase D.toBase)
(hθ : (∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
(M : RigidifiedLineBundle c ε t) (hM : FibrewiseAlgEquivZero M)
(N : RigidifiedLineBundle c ε t) (hN : FibrewiseAlgEquivZero N)
(Q : T.Modules), Scheme.Modules.IsInvertible Q →
Nonempty (N.L ≅ (Scheme.Modules.pullback (curveChange (c := c) (c' := c) W.inv hW' t)).obj
M.L ⊗
(Scheme.Modules.pullback (pullback.snd c t)).obj Q) →
postComp θ (h.classify t M hM) = h.classify t N hN))
(θ' : SchemeHomOver (D.baseChange R').toBase (D.baseChange R').toBase)
(hθ' : (∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R'))
(M : RigidifiedLineBundle (baseChange R c R') (sectionBaseChange R' ε) t) (hM :
FibrewiseAlgEquivZero M)
(N : RigidifiedLineBundle (baseChange R c R') (sectionBaseChange R' ε) t) (hN :
FibrewiseAlgEquivZero N)
(Q : T.Modules), Scheme.Modules.IsInvertible Q →
Nonempty (N.L ≅
(Scheme.Modules.pullback (curveChange (c := baseChange R c R')
(c' := baseChange R c R') W'.inv hW'₂' t)).obj M.L ⊗
(Scheme.Modules.pullback (pullback.snd (baseChange R c R') t)).obj Q) →
postComp θ' (hR.classify t M hM) = hR.classify t N hN)) :
∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R')) (v : SchemeHomOver t (D.baseChange
R').toBase),
(postComp θ' v).1 ≫ pullback.fst D.toBase (specMap R R') = (v.1 ≫ pullback.fst D.toBase
(specMap R R')) ≫ θ.1