Module

RigKerDualNumber_existsUnique_kerPoint_baseChange_comp_fst_eq.lean

Nyll.JacobianVarieties.Picard.RigKerDualNumber_existsUnique_kerPoint_baseChange_comp_fst_eq

13 declarations indexed from sourceView source ↗

Module documentation

Base change of points in the dual-number kernel

Transport points along the pullback defining the base-changed Picard carrier. Compatibility with multiplication and the identity gives the unique lift in the dual-number kernel.

Imports5

Imported by2

def

castBase

L78 ↗

JacobianVarieties.Picard.Proofs.DualKer.AlgebraicGeometry.RelPicard.BaseTransport.castBase

Documentation

Transport a point over an equality of structure morphisms.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DualKer
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry

Lean source · statement

def castBase {B Y X : Scheme.{u}} {s s' : Y ⟶ B} {f : X ⟶ B} (e : s = s') (a : SchemeHomOver s f) :
    SchemeHomOver s' f

theorem

castBase_coe

L82 ↗

JacobianVarieties.Picard.Proofs.DualKer.AlgebraicGeometry.RelPicard.BaseTransport.castBase_coe

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DualKer
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry

Lean source · statement

theorem castBase_coe {B Y X : Scheme.{u}} {s s' : Y ⟶ B} {f : X ⟶ B} (e : s = s')
    (a : SchemeHomOver s f) : (castBase e a).1 = a.1

theorem

mul_castBase

L85 ↗

JacobianVarieties.Picard.Proofs.DualKer.AlgebraicGeometry.RelPicard.BaseTransport.mul_castBase

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DualKer
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry

Lean source · statement

theorem mul_castBase {R : Type u} [CommRing R] {A T : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
    (G : RelativeGroupLaw R f) {s s' : T ⟶ Spec (CommRingCat.of R)} (e : s = s')
    (a b : SchemeHomOver s f) :
    G.mul s' (castBase e a) (castBase e b) = castBase e (G.mul s a b)

def

liftPt

L92 ↗

JacobianVarieties.Picard.Proofs.DualKer.AlgebraicGeometry.RelPicard.BaseTransport.liftPt

Documentation

Lift a point to the pullback defining the base-changed Picard carrier.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DualKer
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry

Lean source · statement

def liftPt {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    (D : RelativePic0Designation R c) (R' : Type u) [CommRing R'] [Algebra R R']
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R'))
    (a : SchemeHomOver (t ≫ specMap R R') D.toBase) :
    SchemeHomOver t (D.baseChange R').toBase

theorem

liftPt_fst

L99 ↗

JacobianVarieties.Picard.Proofs.DualKer.AlgebraicGeometry.RelPicard.BaseTransport.liftPt_fst

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DualKer
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry

Lean source · statement

theorem liftPt_fst {R : Type u} [CommRing R] {C : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of R)}
    (D : RelativePic0Designation R c) (R' : Type u) [CommRing R'] [Algebra R R']
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R'))
    (a : SchemeHomOver (t ≫ specMap R R') D.toBase) :
    (liftPt D R' t a).1 ≫ pullback.fst D.toBase (specMap R R') = a.1

theorem

eq_liftPt

L107 ↗

JacobianVarieties.Picard.Proofs.DualKer.AlgebraicGeometry.RelPicard.BaseTransport.eq_liftPt

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DualKer
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry

Lean source · statement

theorem eq_liftPt {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    (D : RelativePic0Designation R c) (R' : Type u) [CommRing R'] [Algebra R R']
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R'))
    (z : SchemeHomOver t (D.baseChange R').toBase)
    (a : SchemeHomOver (t ≫ specMap R R') D.toBase)
    (hz : z.1 ≫ pullback.fst D.toBase (specMap R R') = a.1) : z = liftPt D R' t a

theorem

liftPt_mul

L118 ↗

JacobianVarieties.Picard.Proofs.DualKer.AlgebraicGeometry.RelPicard.BaseTransport.liftPt_mul

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DualKer
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry

Lean source · statement

theorem liftPt_mul {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']
    (h' : RepresentsRelSubPic (baseChange R c R') (sectionBaseChange R' ε)
      (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε)) (D.baseChange R'))
    (hP : Nonempty (h'.poincare.L ≅ (BaseChange.ofR c ε R'
      (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R R'), pullback.condition⟩)).L))
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R'))
    (a b : SchemeHomOver (t ≫ specMap R R') D.toBase) :
    liftPt D R' t ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).mul
        (t ≫ specMap R R') a b) =
      (RepresentsRelSubPic.relativeGroupLaw
        (P := algEquivZeroGroupCut (baseChange R c R') (sectionBaseChange R' ε)) h').mul t
        (liftPt D R' t a) (liftPt D R' t b)

theorem

one_castBase

L139 ↗

JacobianVarieties.Picard.Proofs.DualKer.AlgebraicGeometry.RelPicard.BaseTransport.one_castBase

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DualKer
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry

Lean source · statement

theorem one_castBase {R : Type u} [CommRing R] {A T : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
    (G : RelativeGroupLaw R f) {s s' : T ⟶ Spec (CommRingCat.of R)} (e : s = s') :
    castBase e (G.one s) = G.one s'

theorem

eq_one_of_mul_self

L144 ↗

JacobianVarieties.Picard.Proofs.DualKer.AlgebraicGeometry.RelPicard.BaseTransport.eq_one_of_mul_self

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DualKer
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry

Lean source · statement

theorem eq_one_of_mul_self {R : Type u} [CommRing R]
    {A T : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)} (G : RelativeGroupLaw R f)
    (t : T ⟶ Spec (CommRingCat.of R)) (u : SchemeHomOver t f) (hu : G.mul t u u = u) :
    u = G.one t

theorem

liftPt_one

L157 ↗

JacobianVarieties.Picard.Proofs.DualKer.AlgebraicGeometry.RelPicard.BaseTransport.liftPt_one

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DualKer
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry

Lean source · statement

theorem liftPt_one {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']
    (h' : RepresentsRelSubPic (baseChange R c R') (sectionBaseChange R' ε)
      (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε)) (D.baseChange R'))
    (hP : Nonempty (h'.poincare.L ≅ (BaseChange.ofR c ε R'
      (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R R'), pullback.condition⟩)).L))
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R')) :
    liftPt D R' t ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).one
        (t ≫ specMap R R')) =
      (RepresentsRelSubPic.relativeGroupLaw
        (P := algEquivZeroGroupCut (baseChange R c R') (sectionBaseChange R' ε)) h').one t

theorem

comp_liftPt_coe

L173 ↗

JacobianVarieties.Picard.Proofs.DualKer.AlgebraicGeometry.RelPicard.BaseTransport.comp_liftPt_coe

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DualKer
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry

Lean source · full declaration

theorem comp_liftPt_coe {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    (D : RelativePic0Designation R c) (R' : Type u) [CommRing R'] [Algebra R R']
    {T T₀ : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R')) (t₀ : T₀ ⟶ Spec (CommRingCat.of R'))
    (g : T₀ ⟶ T) (hg : g ≫ t = t₀) (a : SchemeHomOver (t ≫ specMap R R') D.toBase) :
    g ≫ (liftPt D R' t a).1 =
      (liftPt D R' t₀ ⟨g ≫ a.1, by rw [Category.assoc, a.2, ← Category.assoc, hg]⟩).1 := by
  have := eq_liftPt D R' t₀
    ⟨g ≫ (liftPt D R' t a).1, by rw [Category.assoc, (liftPt D R' t a).2, hg]⟩
    ⟨g ≫ a.1, by rw [Category.assoc, a.2, ← Category.assoc, hg]⟩
    (by rw [Category.assoc, liftPt_fst])
  exact congrArg Subtype.val this

theorem

dualNumberReduction_comp_liftPt_eq_one

L234 ↗

JacobianVarieties.Picard.Proofs.DualKer.AlgebraicGeometry.RelPicard.RigKerDualNumber.dualNumberReduction_comp_liftPt_eq_one

Source context 23 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DualKer
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
attribute [local simp] castBase_coe
attribute [local simp] liftPt_fst
namespace AlgebraicGeometry
namespace RelPicard
namespace RigKerDualNumber
open _root_.AlgebraicGeometry.RelPicard.RigKerDualNumber
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.JacobianVarieties.Picard.Proofs.DualKer.AlgebraicGeometry.RelPicard.BaseTransport

Lean source · statement

theorem dualNumberReduction_comp_liftPt_eq_one
    {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']
    (h' : RepresentsRelSubPic (baseChange R c R') (sectionBaseChange R' ε)
      (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε)) (D.baseChange R'))
    (hP : Nonempty (h'.poincare.L ≅ (BaseChange.ofR c ε R'
      (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R R'), pullback.condition⟩)).L))
    (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
    (x : { x : SchemeHomOver (Scheme.TwoAffineOpenCover.specMap R (DualNumber B)) D.toBase //
      dualNumberReduction R B ≫ x.1 =
        ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).one
          (Scheme.TwoAffineOpenCover.specMap R B)).1 })
    : dualNumberReduction R' B ≫
        (liftPt D R' (Scheme.TwoAffineOpenCover.specMap R' (DualNumber B))
          (castBase (tower_dualNumber R' B) x.1)).1 =
      ((RepresentsRelSubPic.relativeGroupLaw
          (P := algEquivZeroGroupCut (baseChange R c R') (sectionBaseChange R' ε)) h').one
        (Scheme.TwoAffineOpenCover.specMap R' B)).1

theorem

existsUnique_kerPoint_baseChange_comp_fst_eq

L294 ↗

AlgebraicGeometry.RelPicard.RigKerDualNumber.existsUnique_kerPoint_baseChange_comp_fst_eq

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.DualKer
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
attribute [local simp] castBase_coe
attribute [local simp] liftPt_fst
open _root_.AlgebraicGeometry.RelPicard.BaseTransport in
open _root_.JacobianVarieties.Picard.Proofs.DualKer.AlgebraicGeometry.RelPicard.BaseTransport in
open _root_.JacobianVarieties.Picard.Proofs.DualKer.AlgebraicGeometry.RelPicard.RigKerDualNumber in
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RigKerDualNumber

Lean source · statement

theorem existsUnique_kerPoint_baseChange_comp_fst_eq
    {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']
    (h' : RepresentsRelSubPic (baseChange R c R') (sectionBaseChange R' ε)
      (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε)) (D.baseChange R'))
    (hP : Nonempty (h'.poincare.L ≅ (BaseChange.ofR c ε R'
      (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R R'), pullback.condition⟩)).L))
    (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
    (x : { x : SchemeHomOver (Scheme.TwoAffineOpenCover.specMap R (DualNumber B)) D.toBase //
      dualNumberReduction R B ≫ x.1 =
        ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).one
          (Scheme.TwoAffineOpenCover.specMap R B)).1 })
    : ∃! x' : { x' : SchemeHomOver (specMap R' (DualNumber B)) (D.baseChange R').toBase //
      dualNumberReduction R' B ≫ x'.1 =
        ((RepresentsRelSubPic.relativeGroupLaw
          (P := algEquivZeroGroupCut (baseChange R c R') (sectionBaseChange R' ε)) h').one
          (Scheme.TwoAffineOpenCover.specMap R' B)).1 },
      x'.1.1 ≫ pullback.fst D.toBase (specMap R R') = x.1.1

Module documentation

Base change of points in the dual-number kernel

Declarations