Module

SubPicCondition.lean

Nyll.AlgebraicCurves.Geometry.Picard.SubPicCondition

2 declarations indexed from sourceView source ↗

Module documentation

Pullback-stable conditions on rigidified line bundles, containing the unit and respecting isomorphism.

Imports1

Nyll.AlgebraicCurves.Geometry.Picard.Functor

Imported by19

structure

SubPicCondition

L32 ↗

AlgebraicGeometry.RelPicard.SubPicCondition

Documentation

A condition on rigidified line bundles containing the unit and stable under isomorphism and pullback.

Source context 4 commands

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

namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
variable {R : Type u} [CommRing R] {C : Scheme.{u}}

Lean source · full declaration

structure SubPicCondition (c : C ⟶ Spec (CommRingCat.of R))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) : Type (u + 1) where
  /-- The predicate on rigidified line bundles over each test scheme. -/
  P : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)), RigidifiedLineBundle c ε t → Prop
  /-- The unit rigidified line bundle satisfies the condition. -/
  unit_mem : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)), P t (RigidifiedLineBundle.unit t)
  /-- An isomorphism of underlying line bundles preserves the condition. -/
  congr : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M M' : RigidifiedLineBundle c ε t),
    Nonempty (M.L ≅ M'.L) → P t M → P t M'
  /-- Pullback along a morphism of test schemes preserves the condition. -/
  pullback_mem : ∀ {T T' : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    (t' : T' ⟶ Spec (CommRingCat.of R))
    (ψ : SchemeHomOver t' t) (M : RigidifiedLineBundle c ε t), P t M → P t' (M.pullbackAlong ψ)

def

top

L47 ↗

AlgebraicGeometry.RelPicard.SubPicCondition.top