RepresentsRelSubPic_kerPointsToRigKer_bijective.lean

theorem fibrewiseAlgEquivZero_of_pullbackAlong_iso_unit_aux
    {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
    {T T₀ : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t₀ : T₀ ⟶ Spec (CommRingCat.of R)}
    (ψ : SchemeHomOver t₀ t)
    (hψ : ∀ (k : Type u) [Field k] [IsAlgClosed k] (s : Spec (CommRingCat.of k) ⟶ T),
      ∃ s₀ : Spec (CommRingCat.of k) ⟶ T₀, s₀ ≫ ψ.1 = s)
    (M : RigidifiedLineBundle c ε t)
    (hM : Nonempty ((M.pullbackAlong ψ).L ≅ (RigidifiedLineBundle.unit (c := c) (ε := ε) t₀).L)) :
    FibrewiseAlgEquivZero M

theorem ker_restrict_iff_and_exists_unique_and_mul_aux
    {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)
    {T T₀ : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (t₀ : T₀ ⟶ Spec (CommRingCat.of R))
    (ψ : SchemeHomOver t₀ t)
    (hψ : ∀ (k : Type u) [Field k] [IsAlgClosed k] (s : Spec (CommRingCat.of k) ⟶ T),
      ∃ s₀ : Spec (CommRingCat.of k) ⟶ T₀, s₀ ≫ ψ.1 = s) :
    let L := RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h
    (∀ x : SchemeHomOver t D.toBase,
      GoodReductionJacobian.schemeHomOverComp ψ.1 ψ.2 x = L.one t₀ ↔
        Nonempty (((h.poincare.pullbackAlong x).pullbackAlong ψ).L ≅
          (RigidifiedLineBundle.unit (c := c) (ε := ε) t₀).L)) ∧
    (∀ M : RigidifiedLineBundle c ε t,
      Nonempty ((M.pullbackAlong ψ).L ≅ (RigidifiedLineBundle.unit (c := c) (ε := ε) t₀).L) →
        ∃! x : SchemeHomOver t D.toBase, Nonempty ((h.poincare.pullbackAlong x).L ≅ M.L)) ∧
    (∀ x y : SchemeHomOver t D.toBase,
      Nonempty ((h.poincare.pullbackAlong (L.mul t x y)).L ≅
        ((h.poincare.pullbackAlong x).tensor (h.poincare.pullbackAlong y)).L)) := by
  intro L
  let := RepresentsRelSubPic.grpObj (P := algEquivZeroGroupCut c ε) h
  refine ⟨fun x => ?_, fun M hM => ?_, fun x y => ?_⟩
  · let := (algEquivZeroGroupCut c ε).commGroupObj (Opposite.op (Over.mk t₀))
    have h1 := congrArg Subtype.val
      (RepresentsRelSubPic.homEquiv_one (P := algEquivZeroGroupCut c ε) h (Over.mk t₀))
    have one_iso : Nonempty ((h.poincare.pullbackAlong
        (L.one t₀)).L ≅
          (RigidifiedLineBundle.unit (c := c) (ε := ε) t₀).L) :=
      Quotient.exact h1
    have comp_iso : ((h.poincare.pullbackAlong x).pullbackAlong ψ).L ≅
        (h.poincare.pullbackAlong (GoodReductionJacobian.schemeHomOverComp ψ.1 ψ.2 x)).L :=
      h.poincare.pullbackAlongPullbackAlongIso x ψ
    constructor
    · intro hx
      rw [← hx] at one_iso
      exact ⟨comp_iso ≪≫ one_iso.some⟩
    · rintro ⟨e⟩
      exact h.ext_of_iso t₀ _ _ ⟨comp_iso.symm ≪≫ e ≪≫ one_iso.some.symm⟩
  · exact h.univ t M (fibrewiseAlgEquivZero_of_pullbackAlong_iso_unit_aux ψ hψ M hM)
  · let := (algEquivZeroGroupCut c ε).commGroupObj (Opposite.op (Over.mk t))
    have hm := congrArg Subtype.val
      (RepresentsRelSubPic.homEquiv_mul (P := algEquivZeroGroupCut c ε) h (Over.mk t)
        (schemeHomOverToOverHom x) (schemeHomOverToOverHom y))
    exact Quotient.exact hm

theorem _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic.kerPointsToRigKer_bijective
    {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} {D : RelativePic0Designation R c}
    (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D) (A : Type u) [CommRing A] [Algebra R A] :
    Function.Bijective (h.kerPointsToRigKer A)