AlgebraicGeometry.RelEffCartierDiv.isInvertible_twistModule_and_nonempty_pullback_iso
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_isInvertible_twistModule_and_nonempty_pullback_iso
attribute [-instance]
AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
AlgebraicGeometry.Scheme.Modules.pullback_monoidal
AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
PresheafOfModules.PullbackMonoidal.pullback_monoidal
PresheafOfModules.PullbackMonoidal.isIso_δ
PresheafOfModules.pushforward_laxMonoidal
PresheafOfModules.PullbackMonoidal.isIso_η
PresheafOfModules.free_monoidal
PresheafOfModules.restrictScalars_laxMonoidal
PresheafOfModules.PullbackMonoidal.isIso_δ_gS
PresheafOfModules.pullback_oplaxMonoidal
instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
PresheafOfModules.pullback_monoidal'
attribute [-simp]
PresheafOfModules.freeεIso_hom_app
PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.NeronModelInfraLean source · statement
theorem _root_.AlgebraicGeometry.RelEffCartierDiv.isInvertible_twistModule_and_nonempty_pullback_iso
{R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
[IsSeparated c] [SmoothOfRelativeDimension 1 c]
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {r : ℕ} {T : Scheme.{u}}
{t : T ⟶ Spec (CommRingCat.of R)} (D : RelEffCartierDiv c r t) :
Scheme.Modules.IsInvertible (D.twistModule c ε) ∧
Nonempty ((Scheme.Modules.pullback (RelPicard.rigSection c t ε)).obj (D.twistModule c ε) ≅
𝟙_ T.Modules)