AlgebraicGeometry.RelPicard.RepresentsRelSubPic.nonempty_poincare_pullbackAlong_pow_iso_tensorPow
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.RelPicard.RepresentsRelSubPic
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open scoped CategoryTheory.MonObjLean source · full declaration
theorem nonempty_poincare_pullbackAlong_pow_iso_tensorPow
{R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
{ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
{P : SubPicGroupCondition c ε} {D : RelativePic0Designation R c}
(h : RepresentsRelSubPic c ε P.toSubPicCondition D)
{T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver t D.toBase) (n : ℕ) :
let _ := h.relativeGroupLaw.pointGroup t
Nonempty ((h.poincare.pullbackAlong (a ^ n)).L ≅
(h.poincare.pullbackAlong a).L.tensorPow n) := by
intro pointGroup
have hmul : ∀ x y : SchemeHomOver t D.toBase,
Nonempty ((h.poincare.pullbackAlong (x * y)).L ≅
(h.poincare.pullbackAlong x).L ⊗ (h.poincare.pullbackAlong y).L) := by
intro x y
let := h.grpObj
obtain ⟨e⟩ := h.nonempty_poincare_pullbackAlong_mul_iso (T := Over.mk t)
(schemeHomOverToOverHom x) (schemeHomOverToOverHom y)
exact ⟨e⟩
have hone : Nonempty ((h.poincare.pullbackAlong (1 : SchemeHomOver t D.toBase)).L ≅ 𝟙_ _) := by
let := h.grpObj
obtain ⟨e⟩ := h.nonempty_poincare_pullbackAlong_one_iso (Over.mk t)
exact ⟨e⟩
induction n with
| zero =>
rw [pow_zero]
exact hone
| succ n ih =>
obtain ⟨e1⟩ := hmul (a ^ n) a
obtain ⟨e2⟩ := ih
rw [pow_succ]
exact ⟨e1 ≪≫ (e2 ⊗ᵢ Iso.refl _)⟩