structure
L36 ↗AbelianSchemePropertyBundle
GoodReductionJacobian.AbelianSchemePropertyBundle
The smooth, proper, connected-fibre and group-law properties of a morphism over Spec R.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra
namespace GoodReductionJacobian
section AbstractCarriers
variable (R : Type u) [CommRing R]Lean source · full declaration
structure AbelianSchemePropertyBundle {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of R)) :
Prop where
/-- The structure morphism is smooth. -/
smooth : Smooth f
/-- The structure morphism is proper. -/
proper : IsProper f
/-- Every fibre of the structure morphism is connected. -/
connectedFibres : ∀ s : Spec (CommRingCat.of R), _root_.IsConnected (f.base ⁻¹' {s})
/-- The structure morphism admits a relative group law. -/
hasGroupLaw : Nonempty (RelativeGroupLaw R f)