NYLL
Module

Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
13 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Invertible exists Unique pullback map eq of is Integrally Closed stalk

Imports18
Imported by2

Declarations

lemma

map_map

L101 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.NormalS2.map_map
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
attribute [-instance]
  pullback_monoidal
  isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  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.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace NormalS2
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
lemma map_map {M : X.Modules} {A B C : X.Opens} (i : B ⟶ A) (j : C ⟶ B) (s : Γ(M, A)) :
    M.presheaf.map j.op (M.presheaf.map i.op s) = M.presheaf.map (j ≫ i).op s
lemma

map_congr

L106 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.NormalS2.map_congr
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
attribute [-instance]
  pullback_monoidal
  isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  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.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace NormalS2
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
lemma map_congr {M : X.Modules} {A B : X.Opens} (i j : B ⟶ A) (s : Γ(M, A)) :
    M.presheaf.map i.op s = M.presheaf.map j.op s
lemma

map_id'

L110 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.NormalS2.map_id'
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
attribute [-instance]
  pullback_monoidal
  isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  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.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace NormalS2
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
lemma map_id' {M : X.Modules} {A : X.Opens} (i : A ⟶ A) (s : Γ(M, A)) : M.presheaf.map i.op s = s
lemma

bijective_map_of_eq

L115 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.NormalS2.bijective_map_of_eq
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
attribute [-instance]
  pullback_monoidal
  isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  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.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace NormalS2
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
lemma bijective_map_of_eq {M : X.Modules} {A B : X.Opens} (h : B = A) :
    Function.Bijective (M.presheaf.map (homOfLE h.le).op)
def

shf

L125 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.NormalS2.shf
Documentation

The underlying sheaf of abelian groups of a sheaf of modules.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
attribute [-instance]
  pullback_monoidal
  isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  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.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace NormalS2
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · statement
def shf (M : X.Modules) : TopCat.Sheaf Ab X.carrier
lemma

bijective_smul_of_isFrameOn

L127 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.NormalS2.bijective_smul_of_isFrameOn
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
attribute [-instance]
  pullback_monoidal
  isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  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.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace NormalS2
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
Lean source · full declaration
lemma bijective_smul_of_isFrameOn {M : X.Modules} {A : X.Opens} {e : Γ(M, A)} (he : IsFrameOn e A) :
    Function.Bijective fun g : Γ(X, A) => g • e := by
  have hb := he le_rfl le_rfl
  have hid : (fun g : Γ(X, A) => g • M.presheaf.map (homOfLE le_rfl).op e) = fun g => g • e :=
    funext fun g => by rw [map_id']
  rwa [hid] at hb
lemma

preimage_inf_eq

L138 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.NormalS2.preimage_inf_eq
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
attribute [-instance]
  pullback_monoidal
  isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  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.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace NormalS2
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section InsideU
variable (U : X.Opens) {L : X.Modules}
Lean source · statement
lemma preimage_inf_eq (W : X.Opens) : U.ι ⁻¹ᵁ (W ⊓ U) = U.ι ⁻¹ᵁ W
lemma

bijective_pl_of_frame

L144 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.NormalS2.bijective_pl_of_frame
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
attribute [-instance]
  pullback_monoidal
  isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  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.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace NormalS2
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section InsideU
variable (U : X.Opens) {L : X.Modules}
Lean source · full declaration
lemma bijective_pl_of_frame {O W : X.Opens} (e : Γ(L, O)) (he : IsFrameOn e O) (hWO : W ≤ O) (hWU :
  W ≤ U) :
    Function.Bijective (fun s : Γ(L, W) => pullbackLocalSection U.ι s) := by
  have heW : IsFrameOn (L.presheaf.map (homOfLE hWO).op e) W := (he.map _).mono hWO
  have heι : IsFrameOn (pullbackLocalSection U.ι (L.presheaf.map (homOfLE hWO).op e)) (U.ι ⁻¹ᵁ W) :=
    heW.pullbackLocalSection U.ι
  have hB1 := bijective_smul_of_isFrameOn heW
  have hB2 := bijective_smul_of_isFrameOn heι
  have hι : Function.Bijective (U.ι.app W) := by
    have := U.ι.isIso_app W (by rw [Scheme.Opens.opensRange_ι]; exact hWU)
    exact ConcreteCategory.bijective_of_isIso (U.ι.app W)
  have hcomp : (fun s : Γ(L, W) => pullbackLocalSection U.ι s) ∘
      (fun g : Γ(X, W) => g • L.presheaf.map (homOfLE hWO).op e) =
      (fun h : Γ(U, U.ι ⁻¹ᵁ W) => h • pullbackLocalSection U.ι (L.presheaf.map (homOfLE hWO).op e))
        ∘
        (fun g => U.ι.app W g) := by
    funext g
    simp only [Function.comp_apply, pullbackLocalSection_smul]
  rw [← Function.Bijective.of_comp_iff _ hB1, hcomp]
  exact hB2.comp hι
lemma

injective_pl

L165 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.NormalS2.injective_pl
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
attribute [-instance]
  pullback_monoidal
  isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  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.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace NormalS2
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section InsideU
variable (U : X.Opens) {L : X.Modules}
Lean source · full declaration
lemma injective_pl (O : X → X.Opens) (e : ∀ x, Γ(L, O x)) (hxO : ∀ x, x ∈ O x)
    (he : ∀ x, IsFrameOn (e x) (O x)) (W : X.Opens) (hWU : W ≤ U) :
    Function.Injective (fun s : Γ(L, W) => pullbackLocalSection U.ι s) := by
  intro s t hst
  rw [← sub_eq_zero] at hst ⊢
  change pullbackLocalSection U.ι s - pullbackLocalSection U.ι t = 0 at hst
  rw [← pullbackLocalSection_sub] at hst
  set d := s - t
  have hcov : W ≤ ⨆ x : X, W ⊓ O x := fun y hy => Opens.mem_iSup.mpr ⟨y, ⟨hy, hxO y⟩⟩
  apply (shf L).eq_of_locally_eq' (fun x : X => W ⊓ O x) W (fun x => homOfLE inf_le_left) hcov
  intro x
  change L.presheaf.map (homOfLE (inf_le_left : W ⊓ O x ≤ W)).op d =
    L.presheaf.map (homOfLE (inf_le_left : W ⊓ O x ≤ W)).op 0
  rw [map_zero]
  apply (bijective_pl_of_frame U (e x) (he x) (inf_le_right : W ⊓ O x ≤ O x) (inf_le_left.trans
    hWU)).1
  change pullbackLocalSection U.ι _ = pullbackLocalSection U.ι _
  rw [pullbackLocalSection_zero, ← map_homOfLE_pullbackLocalSection, hst, map_zero]
lemma

bijective_pl

L184 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.NormalS2.bijective_pl
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
attribute [-instance]
  pullback_monoidal
  isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  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.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace NormalS2
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section InsideU
variable (U : X.Opens) {L : X.Modules}
Lean source · full declaration
lemma bijective_pl (hL : IsInvertible L) (W : X.Opens) (hWU : W ≤ U) :
    Function.Bijective (fun s : Γ(L, W) => pullbackLocalSection U.ι s) := by
  have hfr : ∀ x : X, ∃ (O : X.Opens) (e : Γ(L, O)), x ∈ O ∧ IsFrameOn e O := fun x => by
    obtain ⟨O, hxO, ⟨eO⟩⟩ := hL.exists_trivialization x
    obtain ⟨e, he⟩ := exists_isFrameOn_of_pullback_iso_unit O eO
    exact ⟨O, e, hxO, he⟩
  choose O e hxO he using hfr
  refine ⟨injective_pl U O e hxO he W hWU, ?_⟩
  intro τ
  have hloc : ∀ x : X, ∃ t : Γ(L, W ⊓ O x), pullbackLocalSection U.ι t =
      ((Modules.pullback U.ι).obj L).presheaf.map
        (homOfLE (U.ι.preimage_mono (inf_le_left : W ⊓ O x ≤ W))).op τ :=
    fun x => (bijective_pl_of_frame U (e x) (he x) (inf_le_right : W ⊓ O x ≤ O x)
      (inf_le_left.trans hWU)).2 _
  choose t ht using hloc
  have hcompat : TopCat.Presheaf.IsCompatible L.presheaf (fun x : X => W ⊓ O x) t := by
    intro x y
    apply injective_pl U O e hxO he ((W ⊓ O x) ⊓ (W ⊓ O y)) (inf_le_left.trans (inf_le_left.trans
      hWU))
    change pullbackLocalSection U.ι (L.presheaf.map _ (t x)) = pullbackLocalSection U.ι
      (L.presheaf.map _ (t y))
    rw [map_congr _ (homOfLE (inf_le_left : (W ⊓ O x) ⊓ (W ⊓ O y) ≤ W ⊓ O x)) (t x),
      map_congr _ (homOfLE (inf_le_right : (W ⊓ O x) ⊓ (W ⊓ O y) ≤ W ⊓ O y)) (t y),
      ← map_homOfLE_pullbackLocalSection, ← map_homOfLE_pullbackLocalSection, ht, ht, map_map,
        map_map]
    rfl
  have hcov : W ≤ ⨆ x : X, W ⊓ O x := fun y hy => Opens.mem_iSup.mpr ⟨y, ⟨hy, hxO y⟩⟩
  obtain ⟨s, hs, -⟩ := (shf L).existsUnique_gluing' (fun x : X => W ⊓ O x) W (fun x => homOfLE
    inf_le_left)
    hcov t hcompat
  refine ⟨s, ?_⟩
  have hcovι : U.ι ⁻¹ᵁ W ≤ ⨆ x : X, U.ι ⁻¹ᵁ (W ⊓ O x) :=
    fun y hy => Opens.mem_iSup.mpr ⟨U.ι.base y, ⟨hy, hxO _⟩⟩
  apply (shf ((Modules.pullback U.ι).obj L)).eq_of_locally_eq' (fun x : X => U.ι ⁻¹ᵁ (W ⊓ O x))
    (U.ι ⁻¹ᵁ W)
    (fun x => homOfLE (U.ι.preimage_mono inf_le_left)) hcovι
  intro x
  have hsx : L.presheaf.map (homOfLE (inf_le_left : W ⊓ O x ≤ W)).op
      (show Γ(L, W) from s) = t x := hs x
  exact (map_homOfLE_pullbackLocalSection (L := L) U.ι
    (inf_le_left : W ⊓ O x ≤ W) (show Γ(L, W) from s)).trans
      ((congrArg (fun z : Γ(L, W ⊓ O x) => pullbackLocalSection U.ι z) hsx).trans (ht x))
theorem

isIso_unit

L236 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.NormalS2.isIso_unit
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
attribute [-instance]
  pullback_monoidal
  isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  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.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace NormalS2
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Unit
variable [IsLocallyNoetherian X]
  (hX : ∀ x : X, IsDomain (X.presheaf.stalk x) ∧ IsIntegrallyClosed (X.presheaf.stalk x))
  (U : X.Opens) (hU : ∀ x : X, ringKrullDim (X.presheaf.stalk x) ≤ 1 → x ∈ U)
include hX hU in
Lean source · statement
theorem isIso_unit {L : X.Modules} (hL : IsInvertible L) :
    IsIso ((pullbackPushforwardAdjunction U.ι).unit.app L)
theorem

main

L272 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk.AlgebraicGeometry.Scheme.Modules.NormalS2.main
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
attribute [-instance]
  pullback_monoidal
  isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  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.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace NormalS2
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}
section Main
variable [IsLocallyNoetherian X]
  (hX : ∀ x : X, IsDomain (X.presheaf.stalk x) ∧ IsIntegrallyClosed (X.presheaf.stalk x))
  (U : X.Opens) (hU : ∀ x : X, ringKrullDim (X.presheaf.stalk x) ≤ 1 → x ∈ U)
  {L L' : X.Modules} (hL : IsInvertible L) (hL' : IsInvertible L')
  (φ : (Modules.pullback U.ι).obj L ⟶ (Modules.pullback U.ι).obj L')
include hX hU hL hL' in
Lean source · statement
theorem main :
    (∃! ψ : L ⟶ L', (Modules.pullback U.ι).map ψ = φ) ∧
      ∀ ψ : L ⟶ L', (Modules.pullback U.ι).map ψ = φ → IsIso φ → IsIso ψ
theorem

existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk

L343 ↗
AlgebraicGeometry.Scheme.Modules.IsInvertible.existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicGeometry.Scheme.Modules.IsInvertible
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry _root_.Opposite _root_.TopologicalSpace
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs in
open Scheme_Modules_IsInvertible_existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk in
Lean source · statement
theorem existsUnique_pullback_map_eq_of_isIntegrallyClosed_stalk
    {X : Scheme.{u}} [IsLocallyNoetherian X]
    (hX : ∀ x : X, IsDomain (X.presheaf.stalk x) ∧ IsIntegrallyClosed (X.presheaf.stalk x))
    (U : X.Opens) (hU : ∀ x : X, ringKrullDim (X.presheaf.stalk x) ≤ 1 → x ∈ U)
    {L L' : X.Modules} (hL : Scheme.Modules.IsInvertible L) (hL' : Scheme.Modules.IsInvertible L')
    (φ : (Scheme.Modules.pullback U.ι).obj L ⟶ (Scheme.Modules.pullback U.ι).obj L') :
    (∃! ψ : L ⟶ L', (Scheme.Modules.pullback U.ι).map ψ = φ) ∧
      ∀ ψ : L ⟶ L', (Scheme.Modules.pullback U.ι).map ψ = φ → IsIso φ → IsIso ψ

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