NYLL
Module

Product.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.Product
51 declarations indexed from sourceView source ↗

Module documentation

Product

Imports3
Imported by12

Declarations

abbrev

prodStr

L36 ↗
GoodReductionJacobian.prodStr
Documentation

The structure morphism of the fibre product over the base ring.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
Lean source · statement
abbrev prodStr : pullback g h ⟶ Spec (CommRingCat.of R)
theorem

pullback_snd_comp_eq_prodStr

L38 ↗
GoodReductionJacobian.pullback_snd_comp_eq_prodStr
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem pullback_snd_comp_eq_prodStr : pullback.snd g h ≫ h = prodStr g h
def

prodFstPt

L48 ↗
GoodReductionJacobian.prodFstPt
Documentation

The first component of a point of the fibre product.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def prodFstPt (z : SchemeHomOver t (prodStr g h)) : SchemeHomOver t g
def

prodSndPt

L52 ↗
GoodReductionJacobian.prodSndPt
Documentation

The second component of a point of the fibre product.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def prodSndPt (z : SchemeHomOver t (prodStr g h)) : SchemeHomOver t h
def

prodPairPt

L56 ↗
GoodReductionJacobian.prodPairPt
Documentation

The point of the fibre product determined by a pair of points over the same base.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def prodPairPt (x : SchemeHomOver t g) (y : SchemeHomOver t h) : SchemeHomOver t (prodStr g h)
theorem

prodFstPt_coe

L60 ↗
GoodReductionJacobian.prodFstPt_coe
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem prodFstPt_coe (z : SchemeHomOver t (prodStr g h)) :
    (prodFstPt z).1 = z.1 ≫ pullback.fst g h
theorem

prodSndPt_coe

L64 ↗
GoodReductionJacobian.prodSndPt_coe
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem prodSndPt_coe (z : SchemeHomOver t (prodStr g h)) :
    (prodSndPt z).1 = z.1 ≫ pullback.snd g h
theorem

prodPairPt_coe

L68 ↗
GoodReductionJacobian.prodPairPt_coe
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem prodPairPt_coe (x : SchemeHomOver t g) (y : SchemeHomOver t h) :
    (prodPairPt x y).1 = pullback.lift x.1 y.1 (x.2.trans y.2.symm)
theorem

prodFstPt_prodPairPt

L72 ↗
GoodReductionJacobian.prodFstPt_prodPairPt
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem prodFstPt_prodPairPt (x : SchemeHomOver t g) (y : SchemeHomOver t h) :
    prodFstPt (prodPairPt x y) = x
theorem

prodSndPt_prodPairPt

L76 ↗
GoodReductionJacobian.prodSndPt_prodPairPt
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem prodSndPt_prodPairPt (x : SchemeHomOver t g) (y : SchemeHomOver t h) :
    prodSndPt (prodPairPt x y) = y
theorem

prodPt_ext

L80 ↗
GoodReductionJacobian.prodPt_ext
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem prodPt_ext {z w : SchemeHomOver t (prodStr g h)} (h1 : prodFstPt z = prodFstPt w)
    (h2 : prodSndPt z = prodSndPt w) : z = w
theorem

prodPairPt_prodFstPt_prodSndPt

L87 ↗
GoodReductionJacobian.prodPairPt_prodFstPt_prodSndPt
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem prodPairPt_prodFstPt_prodSndPt (z : SchemeHomOver t (prodStr g h)) :
    prodPairPt (prodFstPt z) (prodSndPt z) = z
def

prodPointEquiv

L92 ↗
GoodReductionJacobian.prodPointEquiv
Documentation

The equivalence between points of the fibre product and pairs of points over the base.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · full declaration
def prodPointEquiv (t : T ⟶ Spec (CommRingCat.of R)) :
    SchemeHomOver t (prodStr g h) ≃ SchemeHomOver t g × SchemeHomOver t h where
  toFun z := (prodFstPt z, prodSndPt z)
  invFun p := prodPairPt p.1 p.2
  left_inv z := prodPairPt_prodFstPt_prodSndPt z
  right_inv := fun ⟨x, y⟩ => Prod.ext (prodFstPt_prodPairPt x y) (prodSndPt_prodPairPt x y)
theorem

prodFstPt_natural

L99 ↗
GoodReductionJacobian.prodFstPt_natural
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem prodFstPt_natural {T' : Scheme.{u}} {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : T' ⟶ T)
    (hψ : ψ ≫ t = t') (z : SchemeHomOver t (prodStr g h)) :
    prodFstPt (schemeHomOverComp ψ hψ z) = schemeHomOverComp ψ hψ (prodFstPt z)
theorem

prodSndPt_natural

L104 ↗
GoodReductionJacobian.prodSndPt_natural
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem prodSndPt_natural {T' : Scheme.{u}} {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : T' ⟶ T)
    (hψ : ψ ≫ t = t') (z : SchemeHomOver t (prodStr g h)) :
    prodSndPt (schemeHomOverComp ψ hψ z) = schemeHomOverComp ψ hψ (prodSndPt z)
theorem

prodPairPt_natural

L109 ↗
GoodReductionJacobian.prodPairPt_natural
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem prodPairPt_natural {T' : Scheme.{u}} {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : T' ⟶ T)
    (hψ : ψ ≫ t = t') (x : SchemeHomOver t g) (y : SchemeHomOver t h) :
    schemeHomOverComp ψ hψ (prodPairPt x y) =
      prodPairPt (schemeHomOverComp ψ hψ x) (schemeHomOverComp ψ hψ y)
theorem

prodFstPt_schemeHomOverComp

L117 ↗
GoodReductionJacobian.prodFstPt_schemeHomOverComp
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem prodFstPt_schemeHomOverComp {S : Scheme.{u}} {s : S ⟶ Spec (CommRingCat.of R)}
    (x : SchemeHomOver s t) (z : SchemeHomOver t (prodStr g h)) :
    prodFstPt (NeronModelInfra.schemeHomOverComp x z) = NeronModelInfra.schemeHomOverComp x
      (prodFstPt z)
theorem

prodSndPt_schemeHomOverComp

L123 ↗
GoodReductionJacobian.prodSndPt_schemeHomOverComp
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem prodSndPt_schemeHomOverComp {S : Scheme.{u}} {s : S ⟶ Spec (CommRingCat.of R)}
    (x : SchemeHomOver s t) (z : SchemeHomOver t (prodStr g h)) :
    prodSndPt (NeronModelInfra.schemeHomOverComp x z) = NeronModelInfra.schemeHomOverComp x
      (prodSndPt z)
theorem

schemeHomOverComp_prodPairPt

L129 ↗
GoodReductionJacobian.schemeHomOverComp_prodPairPt
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Points
variable {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem schemeHomOverComp_prodPairPt {S : Scheme.{u}} {s : S ⟶ Spec (CommRingCat.of R)}
    (x : SchemeHomOver s t) (y : SchemeHomOver t g) (z : SchemeHomOver t h) :
    NeronModelInfra.schemeHomOverComp x (prodPairPt y z) =
      prodPairPt (NeronModelInfra.schemeHomOverComp x y) (NeronModelInfra.schemeHomOverComp x z)
def

prod

L143 ↗
GoodReductionJacobian.RelativeGroupLaw.prod
Documentation

The componentwise relative group law on the fibre product.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
namespace RelativeGroupLaw
Lean source · full declaration
def prod (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h) : RelativeGroupLaw R (prodStr g h)
  where
  mul t z w := prodPairPt (GB.mul t (prodFstPt z) (prodFstPt w)) (GC.mul t (prodSndPt z) (prodSndPt
    w))
  one t := prodPairPt (GB.one t) (GC.one t)
  inv t z := prodPairPt (GB.inv t (prodFstPt z)) (GC.inv t (prodSndPt z))
  mul_assoc t x y z := by
    apply prodPt_ext
    · simp only [prodFstPt_prodPairPt, GB.mul_assoc]
    · simp only [prodSndPt_prodPairPt, GC.mul_assoc]
  one_mul t x := by
    apply prodPt_ext
    · simp only [prodFstPt_prodPairPt, GB.one_mul]
    · simp only [prodSndPt_prodPairPt, GC.one_mul]
  mul_one t x := by
    apply prodPt_ext
    · simp only [prodFstPt_prodPairPt, GB.mul_one]
    · simp only [prodSndPt_prodPairPt, GC.mul_one]
  inv_mul_cancel t x := by
    apply prodPt_ext
    · simp only [prodFstPt_prodPairPt, GB.inv_mul_cancel]
    · simp only [prodSndPt_prodPairPt, GC.inv_mul_cancel]
  mul_natural t t' ψ hψ x y := by
    rw [prodPairPt_natural, GB.mul_natural, GC.mul_natural, prodFstPt_natural, prodFstPt_natural,
      prodSndPt_natural, prodSndPt_natural]
theorem

prod_mul

L175 ↗
GoodReductionJacobian.RelativeGroupLaw.prod_mul
Source context 11 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
namespace RelativeGroupLaw
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
section Unfolding
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem prod_mul (z w : SchemeHomOver t (prodStr g h)) :
    (GB.prod GC).mul t z w =
      prodPairPt (GB.mul t (prodFstPt z) (prodFstPt w)) (GC.mul t (prodSndPt z) (prodSndPt w))
theorem

prod_one

L180 ↗
GoodReductionJacobian.RelativeGroupLaw.prod_one
Source context 11 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
namespace RelativeGroupLaw
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
section Unfolding
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem prod_one : (GB.prod GC).one t = prodPairPt (GB.one t) (GC.one t)
theorem

prod_inv

L183 ↗
GoodReductionJacobian.RelativeGroupLaw.prod_inv
Source context 11 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
namespace RelativeGroupLaw
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
section Unfolding
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem prod_inv (z : SchemeHomOver t (prodStr g h)) :
    (GB.prod GC).inv t z = prodPairPt (GB.inv t (prodFstPt z)) (GC.inv t (prodSndPt z))
theorem

prodFstPt_mul

L187 ↗
GoodReductionJacobian.RelativeGroupLaw.prodFstPt_mul
Source context 11 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
namespace RelativeGroupLaw
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
section Unfolding
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem prodFstPt_mul (z w : SchemeHomOver t (prodStr g h)) :
    prodFstPt ((GB.prod GC).mul t z w) = GB.mul t (prodFstPt z) (prodFstPt w)
theorem

prodSndPt_mul

L191 ↗
GoodReductionJacobian.RelativeGroupLaw.prodSndPt_mul
Source context 11 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
namespace RelativeGroupLaw
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
section Unfolding
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem prodSndPt_mul (z w : SchemeHomOver t (prodStr g h)) :
    prodSndPt ((GB.prod GC).mul t z w) = GC.mul t (prodSndPt z) (prodSndPt w)
theorem

prodPairPt_mul_prodPairPt

L195 ↗
GoodReductionJacobian.RelativeGroupLaw.prodPairPt_mul_prodPairPt
Source context 11 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
namespace RelativeGroupLaw
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
section Unfolding
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem prodPairPt_mul_prodPairPt (x x' : SchemeHomOver t g) (y y' : SchemeHomOver t h) :
    (GB.prod GC).mul t (prodPairPt x y) (prodPairPt x' y') = prodPairPt (GB.mul t x x') (GC.mul t y
      y')
theorem

prod

L202 ↗
GoodReductionJacobian.RelativeGroupLaw.IsCommutative.prod
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
namespace RelativeGroupLaw
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
Lean source · statement
theorem IsCommutative.prod {GB : RelativeGroupLaw R g} {GC : RelativeGroupLaw R h} (hB :
  GB.IsCommutative)
    (hC : GC.IsCommutative) : (GB.prod GC).IsCommutative
def

prodFst

L211 ↗
GoodReductionJacobian.prodFst
Documentation

The first projection of the product as a morphism over the base.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
Lean source · statement
def prodFst : SchemeHomOver (prodStr g h) g
def

prodSnd

L215 ↗
GoodReductionJacobian.prodSnd
Documentation

The second projection of the product as a morphism over the base.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
Lean source · statement
def prodSnd : SchemeHomOver (prodStr g h) h
def

prodInl

L219 ↗
GoodReductionJacobian.prodInl
Documentation

The inclusion of the first factor with the identity point in the second factor.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
Lean source · statement
def prodInl (GC : RelativeGroupLaw R h) : SchemeHomOver g (prodStr g h)
def

prodInr

L223 ↗
GoodReductionJacobian.prodInr
Documentation

The inclusion of the second factor with the identity point in the first factor.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
Lean source · statement
def prodInr (GB : RelativeGroupLaw R g) : SchemeHomOver h (prodStr g h)
theorem

prodFst_coe

L226 ↗
GoodReductionJacobian.prodFst_coe
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
Lean source · statement
theorem prodFst_coe : (prodFst (g := g) (h := h)).1 = pullback.fst g h
theorem

prodSnd_coe

L228 ↗
GoodReductionJacobian.prodSnd_coe
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
Lean source · statement
theorem prodSnd_coe : (prodSnd (g := g) (h := h)).1 = pullback.snd g h
theorem

schemeHomOverComp_prodFst

L235 ↗
GoodReductionJacobian.schemeHomOverComp_prodFst
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section MapsOnPoints
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem schemeHomOverComp_prodFst (z : SchemeHomOver t (prodStr g h)) :
    NeronModelInfra.schemeHomOverComp z (prodFst (g := g) (h := h)) = prodFstPt z
theorem

schemeHomOverComp_prodSnd

L239 ↗
GoodReductionJacobian.schemeHomOverComp_prodSnd
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section MapsOnPoints
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem schemeHomOverComp_prodSnd (z : SchemeHomOver t (prodStr g h)) :
    NeronModelInfra.schemeHomOverComp z (prodSnd (g := g) (h := h)) = prodSndPt z
theorem

schemeHomOverComp_prodInl

L243 ↗
GoodReductionJacobian.schemeHomOverComp_prodInl
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section MapsOnPoints
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem schemeHomOverComp_prodInl (x : SchemeHomOver t g) :
    NeronModelInfra.schemeHomOverComp x (prodInl GC) = prodPairPt x (GC.one t)
theorem

schemeHomOverComp_prodInr

L250 ↗
GoodReductionJacobian.schemeHomOverComp_prodInr
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section MapsOnPoints
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem schemeHomOverComp_prodInr (y : SchemeHomOver t h) :
    NeronModelInfra.schemeHomOverComp y (prodInr GB) = prodPairPt (GB.one t) y
theorem

prodFst_hom

L257 ↗
GoodReductionJacobian.prodFst_hom
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section MapsOnPoints
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem prodFst_hom (x y : SchemeHomOver t (prodStr g h)) :
    NeronModelInfra.schemeHomOverComp ((GB.prod GC).mul t x y) (prodFst (g := g) (h := h)) =
      GB.mul t (NeronModelInfra.schemeHomOverComp x prodFst) (NeronModelInfra.schemeHomOverComp y
        prodFst)
theorem

prodSnd_hom

L264 ↗
GoodReductionJacobian.prodSnd_hom
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section MapsOnPoints
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem prodSnd_hom (x y : SchemeHomOver t (prodStr g h)) :
    NeronModelInfra.schemeHomOverComp ((GB.prod GC).mul t x y) (prodSnd (g := g) (h := h)) =
      GC.mul t (NeronModelInfra.schemeHomOverComp x prodSnd) (NeronModelInfra.schemeHomOverComp y
        prodSnd)
theorem

prodInl_hom

L271 ↗
GoodReductionJacobian.prodInl_hom
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section MapsOnPoints
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem prodInl_hom (x y : SchemeHomOver t g) :
    NeronModelInfra.schemeHomOverComp (GB.mul t x y) (prodInl GC) =
      (GB.prod GC).mul t (NeronModelInfra.schemeHomOverComp x (prodInl GC))
        (NeronModelInfra.schemeHomOverComp y (prodInl GC))
theorem

prodInr_hom

L278 ↗
GoodReductionJacobian.prodInr_hom
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section MapsOnPoints
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem prodInr_hom (x y : SchemeHomOver t h) :
    NeronModelInfra.schemeHomOverComp (GC.mul t x y) (prodInr GB) =
      (GB.prod GC).mul t (NeronModelInfra.schemeHomOverComp x (prodInr GB))
        (NeronModelInfra.schemeHomOverComp y (prodInr GB))
theorem

prodPairPt_hom

L285 ↗
GoodReductionJacobian.prodPairPt_hom
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section MapsOnPoints
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem prodPairPt_hom {X : Scheme.{u}} {e : X ⟶ Spec (CommRingCat.of R)} (GX : RelativeGroupLaw R
  e)
    (u : SchemeHomOver e g) (v : SchemeHomOver e h)
    (hu : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t e),
      NeronModelInfra.schemeHomOverComp (GX.mul t x y) u =
        GB.mul t (NeronModelInfra.schemeHomOverComp x u) (NeronModelInfra.schemeHomOverComp y u))
    (hv : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t e),
      NeronModelInfra.schemeHomOverComp (GX.mul t x y) v =
        GC.mul t (NeronModelInfra.schemeHomOverComp x v) (NeronModelInfra.schemeHomOverComp y v))
    (x y : SchemeHomOver t e) :
    NeronModelInfra.schemeHomOverComp (GX.mul t x y) (prodPairPt u v) =
      (GB.prod GC).mul t (NeronModelInfra.schemeHomOverComp x (prodPairPt u v))
        (NeronModelInfra.schemeHomOverComp y (prodPairPt u v))
theorem

prodPt_eq_mul_prodInl_prodInr

L301 ↗
GoodReductionJacobian.prodPt_eq_mul_prodInl_prodInr
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section MapsOnPoints
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
variable {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
Lean source · statement
theorem prodPt_eq_mul_prodInl_prodInr (z : SchemeHomOver t (prodStr g h)) :
    z = (GB.prod GC).mul t (NeronModelInfra.schemeHomOverComp (prodFstPt z) (prodInl GC))
      (NeronModelInfra.schemeHomOverComp (prodSndPt z) (prodInr GB))
theorem

prodInl_comp_prodFst

L314 ↗
GoodReductionJacobian.prodInl_comp_prodFst
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Identities
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
Lean source · statement
theorem prodInl_comp_prodFst :
    NeronModelInfra.schemeHomOverComp (prodInl GC) prodFst = schemeHomOverId g
theorem

prodInl_comp_prodSnd

L318 ↗
GoodReductionJacobian.prodInl_comp_prodSnd
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Identities
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
Lean source · statement
theorem prodInl_comp_prodSnd :
    NeronModelInfra.schemeHomOverComp (prodInl GC) prodSnd = GC.one g
theorem

prodInr_comp_prodFst

L322 ↗
GoodReductionJacobian.prodInr_comp_prodFst
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Identities
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
Lean source · statement
theorem prodInr_comp_prodFst :
    NeronModelInfra.schemeHomOverComp (prodInr GB) prodFst = GB.one h
theorem

prodInr_comp_prodSnd

L326 ↗
GoodReductionJacobian.prodInr_comp_prodSnd
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Identities
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
Lean source · statement
theorem prodInr_comp_prodSnd :
    NeronModelInfra.schemeHomOverComp (prodInr (g := g) GB) prodSnd = schemeHomOverId h
theorem

prod_mul_prodFst_prodInl_prodSnd_prodInr

L330 ↗
GoodReductionJacobian.prod_mul_prodFst_prodInl_prodSnd_prodInr
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Identities
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
Lean source · statement
theorem prod_mul_prodFst_prodInl_prodSnd_prodInr :
    (GB.prod GC).mul (prodStr g h) (NeronModelInfra.schemeHomOverComp prodFst (prodInl GC))
      (NeronModelInfra.schemeHomOverComp prodSnd (prodInr GB)) = schemeHomOverId (prodStr g h)
theorem

eq_one_of_prodInl_comp_of_prodInr_comp

L340 ↗
GoodReductionJacobian.eq_one_of_prodInl_comp_of_prodInr_comp
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Identities
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
Lean source · statement
theorem eq_one_of_prodInl_comp_of_prodInr_comp (β : SchemeHomOver (prodStr g h) (prodStr g h))
    (hβ : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t (prodStr g
      h)),
      NeronModelInfra.schemeHomOverComp ((GB.prod GC).mul t x y) β =
        (GB.prod GC).mul t (NeronModelInfra.schemeHomOverComp x β)
          (NeronModelInfra.schemeHomOverComp y β))
    (h1 : NeronModelInfra.schemeHomOverComp (prodInl GC) β = (GB.prod GC).one g)
    (h2 : NeronModelInfra.schemeHomOverComp (prodInr GB) β = (GB.prod GC).one h) :
    β = (GB.prod GC).one (prodStr g h)
theorem

eq_one_of_prod_entries_eq_one

L365 ↗
GoodReductionJacobian.eq_one_of_prod_entries_eq_one
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section Product
variable {R : Type u} [CommRing R] {B C : Scheme.{u}}
  (g : B ⟶ Spec (CommRingCat.of R)) (h : C ⟶ Spec (CommRingCat.of R))
variable {g h}
section Identities
variable (GB : RelativeGroupLaw R g) (GC : RelativeGroupLaw R h)
Lean source · statement
theorem eq_one_of_prod_entries_eq_one (β : SchemeHomOver (prodStr g h) (prodStr g h))
    (hβ : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t (prodStr g
      h)),
      NeronModelInfra.schemeHomOverComp ((GB.prod GC).mul t x y) β =
        (GB.prod GC).mul t (NeronModelInfra.schemeHomOverComp x β)
          (NeronModelInfra.schemeHomOverComp y β))
    (h11 : NeronModelInfra.schemeHomOverComp (NeronModelInfra.schemeHomOverComp (prodInl GC) β)
      prodFst = GB.one g)
    (h12 : NeronModelInfra.schemeHomOverComp (NeronModelInfra.schemeHomOverComp (prodInl GC) β)
      prodSnd = GC.one g)
    (h21 : NeronModelInfra.schemeHomOverComp (NeronModelInfra.schemeHomOverComp (prodInr GB) β)
      prodFst = GB.one h)
    (h22 : NeronModelInfra.schemeHomOverComp (NeronModelInfra.schemeHomOverComp (prodInr GB) β)
      prodSnd = GC.one h) :
    β = (GB.prod GC).one (prodStr g h)
theorem

schemeHomOver_eq_of_epi_comp

L392 ↗
GoodReductionJacobian.schemeHomOver_eq_of_epi_comp
Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
Lean source · statement
theorem schemeHomOver_eq_of_epi_comp {R : Type u} [CommRing R] {X A A' : Scheme.{u}}
    {e : X ⟶ Spec (CommRingCat.of R)} {f : A ⟶ Spec (CommRingCat.of R)} {f' : A' ⟶ Spec
      (CommRingCat.of R)}
    (σ : SchemeHomOver e f) [Epi σ.1] (β γ : SchemeHomOver f f')
    (hσ : NeronModelInfra.schemeHomOverComp σ β = NeronModelInfra.schemeHomOverComp σ γ) : β = γ

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