AlgebraicGeometry.Scheme.Modules.IsInvertible.isIso_ev_app_and_isIso_curry_braiding_ev
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_isIso_ev_app_and_isIso_curry_braiding_ev
attribute [-instance]
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'
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
attribute [-simp] PresheafOfModules.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometryLean source · statement
theorem
_root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.isIso_ev_app_and_isIso_curry_braiding_ev
{X : Scheme.{u}} {L : X.Modules} (hL : Scheme.Modules.IsInvertible L) :
(∀ F : X.Modules, IsIso ((ihom.ev L).app F)) ∧
IsIso (MonoidalClosed.curry
((β_ (Scheme.Modules.dual L) L).hom ≫ (ihom.ev L).app (𝟙_ X.Modules)))