Module

RelativeGroupLaw_exists_isClosedImmersion_comp_eq_one_iff.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_exists_isClosedImmersion_comp_eq_one_iff

2 declarations indexed from sourceView source ↗

Module documentation

Relative Group Law exists is Closed Immersion comp eq one iff

Imports4

Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver
Nyll.AlgebraicCurves.Geometry.Picard.RelativeGroupLaw

Imported by1

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.All

theorem

aux

L51 ↗

AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_exists_isClosedImmersion_comp_eq_one_iff.GoodReductionJacobian.RelativeGroupLaw.KerClosedAux.aux

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isClosedImmersion_comp_eq_one_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
namespace GoodReductionJacobian
namespace RelativeGroupLaw
namespace KerClosedAux
open _root_.GoodReductionJacobian.RelativeGroupLaw
open _root_.GoodReductionJacobian

Lean source · statement

theorem aux {k : Type u} [Field k] {D D₁ D₂ : Scheme.{u}}
    (d : D ⟶ Spec (CommRingCat.of k)) (d₁ : D₁ ⟶ Spec (CommRingCat.of k)) (d₂ : D₂ ⟶ Spec
      (CommRingCat.of k))
    (n₁ : D ⟶ D₁) (n₂ : D ⟶ D₂) (hn₁ : n₁ ≫ d₁ = d) (hn₂ : n₂ ≫ d₂ = d)
    (e₁ : Spec (CommRingCat.of k) ⟶ D₁) (e₂ : Spec (CommRingCat.of k) ⟶ D₂)
    (he₁ : e₁ ≫ d₁ = 𝟙 _) (he₂ : e₂ ≫ d₂ = 𝟙 _) :
    ∃ (K : Scheme.{u}) (j : K ⟶ D), IsClosedImmersion j ∧
      ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (a : T ⟶ D), a ≫ d = t →
        ((a ≫ n₁ = t ≫ e₁ ∧ a ≫ n₂ = t ≫ e₂) ↔ ∃ b : T ⟶ K, b ≫ j = a)

theorem

exists_isClosedImmersion_comp_eq_one_iff

L93 ↗

GoodReductionJacobian.RelativeGroupLaw.exists_isClosedImmersion_comp_eq_one_iff

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_exists_isClosedImmersion_comp_eq_one_iff
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian

Lean source · statement

theorem _root_.GoodReductionJacobian.RelativeGroupLaw.exists_isClosedImmersion_comp_eq_one_iff
    {k : Type u} [Field k] {D D₁ D₂ : Scheme.{u}}
    {d : D ⟶ Spec (CommRingCat.of k)} {d₁ : D₁ ⟶ Spec (CommRingCat.of k)} {d₂ : D₂ ⟶ Spec
      (CommRingCat.of k)}
    (L₁ : RelativeGroupLaw k d₁) (L₂ : RelativeGroupLaw k d₂)
    (ν₁ : SchemeHomOver d d₁) (ν₂ : SchemeHomOver d d₂) :
    ∃ (K : Scheme.{u}) (j : K ⟶ D), IsClosedImmersion j ∧
      ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) (a : SchemeHomOver t d),
        (NeronModelInfra.schemeHomOverComp a ν₁ = L₁.one t ∧ NeronModelInfra.schemeHomOverComp a ν₂
          = L₂.one t) ↔
          ∃ b : T ⟶ K, b ≫ j = a.1

Module documentation

Relative Group Law exists is Closed Immersion comp eq one iff

Declarations

aux

exists_isClosedImmersion_comp_eq_one_iff