NYLL
Module

Scheme_Modules_isLocallyFreeOfRank_tilde.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isLocallyFreeOfRank_tilde
7 declarations indexed from sourceView source ↗

Module documentation

Local freeness of the sheaf associated to a module

Local finite free descriptions of a module over an affine ring give local trivializations of its associated module sheaf.

Imports8
Imported by5

Declarations

theorem

free_finite_finrank_of_algebra_eq

L44 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_tilde.AlgebraicGeometry.free_finite_finrank_of_algebra_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_tilde
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
Lean source · full declaration
theorem free_finite_finrank_of_algebra_eq {A S : Type u} [CommRing A] [CommRing S]
    (M : Type u) [AddCommGroup M] [Module A M] (n : ℕ) (i₁ i₂ : Algebra A S) (h : i₁ = i₂)
    (H : letI := i₁;
      Module.Free S (S ⊗[A] M) ∧ Module.Finite S (S ⊗[A] M) ∧ Module.finrank S (S ⊗[A] M) = n) :
    letI := i₂;
      Module.Free S (S ⊗[A] M) ∧ Module.Finite S (S ⊗[A] M) ∧ Module.finrank S (S ⊗[A] M) = n := by
  subst h; exact H
theorem

free_finite_finrank_baseChange_away

L52 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_tilde.AlgebraicGeometry.free_finite_finrank_baseChange_away
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_tilde
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
Lean source · statement
theorem free_finite_finrank_baseChange_away {R : Type u} [CommRing R] (P : Type u)
    [AddCommGroup P] [Module R P] [Module.Finite R P] [Module.Projective R P] (n : ℕ)
    (hrk : ∀ (K : Type u) [Field K] [Algebra R K], Module.finrank K (K ⊗[R] P) = n)
    (r : R) (p : PrimeSpectrum R) (hr : r ∈ p.asIdeal.primeCompl)
    (hfree : Module.Free (Localization (.powers r)) (LocalizedModule (.powers r) P)) :
    Module.Free (Localization.Away r) (Localization.Away r ⊗[R] P) ∧
      Module.Finite (Localization.Away r) (Localization.Away r ⊗[R] P) ∧
      Module.finrank (Localization.Away r) (Localization.Away r ⊗[R] P) = n
def

tildeIsoFreeOfFinrankEq

L75 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_tilde.AlgebraicGeometry.tildeIsoFreeOfFinrankEq
Documentation

Identify the sheaf associated to a finite free module with the finite free sheaf of its rank.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_tilde
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
Lean source · statement
def tildeIsoFreeOfFinrankEq {S : CommRingCat.{u}} [Nontrivial S] (N : ModuleCat.{u} S)
    [Module.Free S N] [Module.Finite S N] {n : ℕ} (hn : Module.finrank S N = n) :
    tilde N ≅ SheafOfModules.free.{u} (ULift.{u} (Fin n))
theorem

opensMap_final''

L88 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_tilde.AlgebraicGeometry.Scheme.Modules.opensMap_final''
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_tilde
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Modules in
Lean source · statement
theorem Scheme.Modules.opensMap_final'' {X Y : Scheme.{u}} (f : X ⟶ Y) :
    (TopologicalSpace.Opens.map f.base).Final
def

pullbackObjFreeIso'

L94 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_tilde.AlgebraicGeometry.Scheme.Modules.pullbackObjFreeIso'
Documentation

Pullback preserves the free module sheaf on the given index type.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_tilde
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Modules in
Lean source · statement
def Scheme.Modules.pullbackObjFreeIso' {X Y : Scheme.{u}} (f : X ⟶ Y) (I : Type u) :
    (Scheme.Modules.pullback f).obj (SheafOfModules.free.{u} I) ≅ SheafOfModules.free.{u} I
def

isoFreeOfIsoPullback

L103 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_tilde.AlgebraicGeometry.Scheme.Modules.isoFreeOfIsoPullback
Documentation

Identify a module sheaf with a free sheaf when its pullback along an isomorphism is free.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_tilde
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open scoped _root_.AlgebraicGeometry.Scheme _root_.AlgebraicGeometry.Scheme.Modules in
Lean source · statement
def Scheme.Modules.isoFreeOfIsoPullback {U Y : Scheme.{u}} (e : Y ≅ U) (M : U.Modules)
    (I : Type u) (h : (Scheme.Modules.pullback e.hom).obj M ≅ SheafOfModules.free.{u} I) :
    M ≅ SheafOfModules.free.{u} I
theorem

isLocallyFreeOfRank_tilde

L113 ↗
AlgebraicGeometry.Scheme.Modules.isLocallyFreeOfRank_tilde
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_tilde
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.isLocallyFreeOfRank_tilde {R : CommRingCat.{u}} (P :
  ModuleCat.{u} R)
    [Module.Finite R P] [Module.Projective R P] (n : ℕ)
    (hrk : ∀ (K : Type u) [Field K] [Algebra R K], Module.finrank K (K ⊗[R] P) = n) :
    Scheme.Modules.IsLocallyFreeOfRank n (tilde P)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.