NYLL
Module

Scheme_Modules_nonempty_pullback_det_iso_det_pullback.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_nonempty_pullback_det_iso_det_pullback
57 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules nonempty pullback det iso det pullback

Imports9
Imported by3

Declarations

abbrev

F

L58 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.F
Documentation

The module obtained by pulling back the given module along the scheme morphism.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
abbrev F : X.Modules
abbrev

pre

L61 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.pre
Documentation

The presheaf exterior power used to construct the determinant sheaf.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
abbrev pre {Z : Scheme.{u}} (M : Z.Modules) : Z.PresheafOfModules
def

eta

L65 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.eta
Documentation

The local section induced by the unit of the pullback-pushforward adjunction.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
def eta (U : Y.Opens) (e : Γ(E, U)) : Γ(F ψ E, ψ ⁻¹ᵁ U)
lemma

eta_add

L68 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.eta_add
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma eta_add (U : Y.Opens) (e e' : Γ(E, U)) : eta ψ E U (e + e') = eta ψ E U e + eta ψ E U e'
lemma

eta_sum

L71 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.eta_sum
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma eta_sum (U : Y.Opens) {ι : Type*} (T : Finset ι) (f : ι → Γ(E, U)) :
    eta ψ E U (∑ t ∈ T, f t) = ∑ t ∈ T, eta ψ E U (f t)
lemma

eta_smul

L75 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.eta_smul
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma eta_smul (U : Y.Opens) (r : Γ(Y, U)) (e : Γ(E, U)) :
    eta ψ E U (r • e) = ψ.app U r • eta ψ E U e
def

toSh

L80 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.toSh
Documentation

Maps a local exterior-power element into its determinant sheaf by the sheafification unit.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
def toSh {Z : Scheme.{u}} (M : Z.Modules) (W : Z.Opens) :
    (⋀[Γ(Z, W)]^n Γ(M, W)) → Γ(det n M, W)
lemma

toSh_add

L86 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.toSh_add
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma toSh_add {Z : Scheme.{u}} (M : Z.Modules) (W : Z.Opens) (w w' : ⋀[Γ(Z, W)]^n Γ(M, W)) :
    toSh n M W (w + w') = toSh n M W w + toSh n M W w'
lemma

toSh_smul

L92 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.toSh_smul
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma toSh_smul {Z : Scheme.{u}} (M : Z.Modules) (W : Z.Opens) (r : Γ(Z, W)) (w : ⋀[Γ(Z, W)]^n Γ(M,
  W)) :
    toSh n M W (r • w) = r • toSh n M W w
lemma

toSh_res

L98 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.toSh_res
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · full declaration
lemma toSh_res {Z : Scheme.{u}} (M : Z.Modules) {W W' : Z.Opens} (i : W' ⟶ W) (w : ⋀[Γ(Z, W)]^n
  Γ(M, W)) :
    (det n M).presheaf.map i.op (toSh n M W w) =
      toSh n M W' (show ⋀[Γ(Z, W')]^n Γ(M, W') from (pre n M).map i.op (show (pre n M).obj (op W)
        from w)) := by
  have hnat := (((PresheafOfModules.sheafificationAdjunction (𝟙 Z.ringCatSheaf.obj)).unit.app
    (pre n M))).naturality i.op
  have hx := congrArg (fun φ => φ.hom (show (pre n M).obj (op W) from w)) hnat
  exact hx.symm
def

along

L113 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.along
Documentation

Restricts a module scalar action along the map on structure-sheaf sections.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section compare
variable (U : Y.Opens)
Lean source · statement
def along (N : Type u) [AddCommGroup N] [Module Γ(X, ψ ⁻¹ᵁ U) N] :
    Module Γ(Y, U) N
def

etaₗ

L118 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.etaₗ
Documentation

The adjunction-unit section map viewed as a linear map after restricting scalars.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section compare
variable (U : Y.Opens)
Lean source · full declaration
def etaₗ : letI := along ψ U Γ(F ψ E, ψ ⁻¹ᵁ U); Γ(E, U) →ₗ[Γ(Y, U)] Γ(F ψ E, ψ ⁻¹ᵁ U)
  :=
  letI := along ψ U Γ(F ψ E, ψ ⁻¹ᵁ U)
  { toFun := fun e => eta ψ E U e
    map_add' := eta_add ψ E U
    map_smul' := fun r e => eta_smul ψ E U r e }
def

ιMultiAlong

L127 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.ιMultiAlong
Documentation

The canonical alternating exterior-product map with scalars restricted along the section-ring map.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section compare
variable (U : Y.Opens)
Lean source · full declaration
def ιMultiAlong :
    letI := along ψ U Γ(F ψ E, ψ ⁻¹ᵁ U)
    letI := along ψ U (⋀[Γ(X, ψ ⁻¹ᵁ U)]^n Γ(F ψ E, ψ ⁻¹ᵁ U))
    Γ(F ψ E, ψ ⁻¹ᵁ U) [⋀^Fin n]→ₗ[Γ(Y, U)] (⋀[Γ(X, ψ ⁻¹ᵁ U)]^n Γ(F ψ E, ψ ⁻¹ᵁ U)) :=
  letI := along ψ U Γ(F ψ E, ψ ⁻¹ᵁ U)
  letI := along ψ U (⋀[Γ(X, ψ ⁻¹ᵁ U)]^n Γ(F ψ E, ψ ⁻¹ᵁ U))
  { toFun := exteriorPower.ιMulti Γ(X, ψ ⁻¹ᵁ U) n (M := Γ(F ψ E, ψ ⁻¹ᵁ U))
    map_update_add' :=
      (exteriorPower.ιMulti Γ(X, ψ ⁻¹ᵁ U) n (M := Γ(F ψ E, ψ ⁻¹ᵁ U))).map_update_add'
    map_update_smul' := fun v i r x => by
      change (exteriorPower.ιMulti Γ(X, ψ ⁻¹ᵁ U) n (M := Γ(F ψ E, ψ ⁻¹ᵁ U)))
          (Function.update v i ((ψ.app U).hom r • x)) =
        (ψ.app U).hom r • (exteriorPower.ιMulti Γ(X, ψ ⁻¹ᵁ U) n (M := Γ(F ψ E, ψ ⁻¹ᵁ U)))
          (Function.update v i x)
      exact (exteriorPower.ιMulti Γ(X, ψ ⁻¹ᵁ U) n (M := Γ(F ψ E, ψ ⁻¹ᵁ U))).map_update_smul
        v i ((ψ.app U).hom r) x
    map_eq_zero_of_eq' := fun v _ _ h hij =>
      (exteriorPower.ιMulti Γ(X, ψ ⁻¹ᵁ U) n (M := Γ(F ψ E, ψ ⁻¹ᵁ U))).map_eq_zero_of_eq v h hij }
lemma

ιMultiAlong_apply

L146 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.ιMultiAlong_apply
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section compare
variable (U : Y.Opens)
Lean source · statement
lemma ιMultiAlong_apply (v : Fin n → Γ(F ψ E, ψ ⁻¹ᵁ U)) :
    ιMultiAlong ψ n E U v = exteriorPower.ιMulti Γ(X, ψ ⁻¹ᵁ U) n v
lemma

etaₗ_apply

L151 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.etaₗ_apply
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section compare
variable (U : Y.Opens)
Lean source · statement
lemma etaₗ_apply (e : Γ(E, U)) : etaₗ ψ E U e = eta ψ E U e
def

wedgeEtaₗ

L154 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.wedgeEtaₗ
Documentation

The linear map on exterior powers induced by the local adjunction-unit map.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section compare
variable (U : Y.Opens)
Lean source · full declaration
def wedgeEtaₗ :
    letI := along ψ U (⋀[Γ(X, ψ ⁻¹ᵁ U)]^n Γ(F ψ E, ψ ⁻¹ᵁ U))
    (⋀[Γ(Y, U)]^n Γ(E, U)) →ₗ[Γ(Y, U)] (⋀[Γ(X, ψ ⁻¹ᵁ U)]^n Γ(F ψ E, ψ ⁻¹ᵁ U)) :=
  letI := along ψ U Γ(F ψ E, ψ ⁻¹ᵁ U)
  letI := along ψ U (⋀[Γ(X, ψ ⁻¹ᵁ U)]^n Γ(F ψ E, ψ ⁻¹ᵁ U))
  exteriorPower.alternatingMapLinearEquiv ((ιMultiAlong ψ n E U).compLinearMap (etaₗ ψ E U))
lemma

wedgeEtaₗ_ιMulti

L161 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.wedgeEtaₗ_ιMulti
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section compare
variable (U : Y.Opens)
Lean source · full declaration
lemma wedgeEtaₗ_ιMulti (e : Fin n → Γ(E, U)) :
    wedgeEtaₗ ψ n E U (exteriorPower.ιMulti Γ(Y, U) n e) =
      exteriorPower.ιMulti Γ(X, ψ ⁻¹ᵁ U) n (fun i => eta ψ E U (e i)) := by
  let := along ψ U Γ(F ψ E, ψ ⁻¹ᵁ U)
  let := along ψ U (⋀[Γ(X, ψ ⁻¹ᵁ U)]^n Γ(F ψ E, ψ ⁻¹ᵁ U))
  simp only [wedgeEtaₗ, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti,
    AlternatingMap.compLinearMap_apply]
  rw [ιMultiAlong_apply]
  rfl
lemma

wedgeEtaₗ_smul

L171 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.wedgeEtaₗ_smul
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section compare
variable (U : Y.Opens)
Lean source · statement
lemma wedgeEtaₗ_smul (r : Γ(Y, U)) (w : ⋀[Γ(Y, U)]^n Γ(E, U)) :
    wedgeEtaₗ ψ n E U (r • w) = ψ.app U r • wedgeEtaₗ ψ n E U w
def

bFun

L177 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.bFun
Documentation

Sends a local exterior-power element to the determinant of the pulled-back module.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section compare
variable (U : Y.Opens)
Lean source · statement
def bFun : (⋀[Γ(Y, U)]^n Γ(E, U)) → Γ(det n (F ψ E), ψ ⁻¹ᵁ U)
lemma

bFun_ιMulti

L180 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.bFun_ιMulti
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section compare
variable (U : Y.Opens)
Lean source · full declaration
lemma bFun_ιMulti (e : Fin n → Γ(E, U)) :
    bFun ψ n E U (exteriorPower.ιMulti Γ(Y, U) n e) =
      toSh n (F ψ E) (ψ ⁻¹ᵁ U) (exteriorPower.ιMulti Γ(X, ψ ⁻¹ᵁ U) n (fun i => eta ψ E U (e i))) :=
        by
  rw [bFun, wedgeEtaₗ_ιMulti]
lemma

bFun_add

L186 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.bFun_add
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section compare
variable (U : Y.Opens)
Lean source · statement
lemma bFun_add (w w' : ⋀[Γ(Y, U)]^n Γ(E, U)) : bFun ψ n E U (w + w') = bFun ψ n E U w + bFun ψ n E
  U w'
lemma

bFun_smul

L190 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.bFun_smul
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section compare
variable (U : Y.Opens)
Lean source · statement
lemma bFun_smul (r : Γ(Y, U)) (w : ⋀[Γ(Y, U)]^n Γ(E, U)) :
    bFun ψ n E U (r • w) = ψ.app U r • bFun ψ n E U w
lemma

map_eta

L214 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.map_eta
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma map_eta {U U' : (Y.Opens)ᵒᵖ} (i : U ⟶ U') (e : Γ(E, U.unop)) :
    (((F ψ E).presheaf.map ((Opens.map ψ.base).map i.unop).op :
        Γ(F ψ E, ψ ⁻¹ᵁ U.unop) ⟶ _) (eta ψ E U.unop e) : Γ(F ψ E, ψ ⁻¹ᵁ U'.unop)) =
      eta ψ E U'.unop ((E.presheaf.map i : Γ(E, U.unop) ⟶ _) e)
abbrev

preMap

L224 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.preMap
Documentation

The restriction map between local exterior powers on two open subsets.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
abbrev preMap {Z : Scheme.{u}} (M : Z.Modules) {W W' : Z.Opens} (j : W' ⟶ W)
    (w : ⋀[Γ(Z, W)]^n Γ(M, W)) : ⋀[Γ(Z, W')]^n Γ(M, W')
lemma

preMap_ιMulti

L228 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.preMap_ιMulti
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · full declaration
lemma preMap_ιMulti {Z : Scheme.{u}} (M : Z.Modules) {W W' : Z.Opens} (j : W' ⟶ W) (m : Fin n →
  Γ(M, W)) :
    preMap n M j (exteriorPower.ιMulti _ n m) =
      exteriorPower.ιMulti _ n (fun k => (M.presheaf.map j.op : Γ(M, W) ⟶ _) (m k)) :=
  PresheafOfModules.exteriorPower_map_ιMulti n M.val j.op m
lemma

preMap_add

L234 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.preMap_add
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma preMap_add {Z : Scheme.{u}} (M : Z.Modules) {W W' : Z.Opens} (j : W' ⟶ W)
    (w w' : ⋀[Γ(Z, W)]^n Γ(M, W)) : preMap n M j (w + w') = preMap n M j w + preMap n M j w'
lemma

preMap_smul

L238 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.preMap_smul
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma preMap_smul {Z : Scheme.{u}} (M : Z.Modules) {W W' : Z.Opens} (j : W' ⟶ W)
    (r : Γ(Z, W)) (w : ⋀[Γ(Z, W)]^n Γ(M, W)) :
    preMap n M j (r • w) = Z.presheaf.map j.op r • preMap n M j w
lemma

bFun_natural

L243 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.bFun_natural
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma bFun_natural {U U' : Y.Opens} (i : U' ⟶ U) (w : ⋀[Γ(Y, U)]^n Γ(E, U)) :
    bFun ψ n E U' (preMap n E i w) =
      ((det n (F ψ E)).presheaf.map ((Opens.map ψ.base).map i).op :
        Γ(det n (F ψ E), ψ ⁻¹ᵁ U) ⟶ Γ(det n (F ψ E), ψ ⁻¹ᵁ U')) (bFun ψ n E U w)
abbrev

tgt

L282 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.tgt
Documentation

The determinant of the pullback, pushed forward and viewed over the original ring presheaf.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
abbrev tgt : Y.PresheafOfModules
lemma

bFun_zero

L286 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.bFun_zero
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma bFun_zero (U : Y.Opens) : bFun ψ n E U 0 = 0
def

bAb

L293 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.bAb
Documentation

The natural transformation of additive presheaves defined by the local determinant comparison.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · full declaration
def bAb : (pre n E).presheaf ⟶ (tgt ψ n E).presheaf where
  app U := AddCommGrpCat.ofHom (X := ⋀[Γ(Y, U.unop)]^n Γ(E, U.unop)) (Y := Γ(det n (F ψ E), ψ ⁻¹ᵁ
    U.unop))
    { toFun := bFun ψ n E U.unop
      map_zero' := bFun_zero ψ n E U.unop
      map_add' := bFun_add ψ n E U.unop }
  naturality {U U'} i := by
    ext w
    exact bFun_natural ψ n E i.unop w
def

bHom

L305 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.bHom
Documentation

The presheaf-of-modules morphism defined by the additive determinant comparison and its scalar law.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
def bHom : pre n E ⟶ tgt ψ n E
def

β

L312 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.β
Documentation

The sheaf morphism extending the local determinant comparison by the sheafification adjunction.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
def β : det n E ⟶ (pushforward ψ).obj (det n (F ψ E))
def

α

L318 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.α
Documentation

The determinant comparison from the pullback of the determinant, obtained by the pullback adjunction.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
def α : (Modules.pullback ψ).obj (det n E) ⟶ det n (F ψ E)
lemma

β_toSh

L321 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.β_toSh
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma β_toSh (U : Y.Opens) (w : ⋀[Γ(Y, U)]^n Γ(E, U)) :
    (β ψ n E).app U (toSh n E U w) = bFun ψ n E U w
lemma

α_unit_toSh

L332 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.α_unit_toSh
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · full declaration
lemma α_unit_toSh (U : Y.Opens) (e : Fin n → Γ(E, U)) :
    (α ψ n E).app (ψ ⁻¹ᵁ U)
        (((pullbackPushforwardAdjunction ψ).unit.app (det n E)).app U
          (toSh n E U (exteriorPower.ιMulti _ n e))) =
      toSh n (F ψ E) (ψ ⁻¹ᵁ U) (exteriorPower.ιMulti _ n (fun i => eta ψ E U (e i))) := by
  have h1 : ((pullbackPushforwardAdjunction ψ).homEquiv _ _) (α ψ n E) = β ψ n E :=
    Equiv.apply_symm_apply _ _
  rw [Adjunction.homEquiv_unit] at h1
  have h2 := congrArg (fun γ => (Modules.Hom.app γ U) (toSh n E U (exteriorPower.ιMulti _ n e))) h1
  simp only [Modules.Hom.comp_app] at h2
  rw [β_toSh, bFun_ιMulti] at h2
  exact h2
abbrev

res

L364 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.res
Documentation

Restricts a module section along an inclusion of open subsets.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
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

L368 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.res_res
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
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_eq_map

L374 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.res_eq_map
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
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

L378 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.res_smul
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
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

L383 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.res_add
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
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

L386 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.res_sum
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
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

app_res

L390 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.app_res
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma app_res {Z : Scheme.{u}} {M N : Z.Modules} (φ : M ⟶ N) {W' W : Z.Opens} (h : W' ≤ W) (s :
  Γ(M, W)) :
    φ.app W' (res M h s) = res N h (φ.app W s)
lemma

preMap_comp

L398 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.preMap_comp
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma preMap_comp {Z : Scheme.{u}} (M : Z.Modules) {W₁ W₂ W₃ : Z.Opens} (h₂₁ : W₂ ≤ W₁) (h₃₂ : W₃ ≤
  W₂)
    (w : ⋀[Γ(Z, W₁)]^n Γ(M, W₁)) :
    preMap n M (homOfLE h₃₂) (preMap n M (homOfLE h₂₁) w) = preMap n M (homOfLE (h₃₂.trans h₂₁)) w
lemma

preMap_zero

L408 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.preMap_zero
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma preMap_zero {Z : Scheme.{u}} (M : Z.Modules) {W W' : Z.Opens} (j : W' ⟶ W) :
    preMap n M j (0 : ⋀[Γ(Z, W)]^n Γ(M, W)) = 0
lemma

res_toSh

L412 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.res_toSh
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma res_toSh {Z : Scheme.{u}} (M : Z.Modules) {W' W : Z.Opens} (h : W' ≤ W) (w : ⋀[Γ(Z, W)]^n
  Γ(M, W)) :
    res (det n M) h (toSh n M W w) = toSh n M W' (preMap n M (homOfLE h) w)
lemma

res_eta

L417 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.res_eta
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma res_eta {V U : Y.Opens} (h : U ≤ V) (e : Γ(E, V)) :
    res (F ψ E) (ψ.preimage_mono h) (eta ψ E V e) = eta ψ E U (res E h e)
lemma

ιMulti_comp_mem

L423 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.ιMulti_comp_mem
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma ιMulti_comp_mem {A : Type u} [CommRing A] {M : Type u} [AddCommGroup M] [Module A M] {m : ℕ}
    (w : Fin m → M) (P : Submodule A (⋀[A]^m M)) (hP : exteriorPower.ιMulti A m w ∈ P)
    (φ : Fin m → Fin m) : exteriorPower.ιMulti A m (w ∘ φ) ∈ P
lemma

ιMulti_mem_span_singleton

L438 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.ιMulti_mem_span_singleton
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · full declaration
lemma ιMulti_mem_span_singleton {A : Type u} [CommRing A] {M : Type u} [AddCommGroup M] [Module A M]
    (g : Fin n → M) (a : Fin n → Fin n → A) :
    exteriorPower.ιMulti A n (fun t => ∑ k, a t k • g k) ∈
      Submodule.span A {exteriorPower.ιMulti A n g} := by
  classical
  have hsum := (exteriorPower.ιMulti A n (M := M)).toMultilinearMap.map_sum (fun t k => a t k • g k)
  change exteriorPower.ιMulti A n (fun t => ∑ k, a t k • g k) = _ at hsum
  rw [hsum]
  refine Submodule.sum_mem _ fun r _ => ?_
  have hsm := (exteriorPower.ιMulti A n (M := M)).toMultilinearMap.map_smul_univ (fun t => a t (r
    t)) (fun t => g (r t))
  change exteriorPower.ιMulti A n (fun t => a t (r t) • g (r t)) =
    (∏ t, a t (r t)) • exteriorPower.ιMulti A n (fun t => g (r t)) at hsm
  change exteriorPower.ιMulti A n (fun t => a t (r t) • g (r t)) ∈ _
  rw [hsm]
  exact Submodule.smul_mem _ _ (ιMulti_comp_mem g _ (Submodule.subset_span (Set.mem_singleton _)) r)
def

gsec

L461 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.gsec
Documentation

The restrictions of a chosen family of local sections after applying the pullback adjunction unit.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section frame
variable {V : Y.Opens} (e : Fin n → Γ(E, V))
Lean source · statement
def gsec {W : X.Opens} (hW : W ≤ ψ ⁻¹ᵁ V) : Fin n → Γ(F ψ E, W)
lemma

res_gsec

L464 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.res_gsec
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section frame
variable {V : Y.Opens} (e : Fin n → Γ(E, V))
Lean source · statement
lemma res_gsec {W W' : X.Opens} (hW : W ≤ ψ ⁻¹ᵁ V) (h : W' ≤ W) (j : Fin n) :
    res (F ψ E) h (gsec ψ n E e hW j) = gsec ψ n E e (h.trans hW) j
lemma

sect

L473 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.sect
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section frame
variable {V : Y.Opens} (e : Fin n → Γ(E, V))
variable (hb : ∀ (U' : Y.Opens) (hU' : U' ≤ V), ∃ b : Module.Basis (Fin n) Γ(Y, U') Γ(E, U'),
  ∀ i, b i = E.presheaf.map (homOfLE hU').op (e i))
variable {x : X} (hxV : ψ.base x ∈ V)
include hb hxV in
Lean source · statement
lemma sect {W : X.Opens} (s : Γ(F ψ E, W)) (hx : x ∈ W) :
    ∃ (W' : X.Opens) (i : W' ≤ W) (j : W' ≤ ψ ⁻¹ᵁ V), x ∈ W' ∧ ∃ a : Fin n → Γ(X, W'),
      res (F ψ E) i s = ∑ k, a k • gsec ψ n E e j k
lemma

sectFin

L495 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.sectFin
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section frame
variable {V : Y.Opens} (e : Fin n → Γ(E, V))
variable (hb : ∀ (U' : Y.Opens) (hU' : U' ≤ V), ∃ b : Module.Basis (Fin n) Γ(Y, U') Γ(E, U'),
  ∀ i, b i = E.presheaf.map (homOfLE hU').op (e i))
variable {x : X} (hxV : ψ.base x ∈ V)
include hb hxV in
Lean source · full declaration
lemma sectFin : ∀ (m : ℕ) {W : X.Opens} (y : Fin m → Γ(F ψ E, W)) (_ : x ∈ W),
    ∃ (W' : X.Opens) (i : W' ≤ W) (j : W' ≤ ψ ⁻¹ᵁ V), x ∈ W' ∧ ∃ a : Fin m → Fin n → Γ(X, W'),
      ∀ t, res (F ψ E) i (y t) = ∑ k, a t k • gsec ψ n E e j k
  | 0, W, y, hx =>
      ⟨W ⊓ ψ ⁻¹ᵁ V, inf_le_left, inf_le_right, ⟨hx, hxV⟩, fun t => t.elim0, fun t => t.elim0⟩
  | m + 1, W, y, hx => by
    obtain ⟨W₁, i₁, j₁, hx₁, a₁, ha₁⟩ := sectFin m (fun t => y t.succ) hx
    obtain ⟨W₂, i₂, j₂, hx₂, a₀, ha₀⟩ := sect ψ n E e hb hxV (res (F ψ E) i₁ (y 0)) hx₁
    refine ⟨W₂, i₂.trans i₁, j₂, hx₂,
      Fin.cons a₀ (fun t k => X.presheaf.map (homOfLE i₂).op (a₁ t k)), fun t => ?_⟩
    refine Fin.cases ?_ (fun t => ?_) t
    · rw [Fin.cons_zero, ← res_res (F ψ E) i₁ i₂]
      exact ha₀
    · rw [Fin.cons_succ, ← res_res (F ψ E) i₁ i₂, ha₁ t, res_sum]
      refine Finset.sum_congr rfl fun k _ => ?_
      rw [res_smul, res_gsec]
lemma

wedge_local

L512 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.wedge_local
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
section frame
variable {V : Y.Opens} (e : Fin n → Γ(E, V))
variable (hb : ∀ (U' : Y.Opens) (hU' : U' ≤ V), ∃ b : Module.Basis (Fin n) Γ(Y, U') Γ(E, U'),
  ∀ i, b i = E.presheaf.map (homOfLE hU').op (e i))
variable {x : X} (hxV : ψ.base x ∈ V)
include hb hxV in
Lean source · statement
lemma wedge_local {W : X.Opens} (w : ⋀[Γ(X, W)]^n Γ(F ψ E, W)) (hx : x ∈ W) :
    ∃ (W' : X.Opens) (i : W' ≤ W) (j : W' ≤ ψ ⁻¹ᵁ V), x ∈ W' ∧ ∃ r : Γ(X, W'),
      preMap n (F ψ E) (homOfLE i) w = r • exteriorPower.ιMulti _ n (gsec ψ n E e j)
lemma

α_locallySurjective

L557 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.α_locallySurjective
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
lemma α_locallySurjective (hE : IsLocallyFreeOfRank n E) (W : X.Opens) (c : Γ(det n (F ψ E), W))
    (x : X) (hx : x ∈ W) :
    ∃ (V : X.Opens) (i : V ≤ W), x ∈ V ∧ (det n (F ψ E)).presheaf.map (homOfLE i).op c ∈
      Set.range ((α ψ n E).app V)
theorem

nonempty_iso

L581 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_nonempty_pullback_det_iso_det_pullback.AlgebraicGeometry.Scheme.Modules.DetPullback.nonempty_iso
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace DetPullback
variable {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) (E : Y.Modules)
Lean source · statement
theorem nonempty_iso (hE : IsLocallyFreeOfRank n E) :
    Nonempty ((Modules.pullback ψ).obj (det n E) ≅ det n (F ψ E))
theorem

nonempty_pullback_det_iso_det_pullback

L595 ↗
AlgebraicGeometry.Scheme.Modules.nonempty_pullback_det_iso_det_pullback
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_nonempty_pullback_det_iso_det_pullback
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.nonempty_pullback_det_iso_det_pullback
    {X Y : Scheme.{u}} (ψ : X ⟶ Y) (n : ℕ) {E : Y.Modules} (hE : Scheme.Modules.IsLocallyFreeOfRank
      n E) :
    Nonempty ((Scheme.Modules.pullback ψ).obj (Scheme.Modules.det n E) ≅
      Scheme.Modules.det n ((Scheme.Modules.pullback ψ).obj E))

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