NYLL
Module

RepresentsRelSubPic_flat_mul_fst_snd.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_flat_mul_fst_snd
5 declarations indexed from sourceView source ↗

Module documentation

Flatness of relative Picard multiplication

Multiplication on two points factors through an automorphism of the fibre product and its second projection. This proves flatness from the flat structure morphism.

Imports6
Imported by2

Declarations

theorem

mul_inv_cancel'

L60 ↗
JacobianVarieties.Picard.Proofs.FlatMultiplication.AlgebraicGeometry.RelPicard.GrpMulFlat.mul_inv_cancel'
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FlatMultiplication
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
namespace AlgebraicGeometry
namespace RelPicard
namespace GrpMulFlat
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f) (hc : G.IsCommutative)
include hc in
Lean source · statement
theorem mul_inv_cancel' {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x : SchemeHomOver t f) :
    G.mul t x (G.inv t x) = G.one t
theorem

inv_unique

L65 ↗
JacobianVarieties.Picard.Proofs.FlatMultiplication.AlgebraicGeometry.RelPicard.GrpMulFlat.inv_unique
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FlatMultiplication
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
namespace AlgebraicGeometry
namespace RelPicard
namespace GrpMulFlat
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f) (hc : G.IsCommutative)
include hc in
Lean source · statement
theorem inv_unique {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t f)
    (hy : G.mul t y x = G.one t) : y = G.inv t x
theorem

one_natural

L72 ↗
JacobianVarieties.Picard.Proofs.FlatMultiplication.AlgebraicGeometry.RelPicard.GrpMulFlat.one_natural
Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FlatMultiplication
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
namespace AlgebraicGeometry
namespace RelPicard
namespace GrpMulFlat
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f) (hc : G.IsCommutative)
Lean source · statement
theorem one_natural {T T' : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (t' : T' ⟶ Spec (CommRingCat.of R))
    (ψ : T' ⟶ T) (hψ : ψ ≫ t = t') :
    GoodReductionJacobian.schemeHomOverComp ψ hψ (G.one t) = G.one t'
theorem

inv_natural

L85 ↗
JacobianVarieties.Picard.Proofs.FlatMultiplication.AlgebraicGeometry.RelPicard.GrpMulFlat.inv_natural
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FlatMultiplication
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
namespace AlgebraicGeometry
namespace RelPicard
namespace GrpMulFlat
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
  (G : RelativeGroupLaw R f) (hc : G.IsCommutative)
include hc in
Lean source · statement
theorem inv_natural {T T' : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (t' : T' ⟶ Spec (CommRingCat.of R))
    (ψ : T' ⟶ T) (hψ : ψ ≫ t = t') (x : SchemeHomOver t f) :
    GoodReductionJacobian.schemeHomOverComp ψ hψ (G.inv t x) =
      G.inv t' (GoodReductionJacobian.schemeHomOverComp ψ hψ x)
theorem

flat_mul_fst_snd

L96 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.flat_mul_fst_snd
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FlatMultiplication
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.RelPicard
universe u
open AlgebraicGeometry.RelPicard.GrpMulFlat in
Lean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic.flat_mul_fst_snd
    {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
    {P : SubPicGroupCondition c ε} {D : RelativePic0Designation R c}
    (h : RepresentsRelSubPic c ε P.toSubPicCondition D) [Flat D.toBase] :
    Flat (h.relativeGroupLaw.mul (pullback.fst D.toBase D.toBase ≫ D.toBase)
      ⟨pullback.fst D.toBase D.toBase, rfl⟩
      ⟨pullback.snd D.toBase D.toBase, pullback.condition.symm⟩).1

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