NYLL
Module

Scheme_Modules_IsInvertible_exists_nonempty_pullback_preimage_iso_tensorUnit_of_isFinite.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_exists_nonempty_pullback_preimage_iso_tensorUnit_of_isFinite
17 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Invertible exists nonempty pullback preimage iso tensor Unit of is

Finite

Imports14
Imported by6

Declarations

theorem

finite_maximalSpectrum_of_isLocalRing_of_moduleFinite

L49 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.Module.Invertible.finite_maximalSpectrum_of_isLocalRing_of_moduleFinite
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
namespace Module
open _root_.Module
namespace Invertible
open _root_.Module.Invertible
open _root_.Module.Invertible
open _root_.Module
Lean source · statement
theorem finite_maximalSpectrum_of_isLocalRing_of_moduleFinite
    (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [Module.Finite R S] :
    Finite (MaximalSpectrum S)
theorem

exists_notMem_linearEquiv_localizedModule_away_of_module_finite

L87 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.Module.Invertible.exists_notMem_linearEquiv_localizedModule_away_of_module_finite
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
namespace Module
open _root_.Module
namespace Invertible
open _root_.Module.Invertible
open _root_.Module.Invertible
open _root_.Module
Lean source · statement
theorem exists_notMem_linearEquiv_localizedModule_away_of_module_finite
    {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] [Module.Finite A B] (P : Type u)
      [AddCommGroup P]
    [Module B P] [Module.Finite B P] [Module.Invertible B P] (𝔭 : Ideal A) [𝔭.IsPrime] :
    ∃ a : A, a ∉ 𝔭 ∧ Nonempty (LocalizedModule (Submonoid.powers (algebraMap A B a)) P
      ≃ₗ[Localization.Away (algebraMap A B a)]
      Localization.Away (algebraMap A B a))
def

ALGStatement

L151 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.AlgebraicGeometry.Scheme.Modules.B1Glue.ALGStatement
Documentation

The algebraic local triviality assertion for an invertible module over a finite algebra after inverting a base element outside a given prime.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace B1Glue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
Lean source · statement
def ALGStatement : Prop
abbrev

res

L161 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.AlgebraicGeometry.Scheme.Modules.B1Glue.res
Documentation

Restrict a section of M along the open inclusion h.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace B1Glue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
abbrev res (M : Y.Modules) {U W : Y.Opens} (h : W ≤ U) (s : Γ(M, U)) : Γ(M, W)
lemma

res_res

L164 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.AlgebraicGeometry.Scheme.Modules.B1Glue.res_res
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace B1Glue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
lemma res_res (M : Y.Modules) {U W W' : Y.Opens} (h : W ≤ U) (h' : W' ≤ W) (s : Γ(M, U)) :
    res M h' (res M h s) = res M (h'.trans h) s
lemma

res_smul

L170 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.AlgebraicGeometry.Scheme.Modules.B1Glue.res_smul
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace B1Glue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
lemma res_smul (M : Y.Modules) {U W : Y.Opens} (h : W ≤ U) (g : Γ(Y, U)) (s : Γ(M, U)) :
    res M h (g • s) = Y.presheaf.map (homOfLE h).op g • res M h s
lemma

presheaf_map_map

L174 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.AlgebraicGeometry.Scheme.Modules.B1Glue.presheaf_map_map
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace B1Glue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
lemma presheaf_map_map (M : Y.Modules) {A B C : Y.Opens} (f : B ⟶ A) (g : C ⟶ B) (k : C ⟶ A) (x :
  Γ(M, A)) :
    M.presheaf.map g.op (M.presheaf.map f.op x) = M.presheaf.map k.op x
lemma

ringCat_presheaf_map_map

L179 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.AlgebraicGeometry.Scheme.Modules.B1Glue.ringCat_presheaf_map_map
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace B1Glue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
lemma ringCat_presheaf_map_map {A B C : Y.Opens} (f : B ⟶ A) (g : C ⟶ B) (k : C ⟶ A) (x : Γ(Y, A)) :
    Y.presheaf.map g.op (Y.presheaf.map f.op x) = Y.presheaf.map k.op x
theorem

isFrameOn_of_forall_exists

L183 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.AlgebraicGeometry.Scheme.Modules.B1Glue.isFrameOn_of_forall_exists
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace B1Glue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem isFrameOn_of_forall_exists {M : Y.Modules} {U : Y.Opens} {s : Γ(M, U)} {V : Y.Opens} (_hVU
  : V ≤ U)
    (h : ∀ x ∈ V, ∃ W : Y.Opens, x ∈ W ∧ W ≤ V ∧ Scheme.Modules.IsFrameOn s W) :
    Scheme.Modules.IsFrameOn s V
lemma

res_rfl

L240 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.AlgebraicGeometry.Scheme.Modules.B1Glue.res_rfl
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace B1Glue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
lemma res_rfl (M : Y.Modules) {U : Y.Opens} (s : Γ(M, U)) : res M (le_refl U) s = s
theorem

isFrameOn_of_res_eq_smul

L245 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.AlgebraicGeometry.Scheme.Modules.B1Glue.isFrameOn_of_res_eq_smul
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace B1Glue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem isFrameOn_of_res_eq_smul {M : Y.Modules} {U₁ U₂ W : Y.Opens} {s : Γ(M, U₁)} {p : Γ(M, U₂)}
    (h₁ : W ≤ U₁) (h₂ : W ≤ U₂) (hs : Scheme.Modules.IsFrameOn s W) (u : Γ(Y, W))
    (hu : res M h₁ s = u • res M h₂ p) :
    Scheme.Modules.IsFrameOn p W
theorem

exists_forall_exists_pow_smul_eq_of_linearEquiv

L279 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.AlgebraicGeometry.Scheme.Modules.B1Glue.exists_forall_exists_pow_smul_eq_of_linearEquiv
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace B1Glue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem exists_forall_exists_pow_smul_eq_of_linearEquiv {B : Type u} [CommRing B] {P : Type u}
  [AddCommGroup P]
    [Module B P] (a : B)
    (e : LocalizedModule (Submonoid.powers a) P ≃ₗ[Localization.Away a] Localization.Away a) :
    ∃ p : P, ∀ y : P, ∃ (n : ℕ) (c : B), (a ^ n) • y = c • p
theorem

isFrameOn_basicOpen_of_forall_exists_pow_smul_eq

L312 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.AlgebraicGeometry.Scheme.Modules.B1Glue.isFrameOn_basicOpen_of_forall_exists_pow_smul_eq
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace B1Glue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem isFrameOn_basicOpen_of_forall_exists_pow_smul_eq [IsAffine Y] {N : Y.Modules}
    (hN : Scheme.Modules.IsInvertible N) (p : Γ(N, ⊤)) (a : Γ(Y, ⊤))
    (hgen : ∀ y : Γ(N, ⊤), ∃ (n : ℕ) (c : Γ(Y, ⊤)), (a ^ n) • y = c • p) :
    Scheme.Modules.IsFrameOn p (Y.basicOpen a)
def

trivialTwoAffineOpenCover

L359 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.AlgebraicGeometry.Scheme.Modules.B1Glue.trivialTwoAffineOpenCover
Documentation

The two-affine-open cover of an affine scheme consisting of two copies of the whole scheme.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace B1Glue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · full declaration
def trivialTwoAffineOpenCover (Y : Scheme.{u}) [IsAffine Y] : Y.TwoAffineOpenCover
  where
  U0 := ⊤
  U1 := ⊤
  isAffineOpen_U0 := isAffineOpen_top Y
  isAffineOpen_U1 := isAffineOpen_top Y
  sup_eq_top := sup_idem _
  isAffineOpen_inf := by rw [inf_idem]; exact isAffineOpen_top Y
theorem

moduleInvertible_sections_top

L368 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.AlgebraicGeometry.Scheme.Modules.B1Glue.moduleInvertible_sections_top
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace B1Glue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem moduleInvertible_sections_top [IsAffine Y] {N : Y.Modules} (hN :
  Scheme.Modules.IsInvertible N) :
    Module.Invertible Γ(Y, ⊤) Γ(N, ⊤)
theorem

exists_mem_opens_nonempty_pullback_preimage_iso_tensorUnit_of_isFinite

L378 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.AlgebraicGeometry.Scheme.Modules.B1Glue.exists_mem_opens_nonempty_pullback_preimage_iso_tensorUnit_of_isFinite
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace InvertibleFinitePreimage
universe u
open TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
namespace B1Glue
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem exists_mem_opens_nonempty_pullback_preimage_iso_tensorUnit_of_isFinite (hALG :
  ALGStatement.{u})
    {Z T : Scheme.{u}} (q : Z ⟶ T) [IsFinite q] {N : Z.Modules} (hN : Scheme.Modules.IsInvertible
      N) (t : T) :
    ∃ W : T.Opens, t ∈ W ∧
      Nonempty ((Scheme.Modules.pullback (q ⁻¹ᵁ W).ι).obj N ≅ 𝟙_ (↑(q ⁻¹ᵁ W) : Scheme.{u}).Modules)
theorem

exists_nonempty_pullback_preimage_iso_tensorUnit_of_isFinite

L455 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.exists_nonempty_pullback_preimage_iso_tensorUnit_of_isFinite
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicGeometry.Scheme.Modules.IsInvertible
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage
universe u
open _root_.TensorProduct
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
open _root_.TopologicalSpace
open _root_.Opposite
open _root_.CategoryTheory _root_.CategoryTheory.Limits _root_.AlgebraicGeometry
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleFinitePreimage.AlgebraicGeometry
  _root_.CategoryTheory.MonoidalCategory in
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs in
open InvertibleFinitePreimage.AlgebraicGeometry.Scheme.Modules in
Lean source · statement
theorem exists_nonempty_pullback_preimage_iso_tensorUnit_of_isFinite
    {Z T : Scheme.{u}} (q : Z ⟶ T) [IsFinite q] {N : Z.Modules} (hN : Scheme.Modules.IsInvertible
      N) (t : T) :
    ∃ W : T.Opens, t ∈ W ∧
      Nonempty ((Scheme.Modules.pullback (q ⁻¹ᵁ W).ι).obj N ≅ 𝟙_ (↑(q ⁻¹ᵁ W) : Scheme.{u}).Modules)

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