NYLL
Module

Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
31 declarations indexed from sourceView source ↗

Module documentation

Determinant sections detect degeneration

A section of the dual determinant vanishes precisely where the pulled-back map is not invertible.

Imports14
Imported by2

Declarations

abbrev

res

L72 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.res
Documentation

Restriction of a module section to a smaller open subset.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
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

L77 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.res_res
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
Lean source · statement
lemma res_res {Z : Scheme.{u}} (M : Z.Modules) {W₁ W₂ W₃ : Z.Opens} (h₂₁ : W₂ ≤ W₁) (h₃₂ : W₃ ≤ W₂)
    (s : Γ(M, W₁)) : res M h₃₂ (res M h₂₁ s) = res M (h₃₂.trans h₂₁) s
lemma

res_self

L83 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.res_self
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
Lean source · statement
lemma res_self {Z : Scheme.{u}} (M : Z.Modules) {W : Z.Opens} (h : W ≤ W) (s : Γ(M, W)) : res M h s
  = s
lemma

res_eq_map

L89 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.res_eq_map
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
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

L93 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.res_smul
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
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_sum

L98 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.res_sum
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
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

L102 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.app_res
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
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

localBasis_of_le

L109 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.localBasis_of_le
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
Lean source · statement
lemma localBasis_of_le {X : Scheme.{u}} {M : X.Modules} {n : ℕ} {V U : X.Opens} (hUV : U ≤ V)
    (e : Fin n → Γ(M, V))
    (he : ∀ (W : X.Opens) (hW : W ≤ V), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
      ∀ i, b i = M.presheaf.map (homOfLE hW).op (e i)) :
    ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(M, W),
      ∀ i, b i = M.presheaf.map (homOfLE hW).op (M.presheaf.map (homOfLE hUV).op (e i))
lemma

pt_eq

L122 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.pt_eq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
Lean source · statement
lemma pt_eq (q : Spec (CommRingCat.of K)) : q = IsLocalRing.closedPoint K
lemma

le_of_mem

L125 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.le_of_mem
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
Lean source · statement
lemma le_of_mem {W₁ W₂ : (Spec (CommRingCat.of K)).Opens} (h : IsLocalRing.closedPoint K ∈ W₂) : W₁
  ≤ W₂
lemma

preimage_le

L132 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.preimage_le
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
include hs in
Lean source · statement
lemma preimage_le (W : X.Opens) : s ⁻¹ᵁ W ≤ s ⁻¹ᵁ (W ⊓ U)
lemma

opens_cases

L138 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.opens_cases
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
include hs in
Lean source · statement
lemma opens_cases (W : (Spec (CommRingCat.of K)).Opens) : W = s ⁻¹ᵁ U ∨ W = ⊥
lemma

isIso_iff_isIso_app

L147 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.isIso_iff_isIso_app
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
include hs in
Lean source · statement
lemma isIso_iff_isIso_app {A B : (Spec (CommRingCat.of K)).Modules} (g : A ⟶ B) :
    IsIso g ↔ IsIso (g.app (s ⁻¹ᵁ U))
lemma

isUnit_iff_ne_zero'

L157 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.isUnit_iff_ne_zero'
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
include hs in
Lean source · statement
lemma isUnit_iff_ne_zero' (z : (Spec (CommRingCat.of K)).presheaf.obj (op (s ⁻¹ᵁ U))) : IsUnit z ↔
  z ≠ 0
def

eta

L170 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.eta
Documentation

The local section obtained from the unit of the pullback-pushforward adjunction.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
Lean source · statement
def eta (Q : X.Modules) (V : X.Opens) (m : Γ(Q, V)) :
    Γ((Scheme.Modules.pullback s).obj Q, s ⁻¹ᵁ V)
lemma

eta_def

L174 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.eta_def
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
Lean source · statement
lemma eta_def (Q : X.Modules) (V : X.Opens) (m : Γ(Q, V)) :
    eta s Q V m = ((Scheme.Modules.pullbackPushforwardAdjunction s).unit.app Q).app V m
lemma

eta_sum

L177 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.eta_sum
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
Lean source · statement
lemma eta_sum (Q : X.Modules) (V : X.Opens) {ι : Type*} (T : Finset ι) (f : ι → Γ(Q, V)) :
    eta s Q V (∑ t ∈ T, f t) = ∑ t ∈ T, eta s Q V (f t)
lemma

eta_smul

L181 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.eta_smul
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
Lean source · statement
lemma eta_smul (Q : X.Modules) (V : X.Opens) (r : Γ(X, V)) (m : Γ(Q, V)) :
    eta s Q V (r • m) = s.app V r • eta s Q V m
lemma

pullback_map_app_eta

L185 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.pullback_map_app_eta
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
Lean source · statement
lemma pullback_map_app_eta {Q Q' : X.Modules} (g : Q ⟶ Q') (V : X.Opens) (m : Γ(Q, V)) :
    ((Scheme.Modules.pullback s).map g).app (s ⁻¹ᵁ V) (eta s Q V m) = eta s Q' V (g.app V m)
lemma

map_app_unitSection

L193 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.map_app_unitSection
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
Lean source · statement
lemma map_app_unitSection {N : (Spec (CommRingCat.of K)).Modules}
    (g : 𝟙_ X.Modules ⟶ (Scheme.Modules.pushforward s).obj N) {V V' : X.Opens} (h : V' ≤ V) :
    N.presheaf.map (homOfLE (s.preimage_mono h)).op (g.app V (Scheme.Modules.unitSection V)) =
      g.app V' (Scheme.Modules.unitSection V')
theorem

pullbackSection_eq_zero_iff

L206 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.pullbackSection_eq_zero_iff
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
include hs in
Lean source · statement
theorem pullbackSection_eq_zero_iff {Q : X.Modules} (κ : 𝟙_ X.Modules ⟶ Q) :
    Scheme.Modules.pullbackSection s κ = 0 ↔ eta s Q U (κ.app U (Scheme.Modules.unitSection U)) = 0
theorem

isIso_pullback_map_iff

L281 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.isIso_pullback_map_iff
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
section rhs
variable {n : ℕ} {E F : X.Modules} (φ : E ⟶ F)
  (e : Fin n → Γ(E, U))
  (he : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(E, W),
    ∀ i, b i = E.presheaf.map (homOfLE hW).op (e i))
  (f : Fin n → Γ(F, U))
  (hf : ∀ (W : X.Opens) (hW : W ≤ U), ∃ b : Module.Basis (Fin n) Γ(X, W) Γ(F, W),
    ∀ i, b i = F.presheaf.map (homOfLE hW).op (f i))
  (a : Matrix (Fin n) (Fin n) Γ(X, U)) (ha : ∀ j, φ.app U (e j) = ∑ i, a i j • f i)
include hs he hf ha in
Lean source · statement
theorem isIso_pullback_map_iff : IsIso ((Scheme.Modules.pullback s).map φ) ↔ IsUnit (s.app U a.det)
abbrev

wedge

L327 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.wedge
Documentation

The determinant section formed by the exterior product of local sections.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
Lean source · statement
abbrev wedge (n : ℕ) (M : X.Modules) (U : X.Opens) (m : Fin n → Γ(M, U)) :
    Γ(Scheme.Modules.det n M, U)
lemma

isUnit_of_isFrameOn

L334 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.isUnit_of_isFrameOn
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
Lean source · full declaration
lemma isUnit_of_isFrameOn {u : Γ(𝟙_ X.Modules, U)} (hu : Scheme.Modules.IsFrameOn u U) :
    IsUnit (show Γ(X, U) from u) := by
  obtain ⟨g, hg⟩ := (hu le_rfl le_rfl).2 (Scheme.Modules.unitSection U)
  change g • res (𝟙_ X.Modules) le_rfl u = Scheme.Modules.unitSection U at hg
  rw [res_self] at hg
  exact IsUnit.of_mul_eq_one_right g hg
def

mulSec

L344 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.mulSec
Documentation

Multiplication by a section as a morphism on an open subscheme.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
section dualOne
Lean source · statement
def mulSec (A : X.Modules) (U' : X.Opens) (ω : Γ(A, U')) :
    (𝟙_ X.Modules).restrict U'.ι ⟶ A.restrict U'.ι
lemma

mulSec_app

L373 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.mulSec_app
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
section dualOne
Lean source · statement
lemma mulSec_app (A : X.Modules) (U' : X.Opens) (ω : Γ(A, U')) (W : (U' : Scheme.{u}).Opens)
    (r : Γ(X, U'.ι ''ᵁ W)) :
    (mulSec A U' ω).app W r = r • res A (U'.ι_image_le W) ω
lemma

isIso_mulSec

L379 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.isIso_mulSec
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
section dualOne
variable {A : X.Modules} {U' : X.Opens} {ω : Γ(A, U')}
Lean source · statement
lemma isIso_mulSec (hω : Scheme.Modules.IsFrameOn ω U') : IsIso (mulSec A U' ω)
def

dualOne

L384 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.dualOne
Documentation

The dual section taking a chosen frame to the unit section.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
section dualOne
variable {A : X.Modules} {U' : X.Opens} {ω : Γ(A, U')}
Lean source · statement
def dualOne (hω : Scheme.Modules.IsFrameOn ω U') : Γ(Scheme.Modules.dual A, U')
lemma

ihomEval_dualOne

L388 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.ihomEval_dualOne
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
section dualOne
variable {A : X.Modules} {U' : X.Opens} {ω : Γ(A, U')}
Lean source · statement
lemma ihomEval_dualOne (hω : Scheme.Modules.IsFrameOn ω U') :
    Scheme.Modules.ihomEval A (𝟙_ X.Modules) U' ω (dualOne hω) = Scheme.Modules.unitSection U'
theorem

main

L418 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso.DetDegenKit.DetDegen.main
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace DetDegenKit
namespace DetDegen
variable {X : Scheme.{u}} {K : Type u} [Field K] (s : Spec (CommRingCat.of K) ⟶ X) {U : X.Opens}
  (hs : s.base (IsLocalRing.closedPoint K) ∈ U)
Lean source · statement
theorem main {n : ℕ} {E F : X.Modules}
    (hE : Scheme.Modules.IsLocallyFreeOfRank n E) (hF : Scheme.Modules.IsLocallyFreeOfRank n F)
    (φ : E ⟶ F) (ι : Scheme.Modules.det n F ≅ 𝟙_ X.Modules) :
    ∃ θ : 𝟙_ X.Modules ⟶ Scheme.Modules.dual (Scheme.Modules.det n E),
      ∀ (K : Type u) [Field K] (s : Spec (CommRingCat.of K) ⟶ X),
        Scheme.Modules.pullbackSection s θ = 0 ↔ ¬ IsIso ((Scheme.Modules.pullback s).map φ)
theorem

exists_pullbackSection_dual_det_eq_zero_iff_not_isIso

L529 ↗
AlgebraicGeometry.Scheme.Modules.exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
attribute [-instance] PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply PresheafOfModules.freeεIso_hom_app
  PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
Lean source · statement
theorem
  _root_.AlgebraicGeometry.Scheme.Modules.exists_pullbackSection_dual_det_eq_zero_iff_not_isIso
    {X : Scheme.{u}} {n : ℕ} {E F : X.Modules}
    (hE : Scheme.Modules.IsLocallyFreeOfRank n E) (hF : Scheme.Modules.IsLocallyFreeOfRank n F)
    (φ : E ⟶ F) (hdet : Nonempty (Scheme.Modules.det n F ≅ 𝟙_ X.Modules)) :
    ∃ θ : 𝟙_ X.Modules ⟶ Scheme.Modules.dual (Scheme.Modules.det n E),
      ∀ (K : Type u) [Field K] (s : Spec (CommRingCat.of K) ⟶ X),
        Scheme.Modules.pullbackSection s θ = 0 ↔ ¬ IsIso ((Scheme.Modules.pullback s).map φ)

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