NYLL
Module

Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
18 declarations indexed from sourceView source ↗

Module documentation

Local freeness of a finite flat pushforward

Constructs local trivializations of the pushforward from local trivializations on a finite flat cover.

Imports13
Imported by10

Declarations

def

trivCover

L59 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.trivCover
Documentation

The two-chart affine cover consisting of the whole affine scheme in both charts.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · full declaration
def trivCover (X : Scheme.{u}) [IsAffine X] : X.TwoAffineOpenCover where
  U0 := ⊤
  U1 := ⊤
  isAffineOpen_U0 := isAffineOpen_top X
  isAffineOpen_U1 := isAffineOpen_top X
  sup_eq_top := sup_top_eq _
  isAffineOpen_inf := by rw [inf_idem]; exact isAffineOpen_top X
abbrev

M₀

L68 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.M₀
Documentation

The pushforward of the unit module along the given map of affine schemes.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
abbrev M₀ : (Spec A).Modules
abbrev

P₀

L72 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.P₀
Documentation

The module of global sections of the pushed-forward unit module over the source ring.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
abbrev P₀ : ModuleCat.{u} A
theorem

isIso_fromTildeΓ

L75 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.isIso_fromTildeΓ
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
theorem isIso_fromTildeΓ : IsIso (Scheme.Modules.fromTildeΓ (R := A) (M₀ φ))
def

Bmod

L82 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.Bmod
Documentation

The target ring viewed as the underlying type of its module over the source ring.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
def Bmod (_φ : A ⟶ B) : Type u
instance

(anonymous instance)

L83 ↗
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
instance : CommRing (Bmod φ)
instance

algB

L84 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.algB
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
instance algB : Algebra A (Bmod φ)
lemma

algebraMap_Bmod

L86 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.algebraMap_Bmod
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
lemma algebraMap_Bmod (a : A) : algebraMap A (Bmod φ) a = (φ.hom a : B)
theorem

smul_P₀

L88 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.smul_P₀
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · full declaration
theorem smul_P₀ (a : A) (s : P₀ φ) :
    (show Γ(Spec B, ⊤) from a • s) = (show Γ(Spec B, ⊤) from (Spec.map φ).appTop ((Scheme.ΓSpecIso
      A).inv a)) * (show Γ(Spec B, ⊤) from s) := by
  change (show Γ(Spec B, ⊤) from (Spec.map φ).app ⊤ ((Spec A).ringCatSheaf.obj.map
      ((Limits.initialOpOfTerminal Limits.isTerminalTop).to (op ⊤))
        ((StructureSheaf.globalSectionsIso A).hom a))) *
    (show Γ(Spec B, ⊤) from s) = _
  rw [Subsingleton.elim ((Limits.initialOpOfTerminal Limits.isTerminalTop).to (op (⊤ : (Spec
    A).Opens))) (𝟙 _),
    CategoryTheory.Functor.map_id]
  rfl
theorem

exists_linearEquiv

L100 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.exists_linearEquiv
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
theorem exists_linearEquiv : Nonempty (P₀ φ ≃ₗ[A] Bmod φ)
theorem

finite_Bmod

L127 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.finite_Bmod
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
theorem finite_Bmod [IsFinite (Spec.map φ)] : Module.Finite A (Bmod φ)
theorem

flat_Bmod

L131 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.flat_Bmod
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
theorem flat_Bmod [Flat (Spec.map φ)] : Module.Flat A (Bmod φ)
theorem

finitePresentation_Bmod

L135 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.finitePresentation_Bmod
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
theorem finitePresentation_Bmod [IsFinite (Spec.map φ)] [LocallyOfFinitePresentation (Spec.map φ)] :
    Module.FinitePresentation A (Bmod φ)
theorem

finrank_Bmod

L142 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.finrank_Bmod
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
theorem finrank_Bmod [IsFinite (Spec.map φ)] [Flat (Spec.map φ)] (n : ℕ)
    (hn : ∀ p : Spec A, (Spec.map φ).finrank p = n)
    (K : Type u) [Field K] [Algebra A K] : Module.finrank K (K ⊗[A] Bmod φ) = n
theorem

core

L165 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.core
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
section affine
variable {A B : CommRingCat.{u}} (φ : A ⟶ B)
Lean source · statement
theorem core [IsFinite (Spec.map φ)] [Flat (Spec.map φ)] [LocallyOfFinitePresentation (Spec.map φ)]
    (n : ℕ) (hn : ∀ p : Spec A, (Spec.map φ).finrank p = n) :
    IsLocallyFreeOfRank n (M₀ φ)
def

restrictTriv

L185 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.restrictTriv
Documentation

Restrict the given module trivialization to a smaller open subset.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
Lean source · statement
def restrictTriv {Z : Scheme.{u}} {N : Z.Modules} {U₀ U : Z.Opens} (h : U ≤ U₀)
    (e : (Scheme.Modules.pullback U₀.ι).obj N ≅ 𝟙_ (U₀ : Scheme.{u}).Modules) :
    (Scheme.Modules.pullback U.ι).obj N ≅ 𝟙_ (U : Scheme.{u}).Modules
theorem

main

L193 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver.Ws31X1.main
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
namespace Ws31X1
open AlgebraicGeometry.Scheme.Modules
Lean source · statement
theorem main {Z T : Scheme.{u}} (q : Z ⟶ T) [IsFinite q] [Flat q] [LocallyOfFinitePresentation q]
  (n : ℕ)
    (hn : ∀ t : T, q.finrank t = n) (N : Z.Modules)
    (hN : ∀ t : T, ∃ W : T.Opens, t ∈ W ∧
      Nonempty ((Scheme.Modules.pullback (q ⁻¹ᵁ W).ι).obj N ≅ 𝟙_ (↑(q ⁻¹ᵁ W) :
        Scheme.{u}).Modules)) :
    IsLocallyFreeOfRank n ((Scheme.Modules.pushforward q).obj N)
theorem

isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver

L233 ↗
AlgebraicGeometry.Scheme.Modules.isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.TensorProduct
open Ws31X1 (main) in
with_weak_namespace _root_.AlgebraicGeometry.Scheme.Modules
Lean source · statement
theorem isLocallyFreeOfRank_pushforward_of_isFinite_of_flat_of_locallyTrivialOver
    {Z T : Scheme.{u}} (q : Z ⟶ T) [IsFinite q] [Flat q] [LocallyOfFinitePresentation q] (n : ℕ)
    (hn : ∀ t : T, q.finrank t = n) (N : Z.Modules)
    (hN : ∀ t : T, ∃ W : T.Opens, t ∈ W ∧
      Nonempty ((Scheme.Modules.pullback (q ⁻¹ᵁ W).ι).obj N ≅ 𝟙_ (↑(q ⁻¹ᵁ W) :
        Scheme.{u}).Modules)) :
    Scheme.Modules.IsLocallyFreeOfRank n ((Scheme.Modules.pushforward q).obj N)

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