def SheafTensorExact.IsLocallyFree (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] (n : ℕ) : Prop

Locally free module of rank n: there is a finite set S ⊆ R generating the unit ideal such that for each f ∈ S, the localization M[f⁻¹] is a free R[f⁻¹]-module of rank n. This is the algebraic version of "locally free sheaf trivializes on the principal open cover {D(f) : f ∈ S}".

theorem SheafTensorExact.locally_free_isFlat (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] (n : ℕ) (hlf : IsLocallyFree R M n) : Module.Flat R M

A locally free module is flat: flatness is a local property, and free modules over the localizations are flat.

theorem SheafTensorExact.locally_free_tensor_exact (R : Type u_1) [CommRing R] (L : Type u_2) [AddCommGroup L] [Module R L] (n : ℕ) (hlf : IsLocallyFree R L n) {F' : Type u_3} {F : Type u_4} {F'' : Type u_5} [AddCommGroup F'] [Module R F'] [AddCommGroup F] [Module R F] [AddCommGroup F''] [Module R F''] (f : F' →ₗ[R] F) (g : F →ₗ[R] F'') (hex : Function.Exact ⇑f ⇑g) : Function.Exact ⇑(LinearMap.rTensor L f) ⇑(LinearMap.rTensor L g)

Tensoring with a locally free module preserves exactness (right tensor version): if F' → F → F'' is exact and L is locally free, then F' ⊗ L → F ⊗ L → F'' ⊗ L is exact.

theorem SheafTensorExact.locally_free_tensor_short_exact (R : Type u_1) [CommRing R] (L : Type u_2) [AddCommGroup L] [Module R L] (n : ℕ) (hlf : IsLocallyFree R L n) {F' : Type u_3} {F : Type u_4} {F'' : Type u_5} [AddCommGroup F'] [Module R F'] [AddCommGroup F] [Module R F] [AddCommGroup F''] [Module R F''] (f : F' →ₗ[R] F) (g : F →ₗ[R] F'') (hinj : Function.Injective ⇑f) (hex : Function.Exact ⇑f ⇑g) (hsurj : Function.Surjective ⇑g) : Function.Injective ⇑(LinearMap.rTensor L f) ∧ Function.Exact ⇑(LinearMap.rTensor L f) ⇑(LinearMap.rTensor L g) ∧ Function.Surjective ⇑(LinearMap.rTensor L g)

Tensoring with a locally free module preserves short exact sequences: 0 → F' → F → F'' → 0 exact and L locally free imply 0 → F' ⊗ L → F ⊗ L → F'' ⊗ L → 0 is exact.

theorem SheafTensorExact.locally_free_lTensor_exact (R : Type u_1) [CommRing R] (L : Type u_2) [AddCommGroup L] [Module R L] (n : ℕ) (hlf : IsLocallyFree R L n) {F' : Type u_3} {F : Type u_4} {F'' : Type u_5} [AddCommGroup F'] [Module R F'] [AddCommGroup F] [Module R F] [AddCommGroup F''] [Module R F''] (f : F' →ₗ[R] F) (g : F →ₗ[R] F'') (hex : Function.Exact ⇑f ⇑g) : Function.Exact ⇑(LinearMap.lTensor L f) ⇑(LinearMap.lTensor L g)

Left-tensor version of locally_free_tensor_exact: tensoring on the left with a locally free module preserves exactness.

theorem SheafTensorExact.invertible_sheaf_tensor_exact (R : Type u_1) [CommRing R] (L : Type u_2) [AddCommGroup L] [Module R L] (hlf : IsLocallyFree R L 1) {F' : Type u_3} {F : Type u_4} {F'' : Type u_5} [AddCommGroup F'] [Module R F'] [AddCommGroup F] [Module R F] [AddCommGroup F''] [Module R F''] (f : F' →ₗ[R] F) (g : F →ₗ[R] F'') (hex : Function.Exact ⇑f ⇑g) : Function.Exact ⇑(LinearMap.rTensor L f) ⇑(LinearMap.rTensor L g)

Invertible sheaves preserve exactness: tensoring an exact sequence with a line bundle (locally free of rank 1) preserves exactness. This is the algebraic shadow of the fact that twisting by O(D) is an exact functor.