NYLL
Module

RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom
11 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law scheme Nsmul comp eq comp scheme Nsmul of hom

Imports8
Imported by5

Declarations

theorem

mono_iff_forall_injective_schemeHomOverComp

L37 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue.mono_iff_forall_injective_schemeHomOverComp
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17Glue
Lean source · full declaration
theorem mono_iff_forall_injective_schemeHomOverComp
    {B Y X : Scheme.{u}} {g : Y ⟶ B} {f : X ⟶ B} (u : SchemeHomOver g f) :
    Mono u.1 ↔ ∀ ⦃T : Scheme.{u}⦄ (t : T ⟶ B),
      Function.Injective (fun x : SchemeHomOver t g => NeronModelInfra.schemeHomOverComp x u) := by
  constructor
  · intro hm T t x y hxy
    apply Subtype.ext
    have h := congrArg Subtype.val hxy
    simp only [NeronModelInfra.schemeHomOverComp_coe] at h
    exact (cancel_mono u.1).mp h
  · intro h
    refine ⟨fun {T} a b hab => ?_⟩
    have hb : b ≫ g = a ≫ g := by
      rw [← u.2, ← Category.assoc, ← hab, Category.assoc]
    have key := @h T (a ≫ g) ⟨a, rfl⟩ ⟨b, hb⟩ (Subtype.ext (by simpa using hab))
    exact congrArg Subtype.val key
theorem

hom_one

L64 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue.hom_one
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17Glue
section Hom
variable {R : Type u} [CommRing R]
    {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of R)} (LB : RelativeGroupLaw R g)
    {J : Scheme.{u}} {f : J ⟶ Spec (CommRingCat.of R)} (L : RelativeGroupLaw R f)
    (u : SchemeHomOver g f)
    (hu : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t g),
      NeronModelInfra.schemeHomOverComp (LB.mul t x y) u =
        L.mul t (NeronModelInfra.schemeHomOverComp x u) (NeronModelInfra.schemeHomOverComp y u))
include hu in
Lean source · statement
theorem hom_one {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    NeronModelInfra.schemeHomOverComp (LB.one t) u = L.one t
theorem

hom_nsmul

L75 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue.hom_nsmul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17Glue
section Hom
variable {R : Type u} [CommRing R]
    {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of R)} (LB : RelativeGroupLaw R g)
    {J : Scheme.{u}} {f : J ⟶ Spec (CommRingCat.of R)} (L : RelativeGroupLaw R f)
    (u : SchemeHomOver g f)
    (hu : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t g),
      NeronModelInfra.schemeHomOverComp (LB.mul t x y) u =
        L.mul t (NeronModelInfra.schemeHomOverComp x u) (NeronModelInfra.schemeHomOverComp y u))
include hu in
Lean source · statement
theorem hom_nsmul {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (n : ℕ)
    (x : SchemeHomOver t g) :
    NeronModelInfra.schemeHomOverComp (LB.nsmul t n x) u =
      L.nsmul t n (NeronModelInfra.schemeHomOverComp x u)
theorem

nsmul_coe_eq_comp_schemeNsmul

L83 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue.nsmul_coe_eq_comp_schemeNsmul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17Glue
section Hom
variable {R : Type u} [CommRing R]
    {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of R)} (LB : RelativeGroupLaw R g)
    {J : Scheme.{u}} {f : J ⟶ Spec (CommRingCat.of R)} (L : RelativeGroupLaw R f)
    (u : SchemeHomOver g f)
    (hu : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t g),
      NeronModelInfra.schemeHomOverComp (LB.mul t x y) u =
        L.mul t (NeronModelInfra.schemeHomOverComp x u) (NeronModelInfra.schemeHomOverComp y u))
omit hu in
Lean source · statement
theorem nsmul_coe_eq_comp_schemeNsmul {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (n : ℕ) (x : SchemeHomOver t f) :
    (L.nsmul t n x).1 = x.1 ≫ L.schemeNsmul n
theorem

schemeNsmul_comp

L95 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue.schemeNsmul_comp
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17Glue
section Hom
variable {R : Type u} [CommRing R]
    {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of R)} (LB : RelativeGroupLaw R g)
    {J : Scheme.{u}} {f : J ⟶ Spec (CommRingCat.of R)} (L : RelativeGroupLaw R f)
    (u : SchemeHomOver g f)
    (hu : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t g),
      NeronModelInfra.schemeHomOverComp (LB.mul t x y) u =
        L.mul t (NeronModelInfra.schemeHomOverComp x u) (NeronModelInfra.schemeHomOverComp y u))
include hu in
Lean source · statement
theorem schemeNsmul_comp (n : ℕ) : LB.schemeNsmul n ≫ u.1 = u.1 ≫ L.schemeNsmul n
theorem

schemeNsmul_comp_eq_comp_schemeNsmul_of_hom

L104 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue.schemeNsmul_comp_eq_comp_schemeNsmul_of_hom
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17Glue
section Hom
variable {R : Type u} [CommRing R]
    {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of R)} (LB : RelativeGroupLaw R g)
    {J : Scheme.{u}} {f : J ⟶ Spec (CommRingCat.of R)} (L : RelativeGroupLaw R f)
    (u : SchemeHomOver g f)
    (hu : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t g),
      NeronModelInfra.schemeHomOverComp (LB.mul t x y) u =
        L.mul t (NeronModelInfra.schemeHomOverComp x u) (NeronModelInfra.schemeHomOverComp y u))
include hu in
Lean source · statement
theorem schemeNsmul_comp_eq_comp_schemeNsmul_of_hom :
    (∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)),
        NeronModelInfra.schemeHomOverComp (LB.one t) u = L.one t) ∧
    (∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (n : ℕ) (x : SchemeHomOver t g),
        NeronModelInfra.schemeHomOverComp (LB.nsmul t n x) u =
          L.nsmul t n (NeronModelInfra.schemeHomOverComp x u)) ∧
    (∀ n : ℕ, LB.schemeNsmul n ≫ u.1 = u.1 ≫ L.schemeNsmul n)
theorem

isFinite_schemeNsmul_of_isFinite_hom

L114 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue.isFinite_schemeNsmul_of_isFinite_hom
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17Glue
section Hom
variable {R : Type u} [CommRing R]
    {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of R)} (LB : RelativeGroupLaw R g)
    {J : Scheme.{u}} {f : J ⟶ Spec (CommRingCat.of R)} (L : RelativeGroupLaw R f)
    (u : SchemeHomOver g f)
    (hu : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t g),
      NeronModelInfra.schemeHomOverComp (LB.mul t x y) u =
        L.mul t (NeronModelInfra.schemeHomOverComp x u) (NeronModelInfra.schemeHomOverComp y u))
include hu in
Lean source · statement
theorem isFinite_schemeNsmul_of_isFinite_hom (hufin : IsFinite u.1) (n : ℕ)
    (hfin : IsFinite (L.schemeNsmul n)) : IsFinite (LB.schemeNsmul n)
theorem

one_coe_eq_comp_one

L122 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue.one_coe_eq_comp_one
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17Glue
section Hom
variable {R : Type u} [CommRing R]
    {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of R)} (LB : RelativeGroupLaw R g)
    {J : Scheme.{u}} {f : J ⟶ Spec (CommRingCat.of R)} (L : RelativeGroupLaw R f)
    (u : SchemeHomOver g f)
    (hu : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t g),
      NeronModelInfra.schemeHomOverComp (LB.mul t x y) u =
        L.mul t (NeronModelInfra.schemeHomOverComp x u) (NeronModelInfra.schemeHomOverComp y u))
omit hu in
Lean source · statement
theorem one_coe_eq_comp_one {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    (L.one t).1 = t ≫ (L.one (𝟙 (Spec (CommRingCat.of R)))).1
theorem

exists_schemeHomOver_pullback_unit_equiv_ker

L128 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue.exists_schemeHomOver_pullback_unit_equiv_ker
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17Glue
section Hom
variable {R : Type u} [CommRing R]
    {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of R)} (LB : RelativeGroupLaw R g)
    {J : Scheme.{u}} {f : J ⟶ Spec (CommRingCat.of R)} (L : RelativeGroupLaw R f)
    (u : SchemeHomOver g f)
    (hu : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t g),
      NeronModelInfra.schemeHomOverComp (LB.mul t x y) u =
        L.mul t (NeronModelInfra.schemeHomOverComp x u) (NeronModelInfra.schemeHomOverComp y u))
omit hu LB in
Lean source · statement
theorem exists_schemeHomOver_pullback_unit_equiv_ker :
    ∃ e : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)),
        SchemeHomOver t (pullback.snd u.1 (L.one (𝟙 (Spec (CommRingCat.of R)))).1) ≃
          {x : SchemeHomOver t g // NeronModelInfra.schemeHomOverComp x u = L.one t},
      ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
        (y : SchemeHomOver t (pullback.snd u.1 (L.one (𝟙 (Spec (CommRingCat.of R)))).1)),
        ((e t y : {_x : SchemeHomOver t g // _}) : SchemeHomOver t g).1 =
          y.1 ≫ pullback.fst u.1 (L.one (𝟙 (Spec (CommRingCat.of R)))).1
theorem

injective_schemeHomOverComp_of_mono_genericFibreRestrict

L160 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom.S17Glue.injective_schemeHomOverComp_of_mono_genericFibreRestrict
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace S17Glue
Lean source · full declaration
theorem injective_schemeHomOverComp_of_mono_genericFibreRestrict
    (R K : Type u) [CommRing R] [Field K] [Algebra R K]
    {X Y : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) (g : Y ⟶ Spec (CommRingCat.of R))
    (u : SchemeHomOver g f) [Mono (genericFibreRestrict R K f g u).1]
    {T : Scheme.{u}} (tK : T ⟶ Spec (CommRingCat.of K)) :
    Function.Injective (fun x : SchemeHomOver (tK ≫ specGenericFibreInclusion R K) g =>
      NeronModelInfra.schemeHomOverComp x u) := by
  intro x y hxy
  have h := congrArg Subtype.val hxy
  simp only [NeronModelInfra.schemeHomOverComp_coe] at h
  let lx : T ⟶ pullback g (specGenericFibreInclusion R K) := pullback.lift x.1 tK x.2
  let ly : T ⟶ pullback g (specGenericFibreInclusion R K) := pullback.lift y.1 tK y.2
  have key : lx ≫ (genericFibreRestrict R K f g u).1 = ly ≫ (genericFibreRestrict R K f g u).1 := by
    apply pullback.hom_ext
    · simp only [genericFibreRestrict, Category.assoc, pullback.lift_fst]
      rw [← Category.assoc, ← Category.assoc, pullback.lift_fst, pullback.lift_fst, h]
    · simp only [genericFibreRestrict, Category.assoc, pullback.lift_snd]
      rw [pullback.lift_snd, pullback.lift_snd]
  have hl : lx = ly := (cancel_mono _).mp key
  apply Subtype.ext
  have := congrArg (fun m => m ≫ pullback.fst g (specGenericFibreInclusion R K)) hl
  simp only [lx, ly, pullback.lift_fst] at this
  exact this
theorem

schemeNsmul_comp_eq_comp_schemeNsmul_of_hom

L186 ↗
GoodReductionJacobian.RelativeGroupLaw.schemeNsmul_comp_eq_comp_schemeNsmul_of_hom
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_schemeNsmul_comp_eq_comp_schemeNsmul_of_hom
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
Lean source · statement
theorem _root_.GoodReductionJacobian.RelativeGroupLaw.schemeNsmul_comp_eq_comp_schemeNsmul_of_hom
    {R : Type u} [CommRing R]
    {B : Scheme.{u}} {g : B ⟶ Spec (CommRingCat.of R)} (LB : RelativeGroupLaw R g)
    {J : Scheme.{u}} {f : J ⟶ Spec (CommRingCat.of R)} (L : RelativeGroupLaw R f)
    (u : SchemeHomOver g f)
    (hu : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t g),
      NeronModelInfra.schemeHomOverComp (LB.mul t x y) u =
        L.mul t (NeronModelInfra.schemeHomOverComp x u) (NeronModelInfra.schemeHomOverComp y u)) :
    (∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)),
        NeronModelInfra.schemeHomOverComp (LB.one t) u = L.one t) ∧
    (∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (n : ℕ) (x : SchemeHomOver t g),
        NeronModelInfra.schemeHomOverComp (LB.nsmul t n x) u =
          L.nsmul t n (NeronModelInfra.schemeHomOverComp x u)) ∧
    (∀ n : ℕ, LB.schemeNsmul n ≫ u.1 = u.1 ≫ L.schemeNsmul n)

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