Module

RelativePic0DesignationBaseChange.lean

Nyll.JacobianVarieties.Pic0.RelativePic0DesignationBaseChange

5 declarations indexed from sourceView source ↗

Module documentation

Base change of a relative Picard-zero designation and the resulting structure morphism and zero section.

Imports2

Imported by30

abbrev

baseChange

L32 ↗

GoodReductionJacobian.RelativePic0Designation.baseChange

Documentation

Base change of the designated Picard-zero scheme together with its zero section.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.SmoothProperCurve
namespace GoodReductionJacobian.RelativePic0Designation
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}

Lean source · full declaration

abbrev baseChange (D : RelativePic0Designation R c) (R' : Type u) [CommRing R'] [Algebra R R'] :
    RelativePic0Designation R' (SmoothProperCurve.baseChange R c R') where
  P := pullback D.toBase (specMap R R')
  toBase := pullback.snd D.toBase (specMap R R')
  zeroSection := pullback.lift (specMap R R' ≫ D.zeroSection) (𝟙 _)
    (by rw [Category.assoc, D.zeroSection_toBase, Category.comp_id, Category.id_comp])
  zeroSection_toBase := pullback.lift_snd _ _ _

theorem

baseChange_P

L42 ↗

GoodReductionJacobian.RelativePic0Designation.baseChange_P

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.SmoothProperCurve
namespace GoodReductionJacobian.RelativePic0Designation
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
variable (D : RelativePic0Designation R c) (R' : Type u) [CommRing R'] [Algebra R R']

Lean source · statement

theorem baseChange_P : (D.baseChange R').P = pullback D.toBase (specMap R R')

theorem

baseChange_toBase

L44 ↗

GoodReductionJacobian.RelativePic0Designation.baseChange_toBase

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.SmoothProperCurve
namespace GoodReductionJacobian.RelativePic0Designation
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
variable (D : RelativePic0Designation R c) (R' : Type u) [CommRing R'] [Algebra R R']

Lean source · statement

theorem baseChange_toBase : (D.baseChange R').toBase = pullback.snd D.toBase (specMap R R')

theorem

baseChange_zeroSection

L46 ↗

GoodReductionJacobian.RelativePic0Designation.baseChange_zeroSection

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.SmoothProperCurve
namespace GoodReductionJacobian.RelativePic0Designation
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
variable (D : RelativePic0Designation R c) (R' : Type u) [CommRing R'] [Algebra R R']

Lean source · full declaration

theorem baseChange_zeroSection :
    (D.baseChange R').zeroSection = pullback.lift (specMap R R' ≫ D.zeroSection) (𝟙 _)
      (by rw [Category.assoc, D.zeroSection_toBase, Category.comp_id, Category.id_comp]) := rfl

theorem

baseChange_zeroSection_fst

L50 ↗

GoodReductionJacobian.RelativePic0Designation.baseChange_zeroSection_fst

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.SmoothProperCurve
namespace GoodReductionJacobian.RelativePic0Designation
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
variable (D : RelativePic0Designation R c) (R' : Type u) [CommRing R'] [Algebra R R']

Lean source · statement

theorem baseChange_zeroSection_fst :
    (D.baseChange R').zeroSection ≫ pullback.fst D.toBase (specMap R R') = specMap R R' ≫
      D.zeroSection

Module documentation

Declarations

baseChange

baseChange_P

baseChange_toBase

baseChange_zeroSection

baseChange_zeroSection_fst