AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.nonempty_module_tensor_invModule_iso
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_nonempty_module_tensor_invModule_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
pullback_monoidal
isIso_δ
PresheafOfModules.pushforward_laxMonoidal
isIso_η
PresheafOfModules.free_monoidal
PresheafOfModules.restrictScalars_laxMonoidal
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_.AlgebraicGeometryLean source · statement
theorem
_root_.AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.nonempty_module_tensor_invModule_iso
{X : Scheme.{u}} {I : X.IdealSheafData} (hI : I.IsInvertible) :
Nonempty (I.module ⊗ I.invModule ≅ 𝟙_ X.Modules) ∧
Nonempty (I.invModule ⊗ I.module ≅ 𝟙_ X.Modules)