Module

AbelianSchemePropertyBundle_baseChange_of_field.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.AbelianSchemePropertyBundle_baseChange_of_field

1 declaration indexed from sourceView source ↗

Module documentation

Abelian Scheme Property Bundle base Change of field

Imports8

Mathlib.CategoryTheory.MorphismProperty.Limits
Mathlib.AlgebraicGeometry.Geometrically.Integral
Mathlib.AlgebraicGeometry.Geometrically.Basic
Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Morphisms.Proper
Nyll.AlgebraicCurves.Geometry.AbelianSchemes.GroupLaw.BaseChange
Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.abelianSchemePropertyBundle_fibreStr
Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.AbelianSchemePropertyBundle_geometricallyIntegral

Imported by4

theorem

baseChange_of_field

L35 ↗

GoodReductionJacobian.AbelianSchemePropertyBundle.baseChange_of_field

Source context 5 commands

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

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

Lean source · statement

theorem _root_.GoodReductionJacobian.AbelianSchemePropertyBundle.baseChange_of_field
    {R : Type u} [CommRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
    (hA : AbelianSchemePropertyBundle R f) {k : Type u} [Field k]
    (ι : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R)) :
    AbelianSchemePropertyBundle k (pullback.snd f ι)

Module documentation

Abelian Scheme Property Bundle base Change of field

Declarations

baseChange_of_field