@[reducible, inline]

abbrev ReflexiveSheaf.dualSheaf (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Type (max u_2 u_1)

The dual sheaf F^∨ = Hom_R(F, R) of a module M, the local analog of the dual of a sheaf of 𝒪_X-modules.

@[reducible, inline]

abbrev ReflexiveSheaf.doubleDualSheaf (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Type (max (max u_2 u_1) u_1)

The double dual sheaf F^{∨∨} of a module, the target of the reflexivity map F → F^{∨∨}.

@[reducible, inline]

abbrev ReflexiveSheaf.doubleDualMap (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : M →ₗ[R] doubleDualSheaf R M

The reflexivity map F → F^{∨∨}, evaluation at the dual.

theorem ReflexiveSheaf.isReflexive_iff_eval_bijective {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : Module.IsReflexive R M ↔ Function.Bijective ⇑(Module.Dual.eval R M)

M is reflexive iff the evaluation map M → M^{∨∨} is a bijection.

theorem ReflexiveSheaf.eval_apply_eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (m : M) (φ : Module.Dual R M) : ((doubleDualMap R M) m) φ = φ m

Evaluation formula: (eval m)(φ) = φ(m).

theorem ReflexiveSheaf.locallyFree_isReflexive {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Module.IsReflexive R M

A finitely generated projective module (a locally free sheaf) is reflexive: the double-dual map is an isomorphism.

noncomputable def ReflexiveSheaf.doubleDualLocallyFree {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] : M ≃ₗ[R] doubleDualSheaf R M

The double-dual isomorphism M ≃ M^{∨∨} packaged as a LinearEquiv for finitely generated projective modules.

instance ReflexiveSheaf.freeModule_isReflexive {R : Type u_1} [CommRing R] (n : ℕ) : Module.IsReflexive R (Fin n → R)

Free modules of finite rank are reflexive.

noncomputable def ReflexiveSheaf.dualTensorHomLocallyFree (R : Type u_1) (M : Type u_2) (N : Type u_3) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Free R M] [Module.Finite R M] : (M →ₗ[R] N) ≃ₗ[R] TensorProduct R (Module.Dual R M) N

The natural identification Hom_R(M, N) ≃ M^∨ ⊗ N for a finitely-generated free M, the basic dual-tensor-hom isomorphism for locally free sheaves.

def ReflexiveSheaf.endRankOneEquiv (R : Type u_1) [CommRing R] : ((Fin 1 → R) →ₗ[R] Fin 1 → R) ≃ₗ[R] R

The ring of endomorphisms of the rank-one free module is isomorphic to R itself, via evaluation at a basis vector.

noncomputable def ReflexiveSheaf.dualTensorRankOneIso (R : Type u_1) [CommRing R] : TensorProduct R (Module.Dual R (Fin 1 → R)) (Fin 1 → R) ≃ₗ[R] R

The dual-tensor-hom contraction for the rank-one free module collapses to the ring R.

instance ReflexiveSheaf.invertibleSheaf_isReflexive (R : Type u_1) [CommRing R] : Module.IsReflexive R (Fin 1 → R)

An invertible sheaf (here represented as the rank-one free module) is reflexive.