NYLL
Module

RigKerDualNumberBaseTransport.lean

Nyll.AlgebraicCurves.Geometry.Deformation.RigKerDualNumberBaseTransport
27 declarations indexed from sourceView source ↗

Module documentation

Rig Ker Dual Number Base Transport

Imports4
Imported by7

Declarations

theorem

specMap_comp_specMap

L33 ↗
AlgebraicGeometry.RelPicard.BaseTransport.specMap_comp_specMap
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R]
Lean source · statement
theorem specMap_comp_specMap (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S]
    [Algebra S T] [Algebra R T] [IsScalarTower R S T] :
    specMap S T ≫ specMap R S = specMap R T
def

idOver

L40 ↗
AlgebraicGeometry.RelPicard.BaseTransport.idOver
Documentation

The identity morphism regarded as a morphism over two equal base maps.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R]
Lean source · statement
def idOver {T : Scheme.{u}} {t₁ t₂ : T ⟶ Spec (CommRingCat.of R)} (h : t₁ = t₂) : SchemeHomOver t₂
  t₁
theorem

idOver_coe

L44 ↗
AlgebraicGeometry.RelPicard.BaseTransport.idOver_coe
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R]
Lean source · statement
theorem idOver_coe {T : Scheme.{u}} {t₁ t₂ : T ⟶ Spec (CommRingCat.of R)} (h : t₁ = t₂) :
    (idOver h).1 = 𝟙 T
theorem

baseChangeSnd_eq_id

L50 ↗
AlgebraicGeometry.RelPicard.BaseTransport.baseChangeSnd_eq_id
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
Lean source · statement
theorem baseChangeSnd_eq_id {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (φ : SchemeHomOver t
  t)
    (hφ : φ.1 = 𝟙 T) : baseChangeSnd c φ = 𝟙 (pullback c t)
def

pullbackAlong_pullbackAlong_iso

L62 ↗
AlgebraicGeometry.RelPicard.BaseTransport.RigidifiedLineBundle.pullbackAlong_pullbackAlong_iso
Documentation

The comparison between an iterated rigidified pullback and pullback along the composite.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigidifiedLineBundle
variable {c ε}
Lean source · statement
def pullbackAlong_pullbackAlong_iso {T T' T'' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} {t'' : T'' ⟶ Spec (CommRingCat.of R)}
    (M : RigidifiedLineBundle c ε t) (φ : SchemeHomOver t' t) (ψ : SchemeHomOver t'' t') :
    ((M.pullbackAlong φ).pullbackAlong ψ).L ≅ (M.pullbackAlong (postComp φ ψ)).L
def

pullbackAlong_iso_of_coe_eq_id

L70 ↗
AlgebraicGeometry.RelPicard.BaseTransport.RigidifiedLineBundle.pullbackAlong_iso_of_coe_eq_id
Documentation

The underlying-module isomorphism for pullback along an identity scheme morphism.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigidifiedLineBundle
variable {c ε}
Lean source · statement
def pullbackAlong_iso_of_coe_eq_id {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (M : RigidifiedLineBundle c ε t) (φ : SchemeHomOver t t) (hφ : φ.1 = 𝟙 T) :
    (M.pullbackAlong φ).L ≅ M.L
def

pullbackAlong_idOver_idOver_iso

L80 ↗
AlgebraicGeometry.RelPicard.BaseTransport.RigidifiedLineBundle.pullbackAlong_idOver_idOver_iso
Documentation

The underlying-module isomorphism for successive transport along an equality of base maps and its inverse.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigidifiedLineBundle
variable {c ε}
Lean source · statement
def pullbackAlong_idOver_idOver_iso {T : Scheme.{u}} {t₁ t₂ : T ⟶ Spec (CommRingCat.of R)} (h : t₁
  = t₂)
    (M : RigidifiedLineBundle c ε t₁) :
    (((M.pullbackAlong (idOver h)).pullbackAlong (idOver h.symm))).L ≅ M.L
def

unit_pullbackAlong_iso

L90 ↗
AlgebraicGeometry.RelPicard.BaseTransport.RigidifiedLineBundle.unit_pullbackAlong_iso
Documentation

The canonical identification of the pullback of the unit rigidified line bundle with the unit.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigidifiedLineBundle
variable {c ε}
Lean source · statement
def unit_pullbackAlong_iso {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver t' t) :
    ((RigidifiedLineBundle.unit (c := c) (ε := ε) t).pullbackAlong ψ).L ≅
      (RigidifiedLineBundle.unit (c := c) (ε := ε) t').L
def

pullbackAlong_mapIso

L97 ↗
AlgebraicGeometry.RelPicard.BaseTransport.RigidifiedLineBundle.pullbackAlong_mapIso
Documentation

The isomorphism on underlying modules induced by rigidified pullback.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace RigidifiedLineBundle
variable {c ε}
Lean source · statement
def pullbackAlong_mapIso {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} {M M' : RigidifiedLineBundle c ε t}
    (ψ : SchemeHomOver t' t) (e : M.L ≅ M'.L) : (M.pullbackAlong ψ).L ≅ (M'.pullbackAlong ψ).L
def

ofR_pullbackAlong_iso

L112 ↗
AlgebraicGeometry.RelPicard.BaseTransport.BaseChange.ofR_pullbackAlong_iso
Documentation

The comparison identifying base-change transport followed by pullback with pullback followed by transport.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace BaseChange
variable (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def ofR_pullbackAlong_iso {T T'' : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of R')}
    {t'' : T'' ⟶ Spec (CommRingCat.of R')} (ψ : SchemeHomOver t'' t')
    (M : RigidifiedLineBundle c ε (t' ≫ specMap R R')) :
    ((BaseChange.ofR c ε R' M).pullbackAlong ψ).L ≅
      (BaseChange.ofR c ε R' (M.pullbackAlong (BaseChange.overR R' ψ))).L
def

ofR_unit_iso

L125 ↗
AlgebraicGeometry.RelPicard.BaseTransport.BaseChange.ofR_unit_iso
Documentation

The identification of the base-changed unit rigidified line bundle with the unit.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace BaseChange
variable (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def ofR_unit_iso {T : Scheme.{u}} (t' : T ⟶ Spec (CommRingCat.of R')) :
    (BaseChange.ofR c ε R' (RigidifiedLineBundle.unit (t' ≫ specMap R R'))).L ≅
      (RigidifiedLineBundle.unit (c := baseChange R c R') (ε := sectionBaseChange R' ε) t').L
def

ofR_mapIso

L131 ↗
AlgebraicGeometry.RelPicard.BaseTransport.BaseChange.ofR_mapIso
Documentation

The isomorphism on underlying modules induced by transport to the base-changed curve.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace BaseChange
variable (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def ofR_mapIso {T : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of R')}
    {M M' : RigidifiedLineBundle c ε (t' ≫ specMap R R')} (e : M.L ≅ M'.L) :
    (BaseChange.ofR c ε R' M).L ≅ (BaseChange.ofR c ε R' M').L
def

toR_mapIso

L137 ↗
AlgebraicGeometry.RelPicard.BaseTransport.BaseChange.toR_mapIso
Documentation

The isomorphism on underlying modules induced by transport back from the base-changed curve.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
namespace BaseChange
variable (R' : Type u) [CommRing R'] [Algebra R R']
Lean source · statement
def toR_mapIso {T : Scheme.{u}} {t' : T ⟶ Spec (CommRingCat.of R')}
    {M M' : RigidifiedLineBundle (baseChange R c R') (sectionBaseChange R' ε) t'} (e : M.L ≅ M'.L) :
    (BaseChange.toR c ε R' M).L ≅ (BaseChange.toR c ε R' M').L
theorem

fstHom_toRingHom_eq

L152 ↗
AlgebraicGeometry.RelPicard.BaseTransport.fstHom_toRingHom_eq
Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section DualNumberTower
variable (R' : Type u) [CommRing R'] [Algebra R R'] (B : Type u) [CommRing B] [Algebra R' B]
  [Algebra R B]
  [IsScalarTower R R' B]
omit [Algebra R R'] [IsScalarTower R R' B] in
Lean source · statement
theorem fstHom_toRingHom_eq :
    (TrivSqZeroExt.fstHom R B B).toRingHom = (TrivSqZeroExt.fstHom R' B B).toRingHom
theorem

specMap_dualNumber_comp

L155 ↗
AlgebraicGeometry.RelPicard.BaseTransport.specMap_dualNumber_comp
Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R]
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
section DualNumberTower
variable (R' : Type u) [CommRing R'] [Algebra R R'] (B : Type u) [CommRing B] [Algebra R' B]
  [Algebra R B]
  [IsScalarTower R R' B]
Lean source · statement
theorem specMap_dualNumber_comp : specMap R' (DualNumber B) ≫ specMap R R' = specMap R (DualNumber
  B)
theorem

tower_dualNumber

L172 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.tower_dualNumber
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.RigKerDualNumber
open AlgebraicGeometry.RelPicard.BaseTransport MonoidalCategory
variable {R : Type u} [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R']
  {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of
    R))) c)
  (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
Lean source · statement
theorem tower_dualNumber :
    Scheme.TwoAffineOpenCover.specMap R (DualNumber B) = specMap R' (DualNumber B) ≫ specMap R R'
theorem

tower_base

L176 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.tower_base
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.RigKerDualNumber
open AlgebraicGeometry.RelPicard.BaseTransport MonoidalCategory
variable {R : Type u} [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R']
  {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of
    R))) c)
  (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
Lean source · statement
theorem tower_base : Scheme.TwoAffineOpenCover.specMap R B = specMap R' B ≫ specMap R R'
def

pullbackAlong_congr_hom

L183 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.pullbackAlong_congr_hom
Documentation

The comparison between rigidified pullbacks along morphisms with equal underlying scheme maps.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.RigKerDualNumber
open AlgebraicGeometry.RelPicard.BaseTransport MonoidalCategory
variable {R : Type u} [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R']
  {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of
    R))) c)
  (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
variable {c ε} in
Lean source · statement
def _root_.AlgebraicGeometry.RelPicard.RigidifiedLineBundle.pullbackAlong_congr_hom
    {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
    (M : RigidifiedLineBundle c ε t) (φ ψ : SchemeHomOver t' t) (h : φ.1 = ψ.1) :
    (M.pullbackAlong φ).L ≅ (M.pullbackAlong ψ).L
def

baseTransportCarrierIso

L192 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.baseTransportCarrierIso
Documentation

The trivialization after dual-number reduction that accompanies transport to the changed base.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.RigKerDualNumber
open AlgebraicGeometry.RelPicard.BaseTransport MonoidalCategory
variable {R : Type u} [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R']
  {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of
    R))) c)
  (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
variable {c ε} in
Lean source · statement
def baseTransportCarrierIso (M : RigKerDualNumber.Carrier c ε B) :
    ((BaseChange.ofR c ε R' (M.1.pullbackAlong (idOver (tower_dualNumber R' B)))).pullbackAlong
        (dualNumberReductionOver R' B)).L ≅
      (RigidifiedLineBundle.unit (c := baseChange R c R') (ε := sectionBaseChange R' ε)
        (Scheme.TwoAffineOpenCover.specMap R' B)).L
def

baseTransportCarrier

L209 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.baseTransportCarrier
Documentation

The representative in the dual-number kernel obtained by transport to the changed base.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.RigKerDualNumber
open AlgebraicGeometry.RelPicard.BaseTransport MonoidalCategory
variable {R : Type u} [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R']
  {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of
    R))) c)
  (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
variable {c ε} in
Lean source · statement
def baseTransportCarrier (M : RigKerDualNumber.Carrier c ε B) :
    RigKerDualNumber.Carrier (baseChange R c R') (sectionBaseChange R' ε) B
def

baseTransportCarrierInvIso

L215 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.baseTransportCarrierInvIso
Documentation

The trivialization after dual-number reduction that accompanies inverse base transport.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.RigKerDualNumber
open AlgebraicGeometry.RelPicard.BaseTransport MonoidalCategory
variable {R : Type u} [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R']
  {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of
    R))) c)
  (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
variable {c ε} in
Lean source · statement
def baseTransportCarrierInvIso
    (M' : RigKerDualNumber.Carrier (baseChange R c R') (sectionBaseChange R' ε) B) :
    (((BaseChange.toR c ε R' M'.1).pullbackAlong (idOver (tower_dualNumber R'
      B).symm)).pullbackAlong
        (dualNumberReductionOver R B)).L ≅
      (RigidifiedLineBundle.unit (c := c) (ε := ε) (Scheme.TwoAffineOpenCover.specMap R B)).L
def

baseTransportCarrierInv

L234 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.baseTransportCarrierInv
Documentation

The representative in the original dual-number kernel obtained by inverse base transport.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.RigKerDualNumber
open AlgebraicGeometry.RelPicard.BaseTransport MonoidalCategory
variable {R : Type u} [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R']
  {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of
    R))) c)
  (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
variable {c ε} in
Lean source · statement
def baseTransportCarrierInv
    (M' : RigKerDualNumber.Carrier (baseChange R c R') (sectionBaseChange R' ε) B) :
    RigKerDualNumber.Carrier c ε B
def

baseTransport

L243 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.baseTransport
Documentation

The equivalence of dual-number kernels induced by transport through the base-change isomorphism.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.RigKerDualNumber
open AlgebraicGeometry.RelPicard.BaseTransport MonoidalCategory
variable {R : Type u} [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R']
  {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of
    R))) c)
  (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
variable {c ε} in
Lean source · full declaration
def baseTransport :
    RigKerDualNumber c ε B ≃ RigKerDualNumber (baseChange R c R') (sectionBaseChange R' ε) B where
  toFun := Quotient.map (baseTransportCarrier R' c ε B)
    (fun M N (h : Nonempty (M.1.L ≅ N.1.L)) =>
      (⟨BaseChange.ofR_mapIso c ε R' (RigidifiedLineBundle.pullbackAlong_mapIso _ h.some)⟩ :
        Nonempty ((baseTransportCarrier R' c ε B M).1.L ≅ (baseTransportCarrier R' c ε B N).1.L)))
  invFun := Quotient.map (baseTransportCarrierInv R' c ε B)
    (fun M N (h : Nonempty (M.1.L ≅ N.1.L)) =>
      (⟨RigidifiedLineBundle.pullbackAlong_mapIso _ (BaseChange.toR_mapIso c ε R' h.some)⟩ :
        Nonempty ((baseTransportCarrierInv R' c ε B M).1.L ≅ (baseTransportCarrierInv R' c ε B
          N).1.L)))
  left_inv := fun x => by
    induction x using Quotient.ind with
    | _ M =>
      exact Quotient.sound
        (⟨RigidifiedLineBundle.pullbackAlong_mapIso _ (BaseChange.toR_ofR_iso c ε R' _) ≪≫
          RigidifiedLineBundle.pullbackAlong_idOver_idOver_iso (tower_dualNumber R' B) M.1⟩ :
          Nonempty (_ ≅ M.1.L))
  right_inv := fun x => by
    induction x using Quotient.ind with
    | _ M' =>
      exact Quotient.sound
        (⟨BaseChange.ofR_mapIso c ε R'
            (RigidifiedLineBundle.pullbackAlong_idOver_idOver_iso (tower_dualNumber R' B).symm _) ≪≫
          BaseChange.ofR_toR_iso c ε R' M'.1⟩ : Nonempty (_ ≅ M'.1.L))
theorem

baseTransport_mk

L269 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.baseTransport_mk
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.RigKerDualNumber
open AlgebraicGeometry.RelPicard.BaseTransport MonoidalCategory
variable {R : Type u} [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R']
  {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of
    R))) c)
  (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
variable {c ε} in
Lean source · statement
theorem baseTransport_mk (M : RigKerDualNumber.Carrier c ε B) :
    baseTransport R' c ε B (Quotient.mk _ M) = Quotient.mk _ (baseTransportCarrier R' c ε B M)
theorem

baseTransport_symm_mk

L273 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.baseTransport_symm_mk
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.RigKerDualNumber
open AlgebraicGeometry.RelPicard.BaseTransport MonoidalCategory
variable {R : Type u} [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R']
  {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of
    R))) c)
  (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
variable {c ε} in
Lean source · statement
theorem baseTransport_symm_mk
    (M' : RigKerDualNumber.Carrier (baseChange R c R') (sectionBaseChange R' ε) B) :
    (baseTransport R' c ε B).symm (Quotient.mk _ M') = Quotient.mk _ (baseTransportCarrierInv R' c
      ε B M')
theorem

baseTransport_mul

L279 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.baseTransport_mul
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.RigKerDualNumber
open AlgebraicGeometry.RelPicard.BaseTransport MonoidalCategory
variable {R : Type u} [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R']
  {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of
    R))) c)
  (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
variable {c ε} in
Lean source · statement
theorem baseTransport_mul (x y : RigKerDualNumber c ε B) :
    baseTransport R' c ε B (RigKerDualNumber.mul c ε B x y) =
      RigKerDualNumber.mul (baseChange R c R') (sectionBaseChange R' ε) B
        (baseTransport R' c ε B x) (baseTransport R' c ε B y)
theorem

baseTransport_one

L292 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.baseTransport_one
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  AlgebraicGeometry.SmoothProperCurve NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.RigKerDualNumber
open AlgebraicGeometry.RelPicard.BaseTransport MonoidalCategory
variable {R : Type u} [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R']
  {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of
    R))) c)
  (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
variable {c ε} in
Lean source · statement
theorem baseTransport_one :
    baseTransport R' c ε B (RigKerDualNumber.one c ε B) =
      RigKerDualNumber.one (baseChange R c R') (sectionBaseChange R' ε) B

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