NYLL
Module

OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
19 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf is Coherent is Quasicoherent supported In pushforward Unit

Imports1
Imported by5

Declarations

theorem

preimage_eq_bot

L36 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.preimage_eq_bot
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem preimage_eq_bot (U : V.Opens) (hU : (U : Set V) ∩ Set.range ι.base = ∅) : ι ⁻¹ᵁ U = ⊥
theorem

subsingleton_sections_of_eq_bot

L45 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.subsingleton_sections_of_eq_bot
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
Lean source · statement
theorem subsingleton_sections_of_eq_bot (W : Z.Opens) (h : W = ⊥) : Subsingleton Γ(Z, W)
def

image

L50 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.image
Documentation

The closed image of the given closed immersion.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
Lean source · statement
def image : Closeds V
theorem

coe_image

L52 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.coe_image
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
Lean source · statement
theorem coe_image : (image ι : Set V) = Set.range ι.base
theorem

supportedIn

L54 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.supportedIn
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
Lean source · statement
theorem supportedIn : (pushforwardUnit π ι).SupportedIn (image ι)
theorem

res_rfl

L57 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.res_rfl
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
Lean source · statement
theorem res_rfl (W : Z.Opens) (x : Γ(Z, W)) : Z.presheaf.map (homOfLE (le_refl W)).op x = x
theorem

appLE_rfl_apply

L61 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.appLE_rfl_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem appLE_rfl_apply (U : V.Opens) (a : Γ(V, U)) : ι.appLE U (ι ⁻¹ᵁ U) le_rfl a = ι.app U a
def

actHom

L67 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.actHom
Documentation

The section map of the closed immersion viewed as a linear map to the pushforward of its structure sheaf.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
Lean source · full declaration
def actHom (U : V.affineOpens) : Γ(V, U.1) →ₗ[Γ(V, U.1)] (pushforwardUnit π ι).obj
  U.1 where
  toFun a := show Γ(Z, ι ⁻¹ᵁ U.1) from ι.appLE U.1 (ι ⁻¹ᵁ U.1) le_rfl a
  map_add' a b := map_add _ a b
  map_smul' a b := by
    change ι.appLE U.1 (ι ⁻¹ᵁ U.1) le_rfl (a * b) = ι.appLE U.1 (ι ⁻¹ᵁ U.1) le_rfl a * ι.appLE U.1
      (ι ⁻¹ᵁ U.1) le_rfl b
    exact map_mul _ a b
theorem

actHom_surjective

L76 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.actHom_surjective
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
Lean source · statement
theorem actHom_surjective (U : V.affineOpens) : Function.Surjective (actHom π ι U)
theorem

isCoherent

L81 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.isCoherent
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
Lean source · statement
theorem isCoherent : (pushforwardUnit π ι).IsCoherent
theorem

loc_core

L84 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.loc_core
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
Lean source · statement
theorem loc_core (U : V.affineOpens) (g : Γ(Z, ι ⁻¹ᵁ U.1)) (W' : Z.Opens) (hle : W' ≤ ι ⁻¹ᵁ U.1)
    (hW' : W' = Z.basicOpen g) :
    (∀ x : Γ(Z, W'), ∃ (n : ℕ) (y : Γ(Z, ι ⁻¹ᵁ U.1)),
        Z.presheaf.map (homOfLE hle).op y = Z.presheaf.map (homOfLE hle).op (g ^ n) * x) ∧
      (∀ y : Γ(Z, ι ⁻¹ᵁ U.1), Z.presheaf.map (homOfLE hle).op y = 0 → ∃ n : ℕ, g ^ n * y = 0)
theorem

preimage_basicOpen_eq

L107 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.preimage_basicOpen_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem preimage_basicOpen_eq (U : V.affineOpens) (f : Γ(V, U.1)) :
    ι ⁻¹ᵁ V.basicOpen f = Z.basicOpen (ι.appLE U.1 (ι ⁻¹ᵁ U.1) le_rfl f)
theorem

pre_le

L112 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.pre_le
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · statement
theorem pre_le (U : V.affineOpens) (f : Γ(V, U.1)) : ι ⁻¹ᵁ V.basicOpen f ≤ ι ⁻¹ᵁ U.1
theorem

smul_basicOpen

L116 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.smul_basicOpen
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · full declaration
theorem smul_basicOpen (U : V.affineOpens) (f : Γ(V, U.1)) (a : Γ(V, U.1)) (x : Γ(Z, ι ⁻¹ᵁ
  V.basicOpen f)) :
    ((V.presheaf.map (homOfLE (V.basicOpen_le f)).op).hom a •
        (show (pushforwardUnit π ι).obj (V.basicOpen f) from x)) =
      (show (pushforwardUnit π ι).obj (V.basicOpen f) from
        Z.presheaf.map (homOfLE (pre_le ι U f)).op (ι.appLE U.1 (ι ⁻¹ᵁ U.1) le_rfl a) * x) := by
  change ι.appLE (V.basicOpen f) (ι ⁻¹ᵁ V.basicOpen f) le_rfl ((V.presheaf.map (homOfLE
    (V.basicOpen_le f)).op) a) * x
    = _
  congr 1
  rw [← CommRingCat.comp_apply, ← CommRingCat.comp_apply, Scheme.Hom.map_appLE,
    Scheme.Hom.appLE_map]
theorem

smul_top

L130 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.smul_top
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · full declaration
theorem smul_top (U : V.affineOpens) (a : Γ(V, U.1)) (y : Γ(Z, ι ⁻¹ᵁ U.1)) :
    (a • (show (pushforwardUnit π ι).obj U.1 from y)) =
      (show (pushforwardUnit π ι).obj U.1 from ι.appLE U.1 (ι ⁻¹ᵁ U.1) le_rfl a * y) := rfl
theorem

res_eq

L135 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.res_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
omit [IsClosedImmersion ι] in
Lean source · full declaration
theorem res_eq (U : V.affineOpens) (f : Γ(V, U.1)) (y : Γ(Z, ι ⁻¹ᵁ U.1)) :
    (pushforwardUnit π ι).res (V.basicOpen_le f) (show (pushforwardUnit π ι).obj U.1 from y) =
      (show (pushforwardUnit π ι).obj (V.basicOpen f) from Z.presheaf.map (homOfLE (pre_le ι U
        f)).op y) := by
  change Z.presheaf.map _ y = _
  rw [Subsingleton.elim (homOfLE ((Opens.map ι.base).monotone (V.basicOpen_le f))) (homOfLE (pre_le
    ι U f))]
theorem

isQuasicoherent

L143 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.isQuasicoherent
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
Lean source · statement
theorem isQuasicoherent : (pushforwardUnit π ι).IsQuasicoherent
theorem

main

L167 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit.P2mPushUnit.main
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
namespace P2mPushUnit
open AlgebraicGeometry.OModulePresheaf
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
  [IsClosedImmersion ι]
Lean source · statement
theorem main :
    (pushforwardUnit π ι).IsCoherent ∧ (pushforwardUnit π ι).IsQuasicoherent ∧
      (pushforwardUnit π ι).SupportedIn ⟨Set.range ι.base, ι.isClosedEmbedding.isClosed_range⟩
theorem

isCoherent_isQuasicoherent_supportedIn_pushforwardUnit

L174 ↗
AlgebraicGeometry.OModulePresheaf.isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite
Lean source · statement
theorem
  _root_.AlgebraicGeometry.OModulePresheaf.isCoherent_isQuasicoherent_supportedIn_pushforwardUnit
    {R : Type u} [CommRing R] {V Z : Scheme.{u}} (π : V ⟶ Spec (.of R)) (ι : Z ⟶ V)
      [IsClosedImmersion ι] :
    (OModulePresheaf.pushforwardUnit π ι).IsCoherent ∧ (OModulePresheaf.pushforwardUnit π
      ι).IsQuasicoherent ∧
      (OModulePresheaf.pushforwardUnit π ι).SupportedIn ⟨Set.range ι.base,
        ι.isClosedEmbedding.isClosed_range⟩

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