NYLL
Module

AbelianSchemePropertyBundle_of_isPullback.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.AbelianSchemePropertyBundle_of_isPullback
13 declarations indexed from sourceView source ↗

Module documentation

Abelian Scheme Property Bundle of is Pullback

Imports7
Imported by9

Declarations

theorem

inv_comp_eq

L44 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.inv_comp_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_of_isPullback
attribute [-simp] AlgebraicGeometry.schemeFibreEndo_snd AlgebraicGeometry.schemeFibreEndo_fst
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mKcBundleBC
section Transport
variable {R : Type u} [CommRing R] {A B : Scheme.{u}}
  {fA : A ⟶ Spec (CommRingCat.of R)} {fB : B ⟶ Spec (CommRingCat.of R)}
  (e : A ≅ B) (he : e.hom ≫ fB = fA)
include he in
Lean source · statement
theorem inv_comp_eq : e.inv ≫ fA = fB
def

toB

L48 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.toB
Documentation

The point transported through the forward scheme isomorphism over the base.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_of_isPullback
attribute [-simp] AlgebraicGeometry.schemeFibreEndo_snd AlgebraicGeometry.schemeFibreEndo_fst
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mKcBundleBC
section Transport
variable {R : Type u} [CommRing R] {A B : Scheme.{u}}
  {fA : A ⟶ Spec (CommRingCat.of R)} {fB : B ⟶ Spec (CommRingCat.of R)}
  (e : A ≅ B) (he : e.hom ≫ fB = fA)
Lean source · statement
def toB {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (x : SchemeHomOver t fA) : SchemeHomOver
  t fB
def

ofB

L53 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.ofB
Documentation

The point transported through the inverse scheme isomorphism over the base.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_of_isPullback
attribute [-simp] AlgebraicGeometry.schemeFibreEndo_snd AlgebraicGeometry.schemeFibreEndo_fst
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mKcBundleBC
section Transport
variable {R : Type u} [CommRing R] {A B : Scheme.{u}}
  {fA : A ⟶ Spec (CommRingCat.of R)} {fB : B ⟶ Spec (CommRingCat.of R)}
  (e : A ≅ B) (he : e.hom ≫ fB = fA)
Lean source · statement
def ofB {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (y : SchemeHomOver t fB) : SchemeHomOver
  t fA
theorem

toB_coe

L57 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.toB_coe
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_of_isPullback
attribute [-simp] AlgebraicGeometry.schemeFibreEndo_snd AlgebraicGeometry.schemeFibreEndo_fst
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mKcBundleBC
section Transport
variable {R : Type u} [CommRing R] {A B : Scheme.{u}}
  {fA : A ⟶ Spec (CommRingCat.of R)} {fB : B ⟶ Spec (CommRingCat.of R)}
  (e : A ≅ B) (he : e.hom ≫ fB = fA)
Lean source · statement
theorem toB_coe {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (x :
  SchemeHomOver t fA) :
    (toB e he x).1 = x.1 ≫ e.hom
theorem

ofB_coe

L61 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.ofB_coe
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_of_isPullback
attribute [-simp] AlgebraicGeometry.schemeFibreEndo_snd AlgebraicGeometry.schemeFibreEndo_fst
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mKcBundleBC
section Transport
variable {R : Type u} [CommRing R] {A B : Scheme.{u}}
  {fA : A ⟶ Spec (CommRingCat.of R)} {fB : B ⟶ Spec (CommRingCat.of R)}
  (e : A ≅ B) (he : e.hom ≫ fB = fA)
Lean source · statement
theorem ofB_coe {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (y :
  SchemeHomOver t fB) :
    (ofB e he y).1 = y.1 ≫ e.inv
theorem

toB_ofB

L65 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.toB_ofB
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_of_isPullback
attribute [-simp] AlgebraicGeometry.schemeFibreEndo_snd AlgebraicGeometry.schemeFibreEndo_fst
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mKcBundleBC
section Transport
variable {R : Type u} [CommRing R] {A B : Scheme.{u}}
  {fA : A ⟶ Spec (CommRingCat.of R)} {fB : B ⟶ Spec (CommRingCat.of R)}
  (e : A ≅ B) (he : e.hom ≫ fB = fA)
Lean source · statement
theorem toB_ofB {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (y :
  SchemeHomOver t fB) :
    toB e he (ofB e he y) = y
theorem

ofB_toB

L70 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.ofB_toB
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_of_isPullback
attribute [-simp] AlgebraicGeometry.schemeFibreEndo_snd AlgebraicGeometry.schemeFibreEndo_fst
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mKcBundleBC
section Transport
variable {R : Type u} [CommRing R] {A B : Scheme.{u}}
  {fA : A ⟶ Spec (CommRingCat.of R)} {fB : B ⟶ Spec (CommRingCat.of R)}
  (e : A ≅ B) (he : e.hom ≫ fB = fA)
Lean source · statement
theorem ofB_toB {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} (x :
  SchemeHomOver t fA) :
    ofB e he (toB e he x) = x
theorem

toB_schemeHomOverComp

L75 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.toB_schemeHomOverComp
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_of_isPullback
attribute [-simp] AlgebraicGeometry.schemeFibreEndo_snd AlgebraicGeometry.schemeFibreEndo_fst
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mKcBundleBC
section Transport
variable {R : Type u} [CommRing R] {A B : Scheme.{u}}
  {fA : A ⟶ Spec (CommRingCat.of R)} {fB : B ⟶ Spec (CommRingCat.of R)}
  (e : A ≅ B) (he : e.hom ≫ fB = fA)
Lean source · statement
theorem toB_schemeHomOverComp {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : T' ⟶ T) (hψ : ψ ≫ t = t') (x : SchemeHomOver t fA) :
    toB e he (schemeHomOverComp ψ hψ x) = schemeHomOverComp ψ hψ (toB e he x)
theorem

ofB_schemeHomOverComp

L80 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.ofB_schemeHomOverComp
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_of_isPullback
attribute [-simp] AlgebraicGeometry.schemeFibreEndo_snd AlgebraicGeometry.schemeFibreEndo_fst
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mKcBundleBC
section Transport
variable {R : Type u} [CommRing R] {A B : Scheme.{u}}
  {fA : A ⟶ Spec (CommRingCat.of R)} {fB : B ⟶ Spec (CommRingCat.of R)}
  (e : A ≅ B) (he : e.hom ≫ fB = fA)
Lean source · statement
theorem ofB_schemeHomOverComp {T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : T' ⟶ T) (hψ : ψ ≫ t = t') (y : SchemeHomOver t fB) :
    ofB e he (schemeHomOverComp ψ hψ y) = schemeHomOverComp ψ hψ (ofB e he y)
def

transportLaw

L86 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.transportLaw
Documentation

The relative group law transported back through the scheme isomorphism.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_of_isPullback
attribute [-simp] AlgebraicGeometry.schemeFibreEndo_snd AlgebraicGeometry.schemeFibreEndo_fst
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mKcBundleBC
section Transport
variable {R : Type u} [CommRing R] {A B : Scheme.{u}}
  {fA : A ⟶ Spec (CommRingCat.of R)} {fB : B ⟶ Spec (CommRingCat.of R)}
  (e : A ≅ B) (he : e.hom ≫ fB = fA)
Lean source · full declaration
def transportLaw (G : RelativeGroupLaw R fB) : RelativeGroupLaw R fA where
  mul t x y := ofB e he (G.mul t (toB e he x) (toB e he y))
  one t := ofB e he (G.one t)
  inv t x := ofB e he (G.inv t (toB e he x))
  mul_assoc t x y z := by simp only [toB_ofB, G.mul_assoc]
  one_mul t x := by simp only [toB_ofB, G.one_mul, ofB_toB]
  mul_one t x := by simp only [toB_ofB, G.mul_one, ofB_toB]
  inv_mul_cancel t x := by simp only [toB_ofB, G.inv_mul_cancel]
  mul_natural t t' ψ hψ x y := by
    rw [← ofB_schemeHomOverComp, G.mul_natural t t' ψ hψ, toB_schemeHomOverComp,
      toB_schemeHomOverComp]
theorem

connectedSpace_of_field

L106 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.connectedSpace_of_field
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_of_isPullback
attribute [-simp] AlgebraicGeometry.schemeFibreEndo_snd AlgebraicGeometry.schemeFibreEndo_fst
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mKcBundleBC
section Fibres
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  {R' : Type u} [CommRing R'] {ι : Spec (CommRingCat.of R') ⟶ Spec (CommRingCat.of R)}
  {A' : Scheme.{u}} {f' : A' ⟶ Spec (CommRingCat.of R')} {g : A' ⟶ A}
Lean source · statement
theorem connectedSpace_of_field {k : Type u} [Field k] {B : Scheme.{u}} {fk : B ⟶ Spec
  (CommRingCat.of k)}
    (hB : AbelianSchemePropertyBundle k fk) : ConnectedSpace B
theorem

isConnected_fibre

L118 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.isConnected_fibre
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_of_isPullback
attribute [-simp] AlgebraicGeometry.schemeFibreEndo_snd AlgebraicGeometry.schemeFibreEndo_fst
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
namespace P2mKcBundleBC
section Fibres
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  {R' : Type u} [CommRing R'] {ι : Spec (CommRingCat.of R') ⟶ Spec (CommRingCat.of R)}
  {A' : Scheme.{u}} {f' : A' ⟶ Spec (CommRingCat.of R')} {g : A' ⟶ A}
Lean source · statement
theorem isConnected_fibre (hA : AbelianSchemePropertyBundle R f) (hg : IsPullback g f' f ι)
    (s' : ↥(Spec (CommRingCat.of R'))) : _root_.IsConnected (f'.base ⁻¹' {s'})
theorem

of_isPullback

L153 ↗
GoodReductionJacobian.AbelianSchemePropertyBundle.of_isPullback
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_of_isPullback
attribute [-simp] AlgebraicGeometry.schemeFibreEndo_snd AlgebraicGeometry.schemeFibreEndo_fst
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe u
attribute [local simp]
  AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.toB_coe
attribute [local simp]
  AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.ofB_coe
attribute [local simp]
  AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.toB_ofB
attribute [local simp]
  AbelianSchemes.Theorems.Proofs.AbelianSchemePropertyBundle_of_isPullback.P2mKcBundleBC.ofB_toB
open P2mKcBundleBC in
Lean source · full declaration
theorem _root_.GoodReductionJacobian.AbelianSchemePropertyBundle.of_isPullback
    {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
    (hA : AbelianSchemePropertyBundle R f)
    {R' : Type u} [CommRing R'] {ι : Spec (CommRingCat.of R') ⟶ Spec (CommRingCat.of R)}
    {A' : Scheme.{u}} {f' : A' ⟶ Spec (CommRingCat.of R')} {g : A' ⟶ A}
    (hg : IsPullback g f' f ι) :
    AbelianSchemePropertyBundle R' f' where
  smooth := MorphismProperty.of_isPullback hg hA.smooth
  proper := MorphismProperty.of_isPullback hg hA.proper
  connectedFibres := isConnected_fibre hA hg
  hasGroupLaw := by
    obtain ⟨L⟩ := hA.hasGroupLaw
    exact ⟨transportLaw hg.isoPullback (hg.isoPullback_hom_snd) (L.baseChange ι)⟩

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