NYLL
Module

RepresentsRelSubPic_exists_hom_classifies_rigidify_pullback_map_of_comp_eq_comp.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_exists_hom_classifies_rigidify_pullback_map_of_comp_eq_comp
15 declarations indexed from sourceView source ↗

Module documentation

Classifying a semilinear pullback of the Poincare bundle

A map of the curve over a split change of base induces a classifying map. The rigidified pullback construction preserves multiplication and the identity.

Imports18
Imported by1

Declarations

theorem

nonempty_pullback_fst_ofInvertible_iso

L60 ↗
JacobianVarieties.Picard.Proofs.PullbackMapExistence.P2mSemilin.nonempty_pullback_fst_ofInvertible_iso
Source context 12 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackMapExistence
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace P2mSemilin
Lean source · statement
theorem nonempty_pullback_fst_ofInvertible_iso {R : Type u} [CommRing R] {C : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of R)} {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
    {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (L : (pullback c t).Modules)
    (hL : Scheme.Modules.IsInvertible L) {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T) :
    Nonempty ((Scheme.Modules.pullback (pullback.fst (pullback.snd c t) s)).obj
      (RigidifiedLineBundle.ofInvertible (ε := ε) L hL).L ≅
      (Scheme.Modules.pullback (pullback.fst (pullback.snd c t) s)).obj L)
def

fT

L85 ↗
JacobianVarieties.Picard.Proofs.PullbackMapExistence.P2mSemilin.fT
Documentation

The base-change map induced by the curve map and the chosen splitting of the base map.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackMapExistence
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace P2mSemilin
section Transform
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  (β β' : Spec (CommRingCat.of R) ⟶ Spec (CommRingCat.of R)) (hβ : β' ≫ β = 𝟙 (Spec (CommRingCat.of
    R)))
  (f : C ⟶ C) (hf : f ≫ c = c ≫ β)
Lean source · statement
def fT {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) : pullback c (t ≫ β') ⟶ pullback c t
theorem

fT_snd

L89 ↗
JacobianVarieties.Picard.Proofs.PullbackMapExistence.P2mSemilin.fT_snd
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackMapExistence
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace P2mSemilin
section Transform
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  (β β' : Spec (CommRingCat.of R) ⟶ Spec (CommRingCat.of R)) (hβ : β' ≫ β = 𝟙 (Spec (CommRingCat.of
    R)))
  (f : C ⟶ C) (hf : f ≫ c = c ≫ β)
Lean source · statement
theorem fT_snd {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    fT β β' hβ f hf t ≫ pullback.snd c t = pullback.snd c (t ≫ β')
def

shift

L94 ↗
JacobianVarieties.Picard.Proofs.PullbackMapExistence.P2mSemilin.shift
Documentation

A morphism over the base, viewed over its composition with the chosen base splitting.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackMapExistence
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace P2mSemilin
section Transform
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  (β β' : Spec (CommRingCat.of R) ⟶ Spec (CommRingCat.of R)) (hβ : β' ≫ β = 𝟙 (Spec (CommRingCat.of
    R)))
  (f : C ⟶ C) (hf : f ≫ c = c ≫ β)
Lean source · statement
def shift {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
    (ψ : SchemeHomOver t' t) : SchemeHomOver (t' ≫ β') (t ≫ β')
theorem

fT_baseChangeSnd

L98 ↗
JacobianVarieties.Picard.Proofs.PullbackMapExistence.P2mSemilin.fT_baseChangeSnd
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackMapExistence
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace P2mSemilin
section Transform
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  (β β' : Spec (CommRingCat.of R) ⟶ Spec (CommRingCat.of R)) (hβ : β' ≫ β = 𝟙 (Spec (CommRingCat.of
    R)))
  (f : C ⟶ C) (hf : f ≫ c = c ≫ β)
Lean source · statement
theorem fT_baseChangeSnd {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)}
    (ψ : SchemeHomOver t' t) :
    fT β β' hβ f hf t' ≫ baseChangeSnd c ψ = baseChangeSnd c (shift β' ψ) ≫ fT β β' hβ f hf t
theorem

hinv

L106 ↗
JacobianVarieties.Picard.Proofs.PullbackMapExistence.P2mSemilin.hinv
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackMapExistence
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace P2mSemilin
section Transform
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  (β β' : Spec (CommRingCat.of R) ⟶ Spec (CommRingCat.of R)) (hβ : β' ≫ β = 𝟙 (Spec (CommRingCat.of
    R)))
  (f : C ⟶ C) (hf : f ≫ c = c ≫ β)
Lean source · statement
theorem hinv {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c ε t) :
    Scheme.Modules.IsInvertible ((Scheme.Modules.pullback (fT β β' hβ f hf t)).obj M.L)
def

Psi

L111 ↗
JacobianVarieties.Picard.Proofs.PullbackMapExistence.P2mSemilin.Psi
Documentation

Pull back an invertible bundle along the semilinear map and rigidify it.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackMapExistence
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace P2mSemilin
section Transform
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  (β β' : Spec (CommRingCat.of R) ⟶ Spec (CommRingCat.of R)) (hβ : β' ≫ β = 𝟙 (Spec (CommRingCat.of
    R)))
  (f : C ⟶ C) (hf : f ≫ c = c ≫ β)
Lean source · statement
def Psi {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c ε t) :
    RigidifiedLineBundle c ε (t ≫ β')
theorem

hcut

L116 ↗
JacobianVarieties.Picard.Proofs.PullbackMapExistence.P2mSemilin.hcut
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackMapExistence
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace P2mSemilin
section Transform
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
  (β β' : Spec (CommRingCat.of R) ⟶ Spec (CommRingCat.of R)) (hβ : β' ≫ β = 𝟙 (Spec (CommRingCat.of
    R)))
  (f : C ⟶ C) (hf : f ≫ c = c ≫ β)
Lean source · statement
theorem hcut {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : RigidifiedLineBundle c ε t)
    (hM : FibrewiseAlgEquivZero M) : FibrewiseAlgEquivZero (Psi (ε := ε) β β' hβ f hf t M)
theorem

nonempty_poincare_pullbackAlong_law_mul_iso

L146 ↗
JacobianVarieties.Picard.Proofs.PullbackMapExistence.P2mSemilin.nonempty_poincare_pullbackAlong_law_mul_iso
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackMapExistence
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace P2mSemilin
section Law
variable {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)
Lean source · statement
theorem nonempty_poincare_pullbackAlong_law_mul_iso {T : Scheme.{u}}
    (s : T ⟶ Spec (CommRingCat.of R))
    (x y : SchemeHomOver s D.toBase) :
    Nonempty ((h.poincare.pullbackAlong
        ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).mul s x y)).L ≅
      ((h.poincare.pullbackAlong x).tensor (h.poincare.pullbackAlong y)).L)
theorem

nonempty_poincare_pullbackAlong_law_one_iso

L156 ↗
JacobianVarieties.Picard.Proofs.PullbackMapExistence.P2mSemilin.nonempty_poincare_pullbackAlong_law_one_iso
Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackMapExistence
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace P2mSemilin
section Law
variable {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)
Lean source · statement
theorem nonempty_poincare_pullbackAlong_law_one_iso {T : Scheme.{u}}
    (s : T ⟶ Spec (CommRingCat.of R)) :
    Nonempty ((h.poincare.pullbackAlong
        ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).one s)).L ≅
      (RigidifiedLineBundle.unit (c := c) (ε := ε) s).L)
def

tw

L181 ↗
JacobianVarieties.Picard.Proofs.PullbackMapExistence.P2mSemilin.tw
Documentation

Compose a point of the representing scheme with the classifying map over the changed base.

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackMapExistence
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace P2mSemilin
section Clauses
variable {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)
  (β β' : Spec (CommRingCat.of R) ⟶ Spec (CommRingCat.of R)) (hβ : β' ≫ β = 𝟙 (Spec (CommRingCat.of
    R)))
  (f : C ⟶ C) (hf : f ≫ c = c ≫ β)
  (N : SchemeHomOver (D.toBase ≫ β') D.toBase)
  (hN : Nonempty ((h.poincare.pullbackAlong N).L ≅ (Psi (ε := ε) β β' hβ f hf D.toBase
    h.poincare).L))
Lean source · statement
def tw {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (z : SchemeHomOver t D.toBase) :
    SchemeHomOver (t ≫ β') D.toBase
theorem

keyA

L186 ↗
JacobianVarieties.Picard.Proofs.PullbackMapExistence.P2mSemilin.keyA
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackMapExistence
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace P2mSemilin
section Clauses
variable {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)
  (β β' : Spec (CommRingCat.of R) ⟶ Spec (CommRingCat.of R)) (hβ : β' ≫ β = 𝟙 (Spec (CommRingCat.of
    R)))
  (f : C ⟶ C) (hf : f ≫ c = c ≫ β)
  (N : SchemeHomOver (D.toBase ≫ β') D.toBase)
  (hN : Nonempty ((h.poincare.pullbackAlong N).L ≅ (Psi (ε := ε) β β' hβ f hf D.toBase
    h.poincare).L))
include hN in
Lean source · statement
theorem keyA {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver t D.toBase) :
    Nonempty ((h.poincare.pullbackAlong (tw β' N a)).L ≅ (Psi (ε := ε) β β' hβ f hf t
      (h.poincare.pullbackAlong a)).L)
theorem

keyB

L209 ↗
JacobianVarieties.Picard.Proofs.PullbackMapExistence.P2mSemilin.keyB
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackMapExistence
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace P2mSemilin
section Clauses
variable {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)
  (β β' : Spec (CommRingCat.of R) ⟶ Spec (CommRingCat.of R)) (hβ : β' ≫ β = 𝟙 (Spec (CommRingCat.of
    R)))
  (f : C ⟶ C) (hf : f ≫ c = c ≫ β)
  (N : SchemeHomOver (D.toBase ≫ β') D.toBase)
  (hN : Nonempty ((h.poincare.pullbackAlong N).L ≅ (Psi (ε := ε) β β' hβ f hf D.toBase
    h.poincare).L))
include hN in
Lean source · statement
theorem keyB {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t D.toBase) :
    tw β' N ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).mul t x y) =
      (RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).mul (t ≫ β') (tw β'
        N x) (tw β' N y)
theorem

keyC

L235 ↗
JacobianVarieties.Picard.Proofs.PullbackMapExistence.P2mSemilin.keyC
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PullbackMapExistence
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace P2mSemilin
section Clauses
variable {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)
  (β β' : Spec (CommRingCat.of R) ⟶ Spec (CommRingCat.of R)) (hβ : β' ≫ β = 𝟙 (Spec (CommRingCat.of
    R)))
  (f : C ⟶ C) (hf : f ≫ c = c ≫ β)
  (N : SchemeHomOver (D.toBase ≫ β') D.toBase)
  (hN : Nonempty ((h.poincare.pullbackAlong N).L ≅ (Psi (ε := ε) β β' hβ f hf D.toBase
    h.poincare).L))
include hN in
Lean source · statement
theorem keyC {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    tw β' N ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).one t) =
      (RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).one (t ≫ β')
theorem

exists_hom_classifies_rigidify_pullback_map_of_comp_eq_comp

L272 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.exists_hom_classifies_rigidify_pullback_map_of_comp_eq_comp
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicGeometry.RelPicard.RepresentsRelSubPic
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 JacobianVarieties.Picard.Proofs.PullbackMapExistence
universe u
open P2mSemilin in
Lean source · full declaration
theorem exists_hom_classifies_rigidify_pullback_map_of_comp_eq_comp
    {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)
    (β β' : Spec (CommRingCat.of R) ⟶ Spec (CommRingCat.of R))
    (hβ : β' ≫ β = 𝟙 (Spec (CommRingCat.of R)))
    (f : C ⟶ C) (hf : f ≫ c = c ≫ β) :
    ∃ N : SchemeHomOver (D.toBase ≫ β') D.toBase,
      (∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver t D.toBase),
        Nonempty ((h.poincare.pullbackAlong
            (⟨a.1 ≫ N.1, by rw [Category.assoc, N.2, ← Category.assoc, a.2]⟩ :
              SchemeHomOver (t ≫ β') D.toBase)).L ≅
          Scheme.Modules.rigidify (rigSection c (t ≫ β') ε) (pullback.snd c (t ≫ β'))
            ((Scheme.Modules.pullback
                (pullback.map c (t ≫ β') c t f (𝟙 T) β hf.symm
                  (by rw [Category.assoc, hβ, Category.comp_id, Category.id_comp]))).obj
              (h.poincare.pullbackAlong a).L))) ∧
      (∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t D.toBase),
        (⟨((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).mul t x y).1 ≫
          N.1,
            by
              rw [Category.assoc, N.2, ← Category.assoc,
                ((RepresentsRelSubPic.relativeGroupLaw
                  (P := algEquivZeroGroupCut c ε) h).mul t x y).2]⟩ :
            SchemeHomOver (t ≫ β') D.toBase) =
          (RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).mul (t ≫ β')
            ⟨x.1 ≫ N.1, by rw [Category.assoc, N.2, ← Category.assoc, x.2]⟩
            ⟨y.1 ≫ N.1, by rw [Category.assoc, N.2, ← Category.assoc, y.2]⟩) ∧
      (∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)),
        ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).one t).1 ≫ N.1 =
          ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).one (t ≫
            β')).1) := by
  let N : SchemeHomOver (D.toBase ≫ β') D.toBase :=
    h.classify (D.toBase ≫ β') (Psi (ε := ε) β β' hβ f hf D.toBase h.poincare)
      (hcut (ε := ε) β β' hβ f hf D.toBase h.poincare h.poincare_mem)
  have hN : Nonempty ((h.poincare.pullbackAlong N).L ≅ (Psi (ε := ε) β β' hβ f hf D.toBase
    h.poincare).L) :=
    h.classify_spec _ _ _
  refine ⟨N, fun t a => ?_, fun t x y => ?_, fun t => ?_⟩
  · exact keyA h β β' hβ f hf N hN t a
  · exact keyB h β β' hβ f hf N hN t x y
  · exact congrArg Subtype.val (keyC h β β' hβ f hf N hN t)

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