Module

Scheme_Modules_exists_basis_pullback_of_field_point.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_basis_pullback_of_field_point

41 declarations indexed from sourceView source ↗

Module documentation

Bases after pullback to a field-valued point

Local bases of a module give bases after pullback along a point valued in a field.

Imports1

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullback_locally_mem_span_unit

Imported by2

abbrev

res

L35 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.res

Documentation

Restrict a module section to a smaller open subset.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint

Lean source · statement

abbrev res {Z : Scheme.{u}} (M : Z.Modules) {W' W : Z.Opens} (h : W' ≤ W) (s : Γ(M,
  W)) :
    Γ(M, W')

lemma

res_res

L40 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.res_res

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint

Lean source · statement

lemma res_res {Z : Scheme.{u}} (M : Z.Modules) {W₁ W₂ W₃ : Z.Opens} (h₂₁ : W₂ ≤ W₁) (h₃₂ : W₃ ≤ W₂)
    (s : Γ(M, W₁)) : res M h₃₂ (res M h₂₁ s) = res M (h₃₂.trans h₂₁) s

lemma

res_self

L46 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.res_self

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint

Lean source · statement

lemma res_self {Z : Scheme.{u}} (M : Z.Modules) {W : Z.Opens} (h : W ≤ W) (s : Γ(M, W)) : res M h
  s = s

lemma

res_eq_map

L52 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.res_eq_map

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint

Lean source · statement

lemma res_eq_map {Z : Scheme.{u}} (M : Z.Modules) {W' W : Z.Opens} (f : W' ⟶ W) (s : Γ(M, W)) :
    M.presheaf.map f.op s = res M f.le s

lemma

res_smul

L56 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.res_smul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint

Lean source · statement

lemma res_smul {Z : Scheme.{u}} (M : Z.Modules) {W' W : Z.Opens} (h : W' ≤ W) (r : Γ(Z, W)) (s :
  Γ(M, W)) :
    res M h (r • s) = Z.presheaf.map (homOfLE h).op r • res M h s

lemma

res_add

L61 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.res_add

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint

Lean source · statement

lemma res_add {Z : Scheme.{u}} (M : Z.Modules) {W' W : Z.Opens} (h : W' ≤ W) (s t : Γ(M, W)) :
    res M h (s + t) = res M h s + res M h t

lemma

res_sum

L64 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.res_sum

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint

Lean source · statement

lemma res_sum {Z : Scheme.{u}} (M : Z.Modules) {W' W : Z.Opens} (h : W' ≤ W) {ι : Type*} (T :
  Finset ι)
    (s : ι → Γ(M, W)) : res M h (∑ t ∈ T, s t) = ∑ t ∈ T, res M h (s t)

lemma

str_map_map

L68 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.str_map_map

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint

Lean source · statement

lemma str_map_map {Z : Scheme.{u}} {A B C : Z.Opens} (h₁ : B ≤ A) (h₂ : C ≤ B) (h₃ : C ≤ A) (r :
  Γ(Z, A)) :
    Z.presheaf.map (homOfLE h₂).op (Z.presheaf.map (homOfLE h₁).op r) = Z.presheaf.map (homOfLE
      h₃).op r

lemma

str_map_self

L76 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.str_map_self

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint

Lean source · statement

lemma str_map_self {Z : Scheme.{u}} {A : Z.Opens} (h : A ≤ A) (r : Γ(Z, A)) :
    Z.presheaf.map (homOfLE h).op r = r

def

bas

L86 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.bas

Documentation

Choose the stipulated basis on a smaller open subset.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))

Lean source · statement

def bas (W : X.Opens) (hW : W ≤ U) : Module.Basis (Fin n) Γ(X, W) Γ(M, W)

lemma

bas_apply

L89 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.bas_apply

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))

Lean source · statement

lemma bas_apply (W : X.Opens) (hW : W ≤ U) (i : Fin n) : bas e he W hW i = res M hW (e i)

lemma

repr_res

L92 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.repr_res

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))

Lean source · statement

lemma repr_res {W W' : X.Opens} (hW : W ≤ U) (h : W' ≤ W) (m : Γ(M, W)) (j : Fin n) :
    (bas e he W' (h.trans hW)).repr (res M h m) j =
      X.presheaf.map (homOfLE h).op ((bas e he W hW).repr m j)

lemma

pt_eq

L107 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.pt_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

lemma pt_eq (q : Spec (CommRingCat.of K)) : q = IsLocalRing.closedPoint K

lemma

preimage_le

L111 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.preimage_le

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
include hs in

Lean source · statement

lemma preimage_le (W : X.Opens) : s ⁻¹ᵁ W ≤ s ⁻¹ᵁ (W ⊓ U)

lemma

le_of_mem

L116 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.le_of_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

lemma le_of_mem {W₁ W₂ : (Spec (CommRingCat.of K)).Opens} (h : IsLocalRing.closedPoint K ∈ W₂) :
  W₁ ≤ W₂

abbrev

N

L123 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.N

Documentation

The module pulled back to the field-valued point.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

abbrev N : (Spec (CommRingCat.of K)).Modules

def

eta

L126 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.eta

Documentation

Map a section to the pullback using the adjunction unit.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

def eta (V : X.Opens) (m : Γ(M, V)) : Γ(N s (M := M), s ⁻¹ᵁ V)

lemma

eta_add

L129 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.eta_add

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

lemma eta_add (V : X.Opens) (m m' : Γ(M, V)) : eta s V (m + m') = eta s V m + eta s V m'

lemma

eta_sum

L132 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.eta_sum

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

lemma eta_sum (V : X.Opens) {ι : Type*} (T : Finset ι) (f : ι → Γ(M, V)) :
    eta s V (∑ t ∈ T, f t) = ∑ t ∈ T, eta s V (f t)

lemma

eta_smul

L136 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.eta_smul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

lemma eta_smul (V : X.Opens) (r : Γ(X, V)) (m : Γ(M, V)) :
    eta s V (r • m) = s.app V r • eta s V m

lemma

res_eta

L140 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.res_eta

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

lemma res_eta {V V' : X.Opens} (h : V' ≤ V) (m : Γ(M, V)) :
    res (N s (M := M)) (s.preimage_mono h) (eta s V m) = eta s V' (res M h m)

lemma

span_eta_eq_top

L150 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.span_eta_eq_top

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
include he hs in

Lean source · full declaration

lemma span_eta_eq_top :
    ⊤ ≤ Submodule.span ((Spec (CommRingCat.of K)).presheaf.obj (op (s ⁻¹ᵁ U))) (Set.range fun k :
      Fin n => eta s U (e k)) := by
  intro y _
  obtain ⟨U', W', i, j, hU'U, hxW', hmem⟩ :=
    Scheme.Modules.pullback_locally_mem_span_unit s M (W := s ⁻¹ᵁ U) y (x :=
      IsLocalRing.closedPoint K) hs
      (U₀ := U) hs
  obtain rfl : W' = s ⁻¹ᵁ U := le_antisymm i (le_of_mem hxW')
  rw [show ((Scheme.Modules.pullback s).obj M).presheaf.map (homOfLE i).op y = y from res_self _
    i y] at hmem
  refine (Submodule.span_le.mpr ?_) hmem
  rintro _ ⟨m, rfl⟩
  have hm : m = ∑ k, (bas e he U' hU'U).repr m k • res M hU'U (e k) := by
    conv_lhs => rw [← (bas e he U' hU'U).sum_repr m]
    simp only [bas_apply]
  change res (N s (M := M)) j (eta s U' m) ∈ _
  rw [hm, eta_sum, res_sum]
  refine Submodule.sum_mem _ fun k _ => ?_
  rw [eta_smul, res_smul, ← res_eta, res_res, res_self]
  exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨k, rfl⟩)

abbrev

P

L173 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.P

Documentation

Push the unit module on the field-valued point forward to the scheme.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

abbrev P : X.Modules

def

kapFun

L177 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.kapFun

Documentation

Take a basis coordinate after restricting a section near the field-valued point.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

def kapFun (j : Fin n) (W : X.Opens) (m : Γ(M, W)) : Γ(Spec (CommRingCat.of K), s
  ⁻¹ᵁ W)

lemma

kapFun_add

L182 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.kapFun_add

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

lemma kapFun_add (j : Fin n) (W : X.Opens) (m m' : Γ(M, W)) :
    kapFun e he s hs j W (m + m') = kapFun e he s hs j W m + kapFun e he s hs j W m'

lemma

kapFun_smul

L186 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.kapFun_smul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

lemma kapFun_smul (j : Fin n) (W : X.Opens) (r : Γ(X, W)) (m : Γ(M, W)) :
    kapFun e he s hs j W (r • m) = s.app W r * kapFun e he s hs j W m

lemma

kapFun_res

L197 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.kapFun_res

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

lemma kapFun_res (j : Fin n) {W W' : X.Opens} (h : W' ≤ W) (m : Γ(M, W)) :
    kapFun e he s hs j W' (res M h m) =
      (Spec (CommRingCat.of K)).presheaf.map (homOfLE (s.preimage_mono h)).op (kapFun e he s hs j
        W m)

def

toP

L215 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.toP

Documentation

View a structure sheaf section as a section of the pushed-forward unit module.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

def toP (W : X.Opens) (t : Γ(Spec (CommRingCat.of K), s ⁻¹ᵁ W)) : Γ(P s, W)

lemma

toP_add

L217 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.toP_add

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

lemma toP_add (W : X.Opens) (t t' : Γ(Spec (CommRingCat.of K), s ⁻¹ᵁ W)) :
    toP s W (t + t') = toP s W t + toP s W t'

lemma

smul_toP

L220 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.smul_toP

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

lemma smul_toP (W : X.Opens) (r : Γ(X, W)) (t : Γ(Spec (CommRingCat.of K), s ⁻¹ᵁ W)) :
    r • toP s W t = toP s W (s.app W r * t)

lemma

map_toP

L223 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.map_toP

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

lemma map_toP {W W' : X.Opens} (i : W' ⟶ W) (t : Γ(Spec (CommRingCat.of K), s ⁻¹ᵁ W)) :
    (P s).presheaf.map i.op (toP s W t) =
      toP s W' ((Spec (CommRingCat.of K)).presheaf.map ((Opens.map s.base).map i).op t)

def

kapAb

L228 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.kapAb

Documentation

The natural map of abelian presheaves given by a basis coordinate.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · full declaration

def kapAb (j : Fin n) : M.presheaf ⟶ (P s).presheaf where
  app W := AddCommGrpCat.ofHom (X := Γ(M, W.unop)) (Y := Γ(P s, W.unop))
    { toFun := fun m => toP s W.unop (kapFun e he s hs j W.unop m)
      map_zero' := by
        have h := kapFun_add e he s hs j W.unop 0 0
        rw [add_zero] at h
        rw [show kapFun e he s hs j W.unop 0 = 0 from left_eq_add.mp h]
        rfl
      map_add' := fun m m' => by rw [kapFun_add]; rfl }
  naturality W W' g := by
    ext m
    obtain ⟨g, rfl⟩ : ∃ g' : W'.unop ⟶ W.unop, g = g'.op := ⟨g.unop, rfl⟩
    change toP s W'.unop (kapFun e he s hs j W'.unop (M.presheaf.map g.op m)) =
      (P s).presheaf.map g.op (toP s W.unop (kapFun e he s hs j W.unop m))
    rw [res_eq_map, kapFun_res, map_toP,
      Subsingleton.elim ((Opens.map s.base).map g) (homOfLE (s.preimage_mono g.le))]

def

kap

L246 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.kap

Documentation

The module sheaf morphism given by a basis coordinate.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

def kap (j : Fin n) : M ⟶ P s

lemma

kap_app

L251 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.kap_app

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

lemma kap_app (j : Fin n) (W : X.Opens) (m : Γ(M, W)) :
    (kap e he s hs j).app W m = toP s W (kapFun e he s hs j W m)

def

kapSharp

L255 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.kapSharp

Documentation

The adjoint basis-coordinate morphism on the pullback module.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

def kapSharp (j : Fin n) :
    Scheme.Modules.Hom (X := Spec (CommRingCat.of K)) (N s (M := M))
      (SheafOfModules.unit (Spec (CommRingCat.of K)).ringCatSheaf :
        (Spec (CommRingCat.of K)).Modules)

lemma

kapSharp_eta

L261 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.kapSharp_eta

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

lemma kapSharp_eta (j : Fin n) (V : X.Opens) (m : Γ(M, V)) :
    (kapSharp e he s hs j).app (s ⁻¹ᵁ V) (eta s V m) = (kap e he s hs j).app V m

lemma

kapFun_e

L276 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.kapFun_e

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · full declaration

lemma kapFun_e (j i : Fin n) :
    kapFun e he s hs j U (e i) = if i = j then 1 else 0 := by
  simp only [kapFun]
  rw [← bas_apply e he, Module.Basis.repr_self, Finsupp.single_apply]
  split_ifs <;> simp only [map_one, map_zero]

lemma

linearIndependent_eta

L283 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.linearIndependent_eta

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
include he hs in

Lean source · full declaration

lemma linearIndependent_eta :
    LinearIndependent ((Spec (CommRingCat.of K)).presheaf.obj (op (s ⁻¹ᵁ U))) (fun k : Fin n =>
      eta s U (e k)) := by
  rw [Fintype.linearIndependent_iff]
  intro c hc j
  let q : Γ(N s (M := M), s ⁻¹ᵁ U) →ₗ[Γ(Spec (CommRingCat.of K), s ⁻¹ᵁ U)]
      Γ(Spec (CommRingCat.of K), s ⁻¹ᵁ U) :=
    ((kapSharp e he s hs j).val.app (op (s ⁻¹ᵁ U))).hom
  have hcoeff (i : Fin n) : q (eta s U (e i)) = if i = j then 1 else 0 :=
    (kapSharp_eta e he s hs j U (e i)).trans
      ((kap_app e he s hs j U (e i)).trans
        (congrArg (toP s U) (kapFun_e e he s hs j i)))
  have hsum : (∑ i, c i * (if i = j then 1 else 0)) = 0 := by
    calc
      _ = ∑ i, q (c i • eta s U (e i)) := by
        apply Finset.sum_congr rfl
        intro i _
        exact ((q.map_smul (c i) (eta s U (e i))).trans
          (congrArg (fun z : Γ(Spec (CommRingCat.of K), s ⁻¹ᵁ U) => c i • z)
            (hcoeff i))).symm
      _ = q (∑ i, c i • eta s U (e i)) := (map_sum q _ Finset.univ).symm
      _ = q 0 := congrArg q hc
      _ = 0 := map_zero q
  have hsum_eq : (∑ i, c i * (if i = j then 1 else 0)) = c j := by
    rw [Finset.sum_eq_single j]
    · rw [ite_eq_left rfl, mul_one]
    · intro i _ hij
      rw [ite_eq_right hij, mul_zero]
    · intro hj
      exact (hj (Finset.mem_univ j)).elim
  exact hsum_eq.symm.trans hsum

def

basisEta

L316 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.basisEta

Documentation

The basis formed by the images of the local basis under the adjunction unit.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

def basisEta :
    Module.Basis (Fin n) ((Spec (CommRingCat.of K)).presheaf.obj (op (s ⁻¹ᵁ U))) Γ(N s (M := M),
      s ⁻¹ᵁ U)

lemma

basisEta_apply

L321 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_basis_pullback_of_field_point.Ws14DG.FieldPoint.basisEta_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace Ws14DG
namespace FieldPoint
variable {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
    ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
variable {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)

Lean source · statement

lemma basisEta_apply (i : Fin n) : basisEta e he s hs i = eta s U (e i)

theorem

exists_basis_pullback_of_field_point

L328 ↗

AlgebraicGeometry.Scheme.Modules.exists_basis_pullback_of_field_point

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_basis_pullback_of_field_point
universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.exists_basis_pullback_of_field_point
    {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {U : X.Opens} (e : Fin n → Γ(M, U))
    (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
      ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i))
    {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X)
    (hs : s.base (IsLocalRing.closedPoint K) ∈ U) :
    ∃ b : Module.Basis (Fin n) Γ(Spec (CommRingCat.of K), s ⁻¹ᵁ U)
        Γ((Scheme.Modules.pullback s).obj M, s ⁻¹ᵁ U),
      ∀ i, b i = ((Scheme.Modules.pullbackPushforwardAdjunction s).unit.app M).app U (e i)

Module documentation

Bases after pullback to a field-valued point

Declarations