AlgebraicGeometry.RelPicard.RigidifiedLineBundle.nonempty_pullback_rigSection_pullbackAlong_iso_tensorUnit
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.RelPicard.RigidifiedLineBundle
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfraLean source · statement
theorem nonempty_pullback_rigSection_pullbackAlong_iso_tensorUnit
{k : Type u} [Field k] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of k)}
{ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) c}
(N : RigidifiedLineBundle c ε (𝟙 (Spec (CommRingCat.of k))))
(P : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) c)
{T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of k)) :
Nonempty ((Scheme.Modules.pullback (rigSection c t P)).obj (N.pullbackAlong ⟨t,
Category.comp_id t⟩).L ≅
𝟙_ T.Modules)