AlgebraicGeometry.Scheme.Modules.exists_isInvertible_normModule_pullback_pullback_iso_pullback
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.Scheme.Modules
universe u
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs in
open Scheme_Modules_exists_isInvertible_normModule_pullback_pullback_iso_pullback in
open _root_.CategoryTheory in
open _root_.CategoryTheory.Limits in
open _root_.CategoryTheory.MonoidalCategory in
open _root_.AlgebraicGeometry in
open _root_.NeronModelInfra in
open _root_.GoodReductionJacobian in
open _root_.AlgebraicGeometry.RelPicard inLean source · statement
theorem exists_isInvertible_normModule_pullback_pullback_iso_pullback
{X Y T : Scheme.{u}} (π : X ⟶ Y) [IsFinite π] [Flat π] [LocallyOfFinitePresentation π]
(d : ℕ) (hd : ∀ y : Y, π.finrank y = d) (q : Y ⟶ T)
{M : T.Modules} (hM : Scheme.Modules.IsInvertible M) :
∃ N : T.Modules, Scheme.Modules.IsInvertible N ∧
Nonempty (Scheme.Modules.normModule π d ((Scheme.Modules.pullback π).obj
((Scheme.Modules.pullback q).obj M)) ≅
(Scheme.Modules.pullback q).obj N)