Module

abelianSchemePropertyBundle_fibreStr.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.abelianSchemePropertyBundle_fibreStr

1 declaration indexed from sourceView source ↗

Module documentation

abelian Scheme Property Bundle fibre Str

Imports3

Imported by5

theorem

abelianSchemePropertyBundle_fibreStr

L31 ↗

GoodReductionJacobian.abelianSchemePropertyBundle_fibreStr

Source context 5 commands

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

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

Lean source · statement

theorem _root_.GoodReductionJacobian.abelianSchemePropertyBundle_fibreStr
    {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
    (hA : AbelianSchemePropertyBundle R f) (s : (Spec (CommRingCat.of R) : Scheme.{u})) :
    AbelianSchemePropertyBundle (RelativeGroupLaw.baseResidueField s) (RelativeGroupLaw.fibreStr f
      s)

Module documentation

abelian Scheme Property Bundle fibre Str

Declarations

abelianSchemePropertyBundle_fibreStr