Module

Scheme_Modules_IsLocallyFreeOfRank_of_iso.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsLocallyFreeOfRank_of_iso

1 declaration indexed from sourceView source ↗

Module documentation

Local freeness preserved by isomorphisms

Transfers local freeness of a fixed rank along an isomorphism of scheme modules.

Imports1

Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesLocallyFreeOfRank

Imported by10

theorem

of_iso

L28 ↗

AlgebraicGeometry.Scheme.Modules.IsLocallyFreeOfRank.of_iso

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsLocallyFreeOfRank_of_iso
universe u
open CategoryTheory AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.IsLocallyFreeOfRank.of_iso {X : Scheme.{u}} {n :
  ℕ} {M N : X.Modules} (e : M ≅ N) (h : Scheme.Modules.IsLocallyFreeOfRank n M) :
    Scheme.Modules.IsLocallyFreeOfRank n N

Module documentation

Local freeness preserved by isomorphisms

Declarations

of_iso