Module

AffineSectionsBaseChange.lean

Nyll.SchemeTheory.Modules.AffineSectionsBaseChange

87 declarations indexed from sourceView source ↗

Module documentation

Extended sections of an invertible module and pullback

For an affine open with affine inverse image, extending sections of an invertible module gives the sections of its pullback, with the prescribed unit formula.

Imports6

Mathlib.RingTheory.LocalProperties.Exactness
Nyll.SchemeTheory.Modules.Invertible
Nyll.SchemeTheory.Modules.Frames
Nyll.SchemeTheory.Modules.FrameFromTrivialization
Nyll.SchemeTheory.Modules.LocallyTrivialSectionsLocalization
Mathlib.Util.WithWeakNamespace

Imported by7

theorem

map_map

L44 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.map_map

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Res
variable {X : Scheme.{u}} (M : X.Modules)

Lean source · statement

theorem map_map {W₁ W₂ W₃ : X.Opens} (i : W₁ ⟶ W₂) (j : W₂ ⟶ W₃) (k : W₁ ⟶ W₃) (y : Γ(M, W₃)) :
    M.presheaf.map i.op (M.presheaf.map j.op y) = M.presheaf.map k.op y

theorem

map_self

L48 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.map_self

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Res
variable {X : Scheme.{u}} (M : X.Modules)

Lean source · statement

theorem map_self {W : X.Opens} (i : W ⟶ W) (y : Γ(M, W)) : M.presheaf.map i.op y = y

theorem

fmap_map

L51 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.fmap_map

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Res
variable {X : Scheme.{u}} (M : X.Modules)

Lean source · statement

theorem fmap_map {W₁ W₂ W₃ : X.Opens} (i : W₁ ⟶ W₂) (j : W₂ ⟶ W₃) (k : W₁ ⟶ W₃) (g : Γ(X, W₃)) :
    X.presheaf.map i.op (X.presheaf.map j.op g) = X.presheaf.map k.op g

theorem

fmap_self

L55 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.fmap_self

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Res
variable {X : Scheme.{u}} (M : X.Modules)

Lean source · statement

theorem fmap_self {W : X.Opens} (i : W ⟶ W) (g : Γ(X, W)) : X.presheaf.map i.op g = g

theorem

bijective_map_of_eq

L58 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.bijective_map_of_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_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Res
variable {X : Scheme.{u}} (M : X.Modules)

Lean source · statement

theorem bijective_map_of_eq {W₁ W₂ : X.Opens} (h : W₁ = W₂) (i : W₁ ⟶ W₂) :
    Function.Bijective (M.presheaf.map i.op)

theorem

app_map

L64 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.app_map

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Res
variable {X : Scheme.{u}} (M : X.Modules)

Lean source · statement

theorem app_map {N : X.Modules} (φ : M ⟶ N) {W₁ W₂ : X.Opens} (i : W₁ ⟶ W₂) (x : Γ(M, W₂)) :
    φ.app W₁ (M.presheaf.map i.op x) = N.presheaf.map i.op (φ.app W₂ x)

theorem

eval_injective

L74 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.eval_injective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}

Lean source · full declaration

theorem eval_injective (hs : Scheme.Modules.IsFrameOn s V)
    (hP : ∀ W : X.Opens, Function.Injective (P.presheaf.map (homOfLE (inf_le_left : W ⊓ V ≤ W)).op))
        :
    Function.Injective fun f : L ⟶ P => f.app V s := by
  suffices h0 : ∀ f : L ⟶ P, f.app V s = 0 → f = 0 by
    intro f₁ f₂ h
    have := h0 (f₁ - f₂) (by
      rw [Scheme.Modules.Hom.sub_app]
      exact sub_eq_zero.mpr h)
    exact sub_eq_zero.mp this
  intro f hf
  apply Scheme.Modules.hom_ext
  intro W
  ext x
  change f.app W x = 0
  apply hP W
  rw [map_zero, ← app_map]
  obtain ⟨g, hg⟩ := (hs.bijective (inf_le_right : W ⊓ V ≤ V) inf_le_right).2
    (L.presheaf.map (homOfLE (inf_le_left : W ⊓ V ≤ W)).op x)
  rw [← hg, Scheme.Modules.Hom.app_smul, app_map, hf, map_zero, smul_zero]

def

liftFun

L97 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.liftFun

Documentation

Extend a section from the framing open using the given bijective restriction maps.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}
variable (P s) in

Lean source · statement

def liftFun (hs : Scheme.Modules.IsFrameOn s V)
    (hP : ∀ W : X.Opens, Function.Bijective (P.presheaf.map (homOfLE (inf_le_left : W ⊓ V ≤ W)).op))
    (y : Γ(P, V)) (W : X.Opens) (x : Γ(L, W)) : Γ(P, W)

def

coef

L106 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.coef

Documentation

The coefficient of a section in the chosen frame on its overlap with the framing open.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}
variable (P s) in

Lean source · statement

def coef (hs : Scheme.Modules.IsFrameOn s V) (W : X.Opens) (x : Γ(L, W)) : Γ(X, W ⊓ V)

theorem

coef_spec

L110 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.coef_spec

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}
variable (P s) in

Lean source · statement

theorem coef_spec (hs : Scheme.Modules.IsFrameOn s V) (W : X.Opens) (x : Γ(L, W)) :
    coef hs W x • L.presheaf.map (homOfLE (inf_le_right : W ⊓ V ≤ V)).op s =
      L.presheaf.map (homOfLE (inf_le_left : W ⊓ V ≤ W)).op x

theorem

coef_unique

L115 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.coef_unique

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}
variable (P s) in

Lean source · statement

theorem coef_unique (hs : Scheme.Modules.IsFrameOn s V) (W : X.Opens) (x : Γ(L, W)) (g : Γ(X, W ⊓
  V))
    (hg : g • L.presheaf.map (homOfLE (inf_le_right : W ⊓ V ≤ V)).op s =
      L.presheaf.map (homOfLE (inf_le_left : W ⊓ V ≤ W)).op x) :
    g = coef hs W x

theorem

coef_add

L122 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.coef_add

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}
variable (P s) in

Lean source · statement

theorem coef_add (hs : Scheme.Modules.IsFrameOn s V) (W : X.Opens) (x₁ x₂ : Γ(L, W)) :
    coef hs W (x₁ + x₂) = coef hs W x₁ + coef hs W x₂

theorem

coef_smul

L127 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.coef_smul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}
variable (P s) in

Lean source · statement

theorem coef_smul (hs : Scheme.Modules.IsFrameOn s V) (W : X.Opens) (a : Γ(X, W)) (x : Γ(L, W)) :
    coef hs W (a • x) = X.presheaf.map (homOfLE (inf_le_left : W ⊓ V ≤ W)).op a * coef hs W x

theorem

map_coef

L132 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.map_coef

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}
variable (P s) in

Lean source · statement

theorem map_coef (hs : Scheme.Modules.IsFrameOn s V) {W₁ W₂ : X.Opens} (i : W₁ ⟶ W₂) (x : Γ(L, W₂))
  :
    X.presheaf.map (homOfLE (inf_le_inf_right V i.le : W₁ ⊓ V ≤ W₂ ⊓ V)).op (coef hs W₂ x) =
      coef hs W₁ (L.presheaf.map i.op x)

theorem

liftFun_spec

L143 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.liftFun_spec

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}
variable (P s) in

Lean source · statement

theorem liftFun_spec (hs : Scheme.Modules.IsFrameOn s V)
    (hP : ∀ W : X.Opens, Function.Bijective (P.presheaf.map (homOfLE (inf_le_left : W ⊓ V ≤ W)).op))
    (y : Γ(P, V)) (W : X.Opens) (x : Γ(L, W)) :
    P.presheaf.map (homOfLE (inf_le_left : W ⊓ V ≤ W)).op (liftFun P s hs hP y W x) =
      coef hs W x • P.presheaf.map (homOfLE (inf_le_right : W ⊓ V ≤ V)).op y

theorem

liftFun_add

L150 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.liftFun_add

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}
variable (P s) in

Lean source · statement

theorem liftFun_add (hs : Scheme.Modules.IsFrameOn s V)
    (hP : ∀ W : X.Opens, Function.Bijective (P.presheaf.map (homOfLE (inf_le_left : W ⊓ V ≤ W)).op))
    (y : Γ(P, V)) (W : X.Opens) (x₁ x₂ : Γ(L, W)) :
    liftFun P s hs hP y W (x₁ + x₂) = liftFun P s hs hP y W x₁ + liftFun P s hs hP y W x₂

theorem

liftFun_smul

L157 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.liftFun_smul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}
variable (P s) in

Lean source · statement

theorem liftFun_smul (hs : Scheme.Modules.IsFrameOn s V)
    (hP : ∀ W : X.Opens, Function.Bijective (P.presheaf.map (homOfLE (inf_le_left : W ⊓ V ≤ W)).op))
    (y : Γ(P, V)) (W : X.Opens) (a : Γ(X, W)) (x : Γ(L, W)) :
    liftFun P s hs hP y W (a • x) = a • liftFun P s hs hP y W x

theorem

liftFun_map

L164 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.liftFun_map

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}
variable (P s) in

Lean source · statement

theorem liftFun_map (hs : Scheme.Modules.IsFrameOn s V)
    (hP : ∀ W : X.Opens, Function.Bijective (P.presheaf.map (homOfLE (inf_le_left : W ⊓ V ≤ W)).op))
    (y : Γ(P, V)) {W₁ W₂ : X.Opens} (i : W₁ ⟶ W₂) (x : Γ(L, W₂)) :
    liftFun P s hs hP y W₁ (L.presheaf.map i.op x) = P.presheaf.map i.op (liftFun P s hs hP y W₂ x)

def

lift

L176 ↗

P2mPullbackSectionsSol.lift

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}
variable (P s) in
variable (P s) in

Lean source · statement

def _root_.P2mPullbackSectionsSol.lift (hs : Scheme.Modules.IsFrameOn s V)
    (hP : ∀ W : X.Opens, Function.Bijective (P.presheaf.map (homOfLE (inf_le_left : W ⊓ V ≤ W)).op))
    (y : Γ(P, V)) : L ⟶ P

theorem

lift_app

L188 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.lift_app

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}
variable (P s) in
variable (P s) in
open _root_.P2mPullbackSectionsSol

Lean source · statement

theorem lift_app (hs : Scheme.Modules.IsFrameOn s V)
    (hP : ∀ W : X.Opens, Function.Bijective (P.presheaf.map (homOfLE (inf_le_left : W ⊓ V ≤ W)).op))
    (y : Γ(P, V)) (W : X.Opens) (x : Γ(L, W)) :
    (lift P s hs hP y).app W x = liftFun P s hs hP y W x

theorem

lift_app_self

L193 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.lift_app_self

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}
variable (P s) in
variable (P s) in
open _root_.P2mPullbackSectionsSol

Lean source · statement

theorem lift_app_self (hs : Scheme.Modules.IsFrameOn s V)
    (hP : ∀ W : X.Opens, Function.Bijective (P.presheaf.map (homOfLE (inf_le_left : W ⊓ V ≤ W)).op))
    (y : Γ(P, V)) : (lift P s hs hP y).app V s = y

theorem

eval_bijective

L202 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.eval_bijective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section EvalFrame
variable {X : Scheme.{u}} {L P : X.Modules} {V : X.Opens} {s : Γ(L, V)}
variable (P s) in
variable (P s) in
open _root_.P2mPullbackSectionsSol

Lean source · full declaration

theorem eval_bijective (hs : Scheme.Modules.IsFrameOn s V)
    (hP : ∀ W : X.Opens, Function.Bijective (P.presheaf.map (homOfLE (inf_le_left : W ⊓ V ≤ W)).op))
        :
    Function.Bijective fun f : L ⟶ P => f.app V s :=
  ⟨eval_injective hs fun W => (hP W).1, fun y => ⟨lift P s hs hP y, lift_app_self hs hP y⟩⟩

abbrev

pb

L215 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.pb

Documentation

The pullback of the invertible module along p.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)

Lean source · statement

abbrev pb : Z.Modules

abbrev

unitHom

L218 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.unitHom

Documentation

The unit morphism from the module to the pushforward of its pullback.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)

Lean source · statement

abbrev unitHom : L ⟶ (Scheme.Modules.pushforward p).obj (pb p L)

def

eta

L222 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.eta

Documentation

Pull a local section back using the unit of the pullback and pushforward adjunction.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)

Lean source · statement

def eta (V : X.Opens) (s : Γ(L, V)) : Γ(pb p L, p ⁻¹ᵁ V)

theorem

eta_add

L224 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.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_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)

Lean source · statement

theorem eta_add (V : X.Opens) (s₁ s₂ : Γ(L, V)) : eta p L V (s₁ + s₂) = eta p L V s₁ + eta p L V s₂

theorem

eta_smul

L228 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.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_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)

Lean source · statement

theorem eta_smul (V : X.Opens) (a : Γ(X, V)) (s : Γ(L, V)) : eta p L V (a • s) = p.app V a • eta p L
  V s

theorem

map_eta

L234 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.map_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_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)

Lean source · statement

theorem map_eta {V₁ V₂ : X.Opens} (i : V₁ ⟶ V₂) (k : p ⁻¹ᵁ V₁ ⟶ p ⁻¹ᵁ V₂) (s : Γ(L, V₂)) :
    (pb p L).presheaf.map k.op (eta p L V₂ s) = eta p L V₁ (L.presheaf.map i.op s)

theorem

evalPull_eq

L239 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.evalPull_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_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)

Lean source · statement

theorem evalPull_eq (Q : Z.Modules) (F : pb p L ⟶ Q) (V : X.Opens) (s : Γ(L, V)) :
    F.app (p ⁻¹ᵁ V) (eta p L V s) =
      ((Scheme.Modules.pullbackPushforwardAdjunction p).homEquiv L Q F).app V s

theorem

evalPull_bijective

L243 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.evalPull_bijective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)

Lean source · full declaration

theorem evalPull_bijective {V : X.Opens} {s : Γ(L, V)} (hs : Scheme.Modules.IsFrameOn s V) (Q :
  Z.Modules)
    (hQ : ∀ W : X.Opens, Function.Bijective
      (Q.presheaf.map ((Opens.map p.base).map (homOfLE (inf_le_left : W ⊓ V ≤ W))).op)) :
    Function.Bijective fun F : pb p L ⟶ Q => F.app (p ⁻¹ᵁ V) (eta p L V s) := by
  have h := eval_bijective (P := (Scheme.Modules.pushforward p).obj Q) hs hQ
  exact h.comp ((Scheme.Modules.pullbackPushforwardAdjunction p).homEquiv L Q).bijective

abbrev

OO

L254 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.OO

Documentation

The pushforward of the structure module of the open subscheme O.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)
variable (O : Z.Opens)

Lean source · statement

abbrev OO : Z.Modules

def

toFun'

L258 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.toFun'

Documentation

View sections of the pushed forward structure module as sections on the inverse image open.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)
variable (O : Z.Opens)

Lean source · statement

def toFun' (W : Z.Opens) (x : Γ(OO O, W)) : Γ((O : Scheme.{u}), O.ι ⁻¹ᵁ W)

def

ofFun'

L261 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.ofFun'

Documentation

View a section on the inverse image open as a section of the pushed forward structure module.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)
variable (O : Z.Opens)

Lean source · statement

def ofFun' (W : Z.Opens) (x : Γ((O : Scheme.{u}), O.ι ⁻¹ᵁ W)) : Γ(OO O, W)

theorem

toFun'_ofFun'

L263 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.toFun'_ofFun'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)
variable (O : Z.Opens)

Lean source · statement

theorem toFun'_ofFun' (W : Z.Opens) (x : Γ((O : Scheme.{u}), O.ι ⁻¹ᵁ W)) :
    toFun' O W (ofFun' O W x) = x

theorem

toFun'_injective

L266 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.toFun'_injective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)
variable (O : Z.Opens)

Lean source · statement

theorem toFun'_injective (W : Z.Opens) : Function.Injective (toFun' O W)

theorem

toFun'_smul

L268 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.toFun'_smul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)
variable (O : Z.Opens)

Lean source · statement

theorem toFun'_smul (W : Z.Opens) (g : Γ(Z, W)) (x : Γ(OO O, W)) :
    toFun' O W (g • x) = O.ι.app W g * toFun' O W x

theorem

toFun'_zero

L271 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.toFun'_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)
variable (O : Z.Opens)

Lean source · statement

theorem toFun'_zero (W : Z.Opens) : toFun' O W 0 = 0

theorem

toFun'_map

L273 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.toFun'_map

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)
variable (O : Z.Opens)

Lean source · statement

theorem toFun'_map {W₁ W₂ : Z.Opens} (i : W₁ ⟶ W₂) (x : Γ(OO O, W₂)) :
    toFun' O W₁ ((OO O).presheaf.map i.op x) =
      (O : Scheme.{u}).presheaf.map ((Opens.map O.ι.base).map i).op (toFun' O W₂ x)

theorem

OO_map_bijective

L277 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.OO_map_bijective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)
variable (O : Z.Opens)

Lean source · statement

theorem OO_map_bijective {W₁ W₂ : Z.Opens} (i : W₁ ⟶ W₂) (h : O.ι ⁻¹ᵁ W₁ = O.ι ⁻¹ᵁ W₂) :
    Function.Bijective ((OO O).presheaf.map i.op)

theorem

ιapp_injective

L282 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.ιapp_injective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)
variable (O : Z.Opens)

Lean source · statement

theorem ιapp_injective {W : Z.Opens} (hW : W ≤ O) : Function.Injective (O.ι.app W)

theorem

ιapp_bijective

L286 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.ιapp_bijective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)
variable (O : Z.Opens)

Lean source · statement

theorem ιapp_bijective : Function.Bijective (O.ι.app O)

theorem

ιapp_map

L290 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.ιapp_map

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)
variable (O : Z.Opens)

Lean source · statement

theorem ιapp_map {W₁ W₂ : Z.Opens} (i : W₁ ⟶ W₂) (g : Γ(Z, W₂)) :
    O.ι.app W₁ (Z.presheaf.map i.op g) =
      (O : Scheme.{u}).presheaf.map ((Opens.map O.ι.base).map i).op (O.ι.app W₂ g)

theorem

preimage_inf_eq

L296 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.preimage_inf_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)
variable (O : Z.Opens)

Lean source · statement

theorem preimage_inf_eq (V W : X.Opens) :
    (p ⁻¹ᵁ V).ι ⁻¹ᵁ (p ⁻¹ᵁ (W ⊓ V)) = (p ⁻¹ᵁ V).ι ⁻¹ᵁ (p ⁻¹ᵁ W)

theorem

bijective_smul_eta

L303 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.bijective_smul_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_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Pull
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules)
variable (O : Z.Opens)

Lean source · full declaration

theorem bijective_smul_eta {V : X.Opens} {s : Γ(L, V)} (hs : Scheme.Modules.IsFrameOn s V)
    (hN : Scheme.Modules.IsInvertible (pb p L)) :
    Function.Bijective fun g : Γ(Z, p ⁻¹ᵁ V) => g • eta p L V s := by
  set O : Z.Opens := p ⁻¹ᵁ V with hO
  set t : Γ(pb p L, O) := eta p L V s with ht
  have hQ : ∀ W : X.Opens, Function.Bijective
      ((OO O).presheaf.map ((Opens.map p.base).map (homOfLE (inf_le_left : W ⊓ V ≤ W))).op) :=
    fun W => OO_map_bijective O _ (preimage_inf_eq p V W)
  obtain ⟨F₁, hF₁⟩ := (evalPull_bijective p L hs (OO O) hQ).2 (ofFun' O O 1)
  have hF₁' : toFun' O O (F₁.app O t) = 1 := congrArg (toFun' O O) hF₁
  refine ⟨fun g₁ g₂ h => ?_, fun y => ?_⟩
  · have h' : F₁.app O (g₁ • t) = F₁.app O (g₂ • t) := congrArg (F₁.app O) h
    rw [Scheme.Modules.Hom.app_smul, Scheme.Modules.Hom.app_smul] at h'
    have h'' := congrArg (toFun' O O) h'
    rw [toFun'_smul, toFun'_smul, hF₁', mul_one, mul_one] at h''
    exact (ιapp_bijective O).1 h''
  · obtain ⟨g, hg⟩ := (ιapp_bijective O).2 (toFun' O O (F₁.app O y))
    refine ⟨g, ?_⟩
    change g • t = y
    have hfr : ∀ z : O, ∃ (U : Z.Opens), (z : Z) ∈ U ∧
        ∃ u : Γ(pb p L, U), Scheme.Modules.IsFrameOn u U := by
      intro z
      obtain ⟨U, hzU, ⟨e⟩⟩ := hN.1 (z : Z)
      exact ⟨U, hzU, Scheme.Modules.exists_isFrameOn_of_pullback_iso_unit U e⟩
    choose U hzU u hu using hfr
    let W : O → Z.Opens := fun z => U z ⊓ O
    have hcover : O ≤ ⨆ z : O, W z := fun x hx =>
      Opens.mem_iSup.mpr ⟨⟨x, hx⟩, ⟨hzU ⟨x, hx⟩, hx⟩⟩
    let F : TopCat.Sheaf Ab Z := ⟨(pb p L).presheaf, Scheme.Modules.isSheaf _⟩
    refine TopCat.Sheaf.eq_of_locally_eq' F W O (fun z => homOfLE inf_le_right) hcover (g • t) y fun
        z => ?_
    change (pb p L).presheaf.map (homOfLE (inf_le_right : W z ≤ O)).op (g • t) =
      (pb p L).presheaf.map (homOfLE (inf_le_right : W z ≤ O)).op y
    have hu' : Scheme.Modules.IsFrameOn ((pb p L).presheaf.map (homOfLE (inf_le_left : W z ≤ U
        z)).op (u z))
        (W z) := ((hu z).map (homOfLE inf_le_left)).mono inf_le_left
    have hbij := hu'.bijective (le_refl (W z)) le_rfl
    rw [map_self] at hbij
    set u' := (pb p L).presheaf.map (homOfLE (inf_le_left : W z ≤ U z)).op (u z) with hu'def
    clear_value u'
    obtain ⟨c, hc⟩ := hbij.2 ((pb p L).presheaf.map (homOfLE (inf_le_right : W z ≤ O)).op t)
    obtain ⟨d, hd⟩ := hbij.2 ((pb p L).presheaf.map (homOfLE (inf_le_right : W z ≤ O)).op y)
    change c • u' = _ at hc
    change d • u' = _ at hd
    have e1 : F₁.app (W z) ((pb p L).presheaf.map (homOfLE (inf_le_right : W z ≤ O)).op t) =
        (OO O).presheaf.map (homOfLE (inf_le_right : W z ≤ O)).op (F₁.app O t) := app_map _ F₁ _ t
    have e2 : F₁.app (W z) ((pb p L).presheaf.map (homOfLE (inf_le_right : W z ≤ O)).op y) =
        (OO O).presheaf.map (homOfLE (inf_le_right : W z ≤ O)).op (F₁.app O y) := app_map _ F₁ _ y
    set a := toFun' O (W z) (F₁.app (W z) u') with ha
    have h1 : O.ι.app (W z) c * a = 1 := by
      have := congrArg (toFun' O (W z)) (congrArg (F₁.app (W z)) hc)
      rw [Scheme.Modules.Hom.app_smul, toFun'_smul, e1, toFun'_map, hF₁', map_one] at this
      exact this
    have h2 : O.ι.app (W z) (Z.presheaf.map (homOfLE (inf_le_right : W z ≤ O)).op g) =
        O.ι.app (W z) d * a := by
      have := congrArg (toFun' O (W z)) (congrArg (F₁.app (W z)) hd)
      rw [Scheme.Modules.Hom.app_smul, toFun'_smul, e2, toFun'_map] at this
      rw [ιapp_map, hg]
      exact this.symm
    have h3 : Z.presheaf.map (homOfLE (inf_le_right : W z ≤ O)).op g * c = d := by
      apply ιapp_injective O (inf_le_right : W z ≤ O)
      rw [map_mul, h2, mul_assoc, mul_comm a, h1, mul_one]
    rw [Scheme.Modules.map_smul, ← hc, ← hd, ← mul_smul, h3]

theorem

isLocalizedModule_powers_of_comap

L369 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.isLocalizedModule_powers_of_comap

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol

Lean source · statement

theorem isLocalizedModule_powers_of_comap {A B M N : Type*} [CommRing A] [CommRing B] [AddCommGroup
  M]
    [AddCommGroup N] [Module B M] [Module B N] [Module A M] [Module A N] (φ : A →+* B)
    (hM : ∀ (a : A) (m : M), a • m = φ a • m) (hN : ∀ (a : A) (n : N), a • n = φ a • n) (r : A)
    (f : M →ₗ[B] N) [h : IsLocalizedModule (Submonoid.powers (φ r)) f] (g : M →ₗ[A] N)
    (hfg : ∀ x, g x = f x) : IsLocalizedModule (Submonoid.powers r) g

def

algAB

L402 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.algAB

Documentation

The algebra structure on inverse image sections induced by p.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)

Lean source · statement

def algAB : Algebra Γ(X, U) Γ(Z, p ⁻¹ᵁ U)

def

modAN

L405 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.modAN

Documentation

The scalar action on pullback module sections through the map induced by p.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)

Lean source · statement

def modAN : Module Γ(X, U) Γ(pb p L, p ⁻¹ᵁ U)

theorem

algebraMap_AB

L410 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.algebraMap_AB

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · statement

theorem algebraMap_AB (a : Γ(X, U)) : algebraMap Γ(X, U) Γ(Z, p ⁻¹ᵁ U) a = p.app U a

theorem

smul_AN

L412 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.smul_AN

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · statement

theorem smul_AN (a : Γ(X, U)) (n : Γ(pb p L, p ⁻¹ᵁ U)) : a • n = p.app U a • n

instance

isScalarTower_ABN

L414 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.isScalarTower_ABN

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · statement

instance isScalarTower_ABN : IsScalarTower Γ(X, U) Γ(Z, p ⁻¹ᵁ U) Γ(pb p L, p ⁻¹ᵁ U)

instance

smulCommClass_ABN

L419 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.smulCommClass_ABN

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · statement

instance smulCommClass_ABN : SMulCommClass Γ(X, U) Γ(Z, p ⁻¹ᵁ U) Γ(pb p L, p ⁻¹ᵁ U)

instance

smulCommClass_BAN

L424 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.smulCommClass_BAN

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · statement

instance smulCommClass_BAN : SMulCommClass Γ(Z, p ⁻¹ᵁ U) Γ(X, U) Γ(pb p L, p ⁻¹ᵁ U)

def

thetaFix

L428 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.thetaFix

Documentation

Multiply a pulled back section by a fixed section on the inverse image open.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · full declaration

def thetaFix (b : Γ(Z, p ⁻¹ᵁ U)) : Γ(L, U) →ₗ[Γ(X, U)] Γ(pb p L, p ⁻¹ᵁ U) where
  toFun s := b • eta p L U s
  map_add' s₁ s₂ := by
    rw [eta_add, smul_add]
  map_smul' a s := by
    change b • eta p L U (a • s) = p.app U a • (b • eta p L U s)
    rw [eta_smul, smul_smul, smul_smul, mul_comm]

def

thetaBilin

L437 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.thetaBilin

Documentation

The bilinear map multiplying coordinate sections by pulled back module sections.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · full declaration

def thetaBilin : Γ(Z, p ⁻¹ᵁ U) →ₗ[Γ(Z, p ⁻¹ᵁ U)] (Γ(L, U) →ₗ[Γ(X, U)] Γ(pb p L, p ⁻¹ᵁ U)) where
  toFun := thetaFix p L U
  map_add' b₁ b₂ := by
    ext s
    exact add_smul b₁ b₂ (eta p L U s)
  map_smul' c b := by
    ext s
    exact mul_smul c b (eta p L U s)

def

theta

L447 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.theta

Documentation

The canonical tensor product map to sections of the pullback module.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · statement

def theta : Γ(Z, p ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(L, U) →ₗ[Γ(Z, p ⁻¹ᵁ U)] Γ(pb p L, p ⁻¹ᵁ U)

theorem

theta_tmul

L450 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.theta_tmul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · statement

theorem theta_tmul (b : Γ(Z, p ⁻¹ᵁ U)) (s : Γ(L, U)) : theta p L U (b ⊗ₜ s) = b • eta p L U s

def

modAZW

L454 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.modAZW

Documentation

The scalar action on coordinate sections over W induced by the map on sections over U.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · statement

def modAZW (W : Z.Opens) (h : W ≤ p ⁻¹ᵁ U) : Module Γ(X, U) Γ(Z, W)

def

modANW

L458 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.modANW

Documentation

The scalar action on pullback module sections over W induced by sections over U.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · statement

def modANW (W : Z.Opens) (h : W ≤ p ⁻¹ᵁ U) : Module Γ(X, U) Γ(pb p L, W)

theorem

appLE_apply

L461 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.appLE_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · statement

theorem appLE_apply (W : Z.Opens) (h : W ≤ p ⁻¹ᵁ U) (a : Γ(X, U)) :
    p.appLE U W h a = Z.presheaf.map (homOfLE h).op (p.app U a)

def

resB

L465 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.resB

Documentation

Restriction of coordinate sections to an open subset of the inverse image of U.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · full declaration

def resB (W : Z.Opens) (h : W ≤ p ⁻¹ᵁ U) :
    letI := modAZW p U W h
    Γ(Z, p ⁻¹ᵁ U) →ₗ[Γ(X, U)] Γ(Z, W) :=
  letI := modAZW p U W h
  { toFun := Z.presheaf.map (homOfLE h).op
    map_add' := fun x y => map_add _ x y
    map_smul' := fun a x => by
      change Z.presheaf.map (homOfLE h).op (p.app U a * x) = p.appLE U W h a * _
      rw [map_mul, appLE_apply] }

def

resN

L476 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.resN

Documentation

Restriction of pullback module sections to an open subset of the inverse image of U.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · full declaration

def resN (W : Z.Opens) (h : W ≤ p ⁻¹ᵁ U) :
    letI := modANW p L U W h
    Γ(pb p L, p ⁻¹ᵁ U) →ₗ[Γ(X, U)] Γ(pb p L, W) :=
  letI := modANW p L U W h
  { toFun := (pb p L).presheaf.map (homOfLE h).op
    map_add' := fun x y => map_add _ x y
    map_smul' := fun a x => by
      change (pb p L).presheaf.map (homOfLE h).op (p.app U a • x) = p.appLE U W h a • _
      rw [Scheme.Modules.map_smul, appLE_apply] }

theorem

isLocalizedModule_resB_of_eq

L486 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.isLocalizedModule_resB_of_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · full declaration

theorem isLocalizedModule_resB_of_eq (hpU : IsAffineOpen (p ⁻¹ᵁ U)) (r : Γ(X, U)) (W : Z.Opens)
    (h : W ≤ p ⁻¹ᵁ U) (hW : W = Z.basicOpen (p.app U r)) :
    letI := modAZW p U W h
    IsLocalizedModule (Submonoid.powers r) (resB p U W h) := by
  subst hW
  let := modAZW p U (Z.basicOpen (p.app U r)) h
  have : IsLocalization.Away (p.app U r) Γ(Z, Z.basicOpen (p.app U r)) :=
      hpU.isLocalization_basicOpen _
  have : IsLocalizedModule (Submonoid.powers (p.app U r))
      (Algebra.linearMap (Z.presheaf.obj (op (p ⁻¹ᵁ U))) (Z.presheaf.obj (op (Z.basicOpen (p.app U
          r))))) :=
    (isLocalizedModule_iff_isLocalization' _ _).mpr inferInstance
  refine isLocalizedModule_powers_of_comap (p.app U).hom (fun a m => rfl) (fun a n => rfl) r
    (Algebra.linearMap (Z.presheaf.obj (op (p ⁻¹ᵁ U))) (Z.presheaf.obj (op (Z.basicOpen (p.app U
        r)))))
    (resB p U _ h) fun x => rfl

def

modBO

L504 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.modBO

Documentation

The scalar action on module sections over a basic open via localization.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · statement

def modBO (N : Z.Modules) (O : Z.Opens) (f : Γ(Z, O)) : Module Γ(Z, O) Γ(N, Z.basicOpen
    f)

def

resBO

L509 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.resBO

Documentation

Restriction of module sections to a basic open, linear over sections on the original open.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · full declaration

def resBO (N : Z.Modules) (O : Z.Opens) (f : Γ(Z, O)) :
    letI := modBO N O f
    Γ(N, O) →ₗ[Γ(Z, O)] Γ(N, Z.basicOpen f) :=
  letI := modBO N O f
  { toFun := N.presheaf.map (homOfLE (Z.basicOpen_le f)).op
    map_add' := fun x y => map_add _ x y
    map_smul' := fun a x => Scheme.Modules.map_smul N (homOfLE (Z.basicOpen_le f)) a x }

theorem

isLocalizedModule_resBO

L517 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.isLocalizedModule_resBO

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · full declaration

theorem isLocalizedModule_resBO (N : Z.Modules) (O : Z.Opens) (f : Γ(Z, O)) (hN :
  Scheme.Modules.IsInvertible N)
    (hO : IsAffineOpen O) :
    letI := modBO N O f
    IsLocalizedModule (Submonoid.powers f) (resBO N O f) := by
  let := modBO N O f
  have : IsLocalization.Away f Γ(Z, Z.basicOpen f) := hO.isLocalization_basicOpen f
  obtain ⟨h1, h2⟩ :=
    Scheme.Modules.isLocalization_basicOpen_of_locallyTrivial N hN.1 ⟨O, hO⟩ f
  refine ⟨?_, ?_, ?_⟩
  · rintro ⟨s, n, rfl⟩
    rw [Module.End.isUnit_iff]
    have hu : IsUnit (algebraMap Γ(Z, O) Γ(Z, Z.basicOpen f) (f ^ n)) := by
      rw [map_pow]; exact (IsLocalization.Away.algebraMap_isUnit f).pow n
    have := hu.smul_bijective (β := Γ(N, Z.basicOpen f))
    exact this
  · intro y
    obtain ⟨n, x, hx⟩ := h1 y
    exact ⟨⟨x, ⟨f ^ n, n, rfl⟩⟩, hx.symm⟩
  · intro x₁ x₂ h
    have h0 : N.presheaf.map (homOfLE (Z.basicOpen_le f)).op (x₁ - x₂) = 0 := by
      rw [map_sub]; exact sub_eq_zero.mpr h
    obtain ⟨n, hn⟩ := h2 (x₁ - x₂) h0
    refine ⟨⟨f ^ n, n, rfl⟩, ?_⟩
    rw [Submonoid.smul_def, Submonoid.smul_def, ← sub_eq_zero, ← smul_sub]
    exact hn

theorem

isLocalizedModule_resN_of_eq

L544 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.isLocalizedModule_resN_of_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · full declaration

theorem isLocalizedModule_resN_of_eq (hpU : IsAffineOpen (p ⁻¹ᵁ U)) (hN :
  Scheme.Modules.IsInvertible (pb p L))
    (r : Γ(X, U)) (W : Z.Opens) (h : W ≤ p ⁻¹ᵁ U) (hW : W = Z.basicOpen (p.app U r)) :
    letI := modANW p L U W h
    IsLocalizedModule (Submonoid.powers r) (resN p L U W h) := by
  subst hW
  let := modANW p L U (Z.basicOpen (p.app U r)) h
  let := modBO (pb p L) (p ⁻¹ᵁ U) (p.app U r)
  have := isLocalizedModule_resBO (pb p L) (p ⁻¹ᵁ U) (p.app U r) hN hpU
  refine isLocalizedModule_powers_of_comap (p.app U).hom (fun a m => rfl) (fun a n => rfl) r
    (resBO (pb p L) (p ⁻¹ᵁ U) (p.app U r)) (resN p L U _ h) fun x => rfl

theorem

pre_le

L556 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.pre_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_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · statement

theorem pre_le (r : Γ(X, U)) : p ⁻¹ᵁ X.basicOpen r ≤ p ⁻¹ᵁ U

def

modAZ

L559 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.modAZ

Documentation

The scalar action on coordinate sections over the inverse image of a basic open.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · statement

def modAZ (r : Γ(X, U)) : Module Γ(X, U) Γ(Z, p ⁻¹ᵁ X.basicOpen r)

def

modANr

L563 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.modANr

Documentation

The scalar action on pullback module sections over the inverse image of a basic open.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN

Lean source · statement

def modANr (r : Γ(X, U)) : Module Γ(X, U) Γ(pb p L, p ⁻¹ᵁ X.basicOpen r)

theorem

smul_AZ

L568 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.smul_AZ

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN
attribute [local instance] modAZ modANr modBO

Lean source · statement

theorem smul_AZ (r : Γ(X, U)) (a : Γ(X, U)) (b : Γ(Z, p ⁻¹ᵁ X.basicOpen r)) :
    a • b = p.appLE U (p ⁻¹ᵁ X.basicOpen r) (pre_le p U r) a * b

theorem

smul_ANr

L571 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.smul_ANr

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN
attribute [local instance] modAZ modANr modBO

Lean source · statement

theorem smul_ANr (r : Γ(X, U)) (a : Γ(X, U)) (n : Γ(pb p L, p ⁻¹ᵁ X.basicOpen r)) :
    a • n = p.appLE U (p ⁻¹ᵁ X.basicOpen r) (pre_le p U r) a • n

theorem

smul_BO

L574 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.smul_BO

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN
attribute [local instance] modAZ modANr modBO

Lean source · statement

theorem smul_BO (r : Γ(X, U)) (a : Γ(X, U)) (m : Γ(L, X.basicOpen r)) :
    a • m = X.presheaf.map (homOfLE (X.basicOpen_le r)).op a • m

theorem

app_res

L577 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.app_res

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN
attribute [local instance] modAZ modANr modBO

Lean source · statement

theorem app_res (r : Γ(X, U)) (a : Γ(X, U)) :
    p.app (X.basicOpen r) (X.presheaf.map (homOfLE (X.basicOpen_le r)).op a) =
      p.appLE U (p ⁻¹ᵁ X.basicOpen r) (pre_le p U r) a

def

thetaLoc

L585 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.thetaLoc

Documentation

The tensor product map to pullback module sections over the inverse image of a basic open.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN
attribute [local instance] modAZ modANr modBO

Lean source · statement

def thetaLoc (r : Γ(X, U)) :
    Γ(Z, p ⁻¹ᵁ X.basicOpen r) ⊗[Γ(X, U)] Γ(L, X.basicOpen r) →ₗ[Γ(X, U)] Γ(pb p L, p ⁻¹ᵁ X.basicOpen
        r)

theorem

thetaLoc_tmul

L601 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.thetaLoc_tmul

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN
attribute [local instance] modAZ modANr modBO

Lean source · statement

theorem thetaLoc_tmul (r : Γ(X, U)) (b : Γ(Z, p ⁻¹ᵁ X.basicOpen r)) (m : Γ(L, X.basicOpen r)) :
    thetaLoc p L U r (b ⊗ₜ m) = b • eta p L (X.basicOpen r) m

def

resT

L606 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.resT

Documentation

Restriction of both factors in the tensor product to a basic open and its inverse image.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN
attribute [local instance] modAZ modANr modBO

Lean source · statement

def resT (r : Γ(X, U)) :
    Γ(Z, p ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(L, U) →ₗ[Γ(X, U)] Γ(Z, p ⁻¹ᵁ X.basicOpen r) ⊗[Γ(X, U)] Γ(L,
        X.basicOpen r)

def

thetaA

L612 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.thetaA

Documentation

The canonical pullback section map with scalars restricted to sections over U.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN
attribute [local instance] modAZ modANr modBO

Lean source · statement

def thetaA : Γ(Z, p ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(L, U) →ₗ[Γ(X, U)] Γ(pb p L, p ⁻¹ᵁ U)

theorem

thetaA_apply

L615 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.thetaA_apply

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN
attribute [local instance] modAZ modANr modBO

Lean source · statement

theorem thetaA_apply (x : Γ(Z, p ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(L, U)) : thetaA p L U x = theta p L U x

theorem

thetaLoc_comp_resT

L617 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.thetaLoc_comp_resT

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN
attribute [local instance] modAZ modANr modBO

Lean source · statement

theorem thetaLoc_comp_resT (r : Γ(X, U)) :
    thetaLoc p L U r ∘ₗ resT p L U r = resN p L U (p ⁻¹ᵁ X.basicOpen r) (pre_le p U r) ∘ₗ thetaA p L
        U

theorem

thetaLoc_bijective_of_frame

L628 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.thetaLoc_bijective_of_frame

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN
attribute [local instance] modAZ modANr modBO

Lean source · statement

theorem thetaLoc_bijective_of_frame (hU : IsAffineOpen U) (hpU : IsAffineOpen (p ⁻¹ᵁ U))
    (hN : Scheme.Modules.IsInvertible (pb p L)) (r : Γ(X, U)) {s₀ : Γ(L, X.basicOpen r)}
    (hs₀ : Scheme.Modules.IsFrameOn s₀ (X.basicOpen r)) : Function.Bijective (thetaLoc p L U r)

theorem

exists_basicOpen_isFrameOn

L670 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.exists_basicOpen_isFrameOn

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN
attribute [local instance] modAZ modANr modBO

Lean source · statement

theorem exists_basicOpen_isFrameOn (hL : Scheme.Modules.IsInvertible L) (hU : IsAffineOpen U) {x :
  X}
    (hx : x ∈ U) : ∃ f : Γ(X, U), x ∈ X.basicOpen f ∧
      ∃ s : Γ(L, X.basicOpen f), Scheme.Modules.IsFrameOn s (X.basicOpen f)

theorem

theta_bijective

L679 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.theta_bijective

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN
attribute [local instance] modAZ modANr modBO

Lean source · statement

theorem theta_bijective (hL : Scheme.Modules.IsInvertible L) (hU : IsAffineOpen U)
    (hpU : IsAffineOpen (p ⁻¹ᵁ U)) : Function.Bijective (theta p L U)

def

beta

L717 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.beta

Documentation

The linear equivalence between extended sections and pullback sections on an affine inverse image.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN
attribute [local instance] modAZ modANr modBO

Lean source · statement

def beta (hL : Scheme.Modules.IsInvertible L) (hU : IsAffineOpen U) (hpU : IsAffineOpen (p ⁻¹ᵁ U)) :
    Γ(Z, p ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(L, U) ≃ₗ[Γ(Z, p ⁻¹ᵁ U)] Γ(pb p L, p ⁻¹ᵁ U)

theorem

beta_tmul

L721 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.beta_tmul

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol
section Affine
variable {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
attribute [local instance] algAB modAN
attribute [local instance] modAZ modANr modBO

Lean source · statement

theorem beta_tmul (hL : Scheme.Modules.IsInvertible L) (hU : IsAffineOpen U) (hpU : IsAffineOpen (p
  ⁻¹ᵁ U))
    (b : Γ(Z, p ⁻¹ᵁ U)) (s : Γ(L, U)) : beta p L U hL hU hpU (b ⊗ₜ s) = b • eta p L U s

theorem

beta_one_tmul

L728 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.beta_one_tmul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol

Lean source · full declaration

theorem beta_one_tmul {X Z : Scheme.{u}} (p : Z ⟶ X) (L : X.Modules) (U : X.Opens)
    (hL : Scheme.Modules.IsInvertible L) (hU : IsAffineOpen U) (hpU : IsAffineOpen (p ⁻¹ᵁ U)) (s :
        Γ(L, U)) :
    letI := algAB p U
    beta p L U hL hU hpU (1 ⊗ₜ s) = eta p L U s := by
  rw [beta_tmul, one_smul]

theorem

result

L735 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback.P2mPullbackSectionsSol.result

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
noncomputable section
namespace P2mPullbackSectionsSol

Lean source · full declaration

theorem result {X Z : Scheme.{u}} (p : Z ⟶ X) {L : X.Modules} (hL : Scheme.Modules.IsInvertible L)
    (U : X.Opens) (hU : IsAffineOpen U) (hpU : IsAffineOpen (p ⁻¹ᵁ U)) :
    letI := (p.app U).hom.toAlgebra
    ∃ β : Γ(Z, p ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(L, U) ≃ₗ[Γ(Z, p ⁻¹ᵁ U)] Γ((Scheme.Modules.pullback p).obj L, p
        ⁻¹ᵁ U),
      ∀ s : Γ(L, U), β (1 ⊗ₜ s) = (((Scheme.Modules.pullbackPushforwardAdjunction p).unit.app L).app
          U) s :=
  ⟨beta p L U hL hU hpU, beta_one_tmul p L U hL hU hpU⟩

theorem

exists_baseChange_sections_linearEquiv_pullback

L749 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.exists_baseChange_sections_linearEquiv_pullback

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback
universe u
open CategoryTheory AlgebraicGeometry TensorProduct TopologicalSpace Opposite
with_weak_namespace _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible

Lean source · full declaration

theorem exists_baseChange_sections_linearEquiv_pullback
    {X Z : Scheme.{u}} (p : Z ⟶ X) {L : X.Modules} (hL : Scheme.Modules.IsInvertible L)
    (U : X.Opens) (hU : IsAffineOpen U) (hpU : IsAffineOpen (p ⁻¹ᵁ U)) :
    letI := (p.app U).hom.toAlgebra
    ∃ β : Γ(Z, p ⁻¹ᵁ U) ⊗[Γ(X, U)] Γ(L, U) ≃ₗ[Γ(Z, p ⁻¹ᵁ U)] Γ((Scheme.Modules.pullback p).obj L, p
        ⁻¹ᵁ U),
      ∀ s : Γ(L, U), β (1 ⊗ₜ s) = (((Scheme.Modules.pullbackPushforwardAdjunction p).unit.app L).app
          U) s :=
  (open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs in
  open Scheme_Modules_IsInvertible_exists_baseChange_sections_linearEquiv_pullback in
      P2mPullbackSectionsSol.result p hL U hU hpU)

Module documentation

Extended sections of an invertible module and pullback

Declarations