Module

Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare

78 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules exists is Invertible pullback iso of milnor Square

Imports38

Mathlib.AlgebraicGeometry.AffineTransitionLimit
Lean.Elab.Command
Mathlib.Algebra.Category.Grp.Basic
Mathlib.Algebra.Category.Grp.Limits
Mathlib.Algebra.Category.ModuleCat.Sheaf
Mathlib.AlgebraicGeometry.Scheme
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.CategoryTheory.Category.Preorder
Mathlib.CategoryTheory.ConcreteCategory.Basic
Mathlib.CategoryTheory.ConcreteCategory.Forget
Mathlib.CategoryTheory.EqToHom
Mathlib.CategoryTheory.Functor.Basic
Mathlib.CategoryTheory.Functor.Category
Mathlib.CategoryTheory.Iso
Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Mathlib.CategoryTheory.Limits.Preserves.Basic
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Mathlib.CategoryTheory.NatIso
Mathlib.CategoryTheory.Opposites
Mathlib.CategoryTheory.Types.Basic
Mathlib.Geometry.RingedSpace.Basic
Mathlib.Topology.Category.TopCat.Opens
Mathlib.Topology.Maps.Basic
Mathlib.Topology.Sets.Opens
Mathlib.Topology.Sheaves.Sheaf
Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Mathlib.Tactic.Choose
Nyll.AlgebraicCurves.Geometry.Picard.Functor
Nyll.SchemeTheory.Modules.TensorSections
Nyll.SchemeTheory.Modules.PullbackLocalSection
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsFrameOn_pullbackLocalSection
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_of_isFrameOn_of_iSup_eq_top
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isInvertible_of_forall_exists_isFrameOn
Nyll.SchemeTheory.Modules.FrameFromTrivialization
Nyll.SchemeTheory.Modules.PullbackUnitComposition

Imported by2

lemma

map_app

L133 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.map_app

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}

Lean source · statement

lemma map_app {M N : X.Modules} (φ : M ⟶ N) {U V : X.Opens} (i : V ⟶ U) (s : Γ(M, U)) :
    N.presheaf.map i.op (φ.app U s) = φ.app V (M.presheaf.map i.op s)

lemma

map_map

L138 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.map_map

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}

Lean source · statement

lemma map_map {M : X.Modules} {U V V' : X.Opens} (i : V ⟶ U) (j : V' ⟶ V) (s : Γ(M, U)) :
    M.presheaf.map j.op (M.presheaf.map i.op s) = M.presheaf.map (j ≫ i).op s

lemma

map_congr

L143 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.map_congr

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}

Lean source · statement

lemma map_congr {M : X.Modules} {U V : X.Opens} (i j : V ⟶ U) (s : Γ(M, U)) :
    M.presheaf.map i.op s = M.presheaf.map j.op s

lemma

map_id'

L147 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.map_id'

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}

Lean source · statement

lemma map_id' {M : X.Modules} {U : X.Opens} (i : U ⟶ U) (s : Γ(M, U)) : M.presheaf.map i.op s = s

lemma

iso_hom_inv_app_apply

L152 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.iso_hom_inv_app_apply

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}

Lean source · statement

lemma iso_hom_inv_app_apply {M N : X.Modules} (e : M ≅ N) (U : X.Opens) (x : Γ(M, U)) :
    e.inv.app U (e.hom.app U x) = x

lemma

iso_inv_hom_app_apply

L158 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.iso_inv_hom_app_apply

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}

Lean source · statement

lemma iso_inv_hom_app_apply {M N : X.Modules} (e : M ≅ N) (U : X.Opens) (x : Γ(N, U)) :
    e.hom.app U (e.inv.app U x) = x

lemma

comp_app_apply

L164 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.comp_app_apply

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}

Lean source · statement

lemma comp_app_apply {M N K : X.Modules} (φ : M ⟶ N) (ψ : N ⟶ K) (U : X.Opens) (x : Γ(M, U)) :
    (φ ≫ ψ).app U x = ψ.app U (φ.app U x)

lemma

subsingleton_bot

L168 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.subsingleton_bot

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}

Lean source · statement

lemma subsingleton_bot (M : X.Modules) {U : X.Opens} (hU : U = ⊥) (s t : Γ(M, U)) : s = t

def

secFunctor

L175 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.secFunctor

Documentation

The functor taking a sheaf of modules to its sections on the specified open.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}

Lean source · statement

def secFunctor (U : X.Opens) : X.Modules ⥤ Type u

instance

(anonymous instance)

L180 ↗

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}

Lean source · statement

instance (U : X.Opens) : PreservesLimitsOfShape WalkingCospan (secFunctor (X := X) U)

lemma

secFunctor_map

L192 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.secFunctor_map

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}

Lean source · statement

lemma secFunctor_map {M N : X.Modules} (f : M ⟶ N) (U : X.Opens) (s : Γ(M, U)) :
    (secFunctor U).map f s = f.app U s

def

secIsLimit

L200 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.secIsLimit

Documentation

The pullback cone on sections obtained by preservation of the module-sheaf pullback.

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}
section FibreProduct
variable {A B C : X.Modules} (a : A ⟶ C) (b : B ⟶ C) (U : X.Opens)

Lean source · full declaration

def secIsLimit : IsLimit (PullbackCone.mk ((secFunctor U).map (pullback.fst a b))
    ((secFunctor U).map (pullback.snd a b))
    (by rw [← Functor.map_comp, ← Functor.map_comp, pullback.condition])) :=
  isLimitOfHasPullbackOfPreservesLimit (secFunctor U) a b

def

mkSec

L208 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.mkSec

Documentation

The section of the pullback sheaf induced by two sections with the same image.

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}
section FibreProduct
variable {A B C : X.Modules} (a : A ⟶ C) (b : B ⟶ C) (U : X.Opens)
variable {U}

Lean source · statement

def mkSec (s : Γ(A, U)) (t : Γ(B, U)) (h : a.app U s = b.app U t) : Γ(Limits.pullback a b, U)

lemma

fst_mkSec

L212 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.fst_mkSec

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}
section FibreProduct
variable {A B C : X.Modules} (a : A ⟶ C) (b : B ⟶ C) (U : X.Opens)
variable {U}

Lean source · statement

lemma fst_mkSec (s : Γ(A, U)) (t : Γ(B, U)) (h : a.app U s = b.app U t) :
    (pullback.fst a b).app U (mkSec a b s t h) = s

lemma

snd_mkSec

L218 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.snd_mkSec

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}
section FibreProduct
variable {A B C : X.Modules} (a : A ⟶ C) (b : B ⟶ C) (U : X.Opens)
variable {U}

Lean source · statement

lemma snd_mkSec (s : Γ(A, U)) (t : Γ(B, U)) (h : a.app U s = b.app U t) :
    (pullback.snd a b).app U (mkSec a b s t h) = t

lemma

sec_ext

L224 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.sec_ext

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}
section FibreProduct
variable {A B C : X.Modules} (a : A ⟶ C) (b : B ⟶ C) (U : X.Opens)
variable {U}

Lean source · statement

lemma sec_ext {x y : Γ(Limits.pullback a b, U)} (h₁ : (pullback.fst a b).app U x = (pullback.fst a
  b).app U y)
    (h₂ : (pullback.snd a b).app U x = (pullback.snd a b).app U y) : x = y

lemma

sec_condition

L231 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.sec_condition

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section General
variable {X : Scheme.{u}}
section FibreProduct
variable {A B C : X.Modules} (a : A ⟶ C) (b : B ⟶ C) (U : X.Opens)
variable {U}

Lean source · statement

lemma sec_condition (x : Γ(Limits.pullback a b, U)) :
    a.app U ((pullback.fst a b).app U x) = b.app U ((pullback.snd a b).app U x)

lemma

preimage_eq

L246 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.preimage_eq

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
include hsq in

Lean source · statement

lemma preimage_eq (U : W.Opens) : j₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ U) = j₁ ⁻¹ᵁ (i₁ ⁻¹ᵁ U)

def

tr

L251 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.tr

Documentation

Transport sections along the equality between the two inverse images in the commutative square.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

def tr (M : Z.Modules) (U : W.Opens) (x : Γ(M, j₁ ⁻¹ᵁ (i₁ ⁻¹ᵁ U))) : Γ(M, j₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ U))

lemma

tr_def

L254 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.tr_def

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

lemma tr_def (M : Z.Modules) (U : W.Opens) (x : Γ(M, j₁ ⁻¹ᵁ (i₁ ⁻¹ᵁ U))) :
    tr hsq M U x = M.presheaf.map (eqToHom (preimage_eq hsq U)).op x

def

K

L258 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.K

Documentation

The common pushed-forward module on the intersection used to form the gluing pullback.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

def K (i₂ : V₂ ⟶ W) (j₂ : Z ⟶ V₂) (L₂ : V₂.Modules) : W.Modules

def

aMap

L262 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.aMap

Documentation

The first restriction map to the common module, followed by the chosen gluing isomorphism.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

def aMap : (pushforward i₁).obj L₁ ⟶ K i₂ j₂ L₂

def

bMap

L268 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.bMap

Documentation

The second restriction map to the common module on the intersection.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

def bMap : (pushforward i₂).obj L₂ ⟶ K i₂ j₂ L₂

lemma

aMap_app

L272 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.aMap_app

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

lemma aMap_app (U : W.Opens) (s : Γ(L₁, i₁ ⁻¹ᵁ U)) :
    (aMap hsq L₁ L₂ φ).app U s = tr hsq _ U (φ.hom.app _ (pullbackLocalSection j₁ s))

lemma

bMap_app

L277 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.bMap_app

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

lemma bMap_app (U : W.Opens) (s : Γ(L₂, i₂ ⁻¹ᵁ U)) :
    (bMap L₂ : (pushforward i₂).obj L₂ ⟶ K i₂ j₂ L₂).app U s = pullbackLocalSection j₂ s

def

glued

L282 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.glued

Documentation

The module sheaf obtained as the pullback of the two restriction maps.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

def glued : W.Modules

def

pr₁

L285 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.pr₁

Documentation

The projection of the glued module to the pushforward from the first piece.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

def pr₁ : glued hsq L₁ L₂ φ ⟶ (pushforward i₁).obj L₁

def

pr₂

L288 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.pr₂

Documentation

The projection of the glued module to the pushforward from the second piece.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

def pr₂ : glued hsq L₁ L₂ φ ⟶ (pushforward i₂).obj L₂

def

c₁

L293 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.c₁

Documentation

The first component of a section of the glued module.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {hsq L₁ L₂ φ}

Lean source · statement

def c₁ {U : W.Opens} (s : Γ(glued hsq L₁ L₂ φ, U)) : Γ(L₁, i₁ ⁻¹ᵁ U)

def

c₂

L296 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.c₂

Documentation

The second component of a section of the glued module.

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {hsq L₁ L₂ φ}

Lean source · statement

def c₂ {U : W.Opens} (s : Γ(glued hsq L₁ L₂ φ, U)) : Γ(L₂, i₂ ⁻¹ᵁ U)

lemma

c₁_def

L298 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.c₁_def

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {hsq L₁ L₂ φ}

Lean source · statement

lemma c₁_def {U : W.Opens} (s : Γ(glued hsq L₁ L₂ φ, U)) : c₁ s = (pr₁ hsq L₁ L₂ φ).app U s

lemma

c₂_def

L299 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.c₂_def

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {hsq L₁ L₂ φ}

Lean source · statement

lemma c₂_def {U : W.Opens} (s : Γ(glued hsq L₁ L₂ φ, U)) : c₂ s = (pr₂ hsq L₁ L₂ φ).app U s

lemma

cond

L301 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.cond

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {hsq L₁ L₂ φ}

Lean source · statement

lemma cond {U : W.Opens} (s : Γ(glued hsq L₁ L₂ φ, U)) :
    tr hsq _ U (φ.hom.app _ (pullbackLocalSection j₁ (c₁ s))) = pullbackLocalSection j₂ (c₂ s)

def

mk

L308 ↗

AlgebraicGeometry.Scheme.Modules.MilnorPatch.mk

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {hsq L₁ L₂ φ}

Lean source · statement

def _root_.AlgebraicGeometry.Scheme.Modules.MilnorPatch.mk {U : W.Opens} (s₁ : Γ(L₁, i₁ ⁻¹ᵁ
  U)) (s₂ : Γ(L₂, i₂ ⁻¹ᵁ U))
    (h : tr hsq _ U (φ.hom.app _ (pullbackLocalSection j₁ s₁)) = pullbackLocalSection j₂ s₂) :
    Γ(glued hsq L₁ L₂ φ, U)

lemma

c₁_mk

L316 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.c₁_mk

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {hsq L₁ L₂ φ}

Lean source · statement

lemma c₁_mk {U : W.Opens} (s₁ : Γ(L₁, i₁ ⁻¹ᵁ U)) (s₂ : Γ(L₂, i₂ ⁻¹ᵁ U))
    (h : tr hsq _ U (φ.hom.app _ (pullbackLocalSection j₁ s₁)) = pullbackLocalSection j₂ s₂) :
    c₁ (mk s₁ s₂ h) = s₁

lemma

c₂_mk

L321 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.c₂_mk

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {hsq L₁ L₂ φ}

Lean source · statement

lemma c₂_mk {U : W.Opens} (s₁ : Γ(L₁, i₁ ⁻¹ᵁ U)) (s₂ : Γ(L₂, i₂ ⁻¹ᵁ U))
    (h : tr hsq _ U (φ.hom.app _ (pullbackLocalSection j₁ s₁)) = pullbackLocalSection j₂ s₂) :
    c₂ (mk s₁ s₂ h) = s₂

lemma

ext

L326 ↗

AlgebraicGeometry.Scheme.Modules.MilnorPatch.ext

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {hsq L₁ L₂ φ}

Lean source · statement

lemma _root_.AlgebraicGeometry.Scheme.Modules.MilnorPatch.ext {U : W.Opens} {s t : Γ(glued
  hsq L₁ L₂ φ, U)} (h₁ : c₁ s = c₁ t) (h₂ : c₂ s = c₂ t) : s = t

lemma

c₁_map

L332 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.c₁_map

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {hsq L₁ L₂ φ}

Lean source · statement

lemma c₁_map {U V : W.Opens} (ι : V ⟶ U) (s : Γ(glued hsq L₁ L₂ φ, U)) :
    c₁ ((glued hsq L₁ L₂ φ).presheaf.map ι.op s) = L₁.presheaf.map ((Opens.map i₁.base).map ι).op
      (c₁ s)

lemma

c₂_map

L338 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.c₂_map

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {hsq L₁ L₂ φ}

Lean source · statement

lemma c₂_map {U V : W.Opens} (ι : V ⟶ U) (s : Γ(glued hsq L₁ L₂ φ, U)) :
    c₂ ((glued hsq L₁ L₂ φ).presheaf.map ι.op s) = L₂.presheaf.map ((Opens.map i₂.base).map ι).op
      (c₂ s)

lemma

c₁_smul

L344 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.c₁_smul

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {hsq L₁ L₂ φ}

Lean source · statement

lemma c₁_smul {U : W.Opens} (r : Γ(W, U)) (s : Γ(glued hsq L₁ L₂ φ, U)) : c₁ (r • s) = i₁.app U r •
  c₁ s

lemma

c₂_smul

L349 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.c₂_smul

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Glue
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {hsq L₁ L₂ φ}

Lean source · statement

lemma c₂_smul {U : W.Opens} (r : Γ(W, U)) (s : Γ(glued hsq L₁ L₂ φ, U)) : c₂ (r • s) = i₂.app U r •
  c₂ s

lemma

subsingleton_bot_ring

L360 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.subsingleton_bot_ring

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Frames
variable {X Y : Scheme.{u}}

Lean source · statement

lemma subsingleton_bot_ring {U : X.Opens} (hU : U = ⊥) (f g : Γ(X, U)) : f = g

lemma

isFrameOn_of_eq_bot

L366 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.isFrameOn_of_eq_bot

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Frames
variable {X Y : Scheme.{u}}

Lean source · statement

lemma isFrameOn_of_eq_bot {M : X.Modules} {U : X.Opens} (hU : U = ⊥) (s : Γ(M, U)) (V : X.Opens) :
    IsFrameOn s V

lemma

bijective_self

L372 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn.bijective_self

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Frames
variable {X Y : Scheme.{u}}

Lean source · full declaration

lemma _root_.AlgebraicGeometry.Scheme.Modules.IsFrameOn.bijective_self {M : X.Modules} {U :
  X.Opens} {s : Γ(M, U)} (h : IsFrameOn s U) :
    Function.Bijective fun g : Γ(X, U) => g • s := by
  have hb := h le_rfl le_rfl
  rwa [map_id'] at hb

lemma

exists_isUnit_smul_eq

L395 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn.exists_isUnit_smul_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_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Frames
variable {X Y : Scheme.{u}}

Lean source · statement

lemma _root_.AlgebraicGeometry.Scheme.Modules.IsFrameOn.exists_isUnit_smul_eq {M :
  X.Modules} {U : X.Opens} {s s' : Γ(M, U)} (hs : IsFrameOn s U)
    (hs' : IsFrameOn s' U) : ∃ u : Γ(X, U), IsUnit u ∧ s' = u • s

lemma

unit_smul

L425 ↗

AlgebraicGeometry.Scheme.Modules.IsFrameOn.unit_smul

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Frames
variable {X Y : Scheme.{u}}

Lean source · statement

lemma _root_.AlgebraicGeometry.Scheme.Modules.IsFrameOn.unit_smul {M : X.Modules} {U V :
  X.Opens} {s : Γ(M, U)} (hs : IsFrameOn s V) {u : Γ(X, U)}
    (hu : IsUnit u) : IsFrameOn (u • s) V

lemma

app_apply_map

L464 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.app_apply_map

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Frames
variable {X Y : Scheme.{u}}

Lean source · statement

lemma app_apply_map (f : X ⟶ Y) {U V : Y.Opens} (e : V ≤ U) (s : Γ(Y, U)) :
    f.app V (Y.presheaf.map (homOfLE e).op s) =
      X.presheaf.map (homOfLE (f.preimage_mono e)).op (f.app U s)

lemma

exists_preimage_eq

L472 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.exists_preimage_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_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Frames
variable {X Y : Scheme.{u}}

Lean source · statement

lemma exists_preimage_eq (f : X ⟶ Y) [IsClosedImmersion f] (O : X.Opens) :
    ∃ U : Y.Opens, f ⁻¹ᵁ U = O ∧ ∀ y : Y, y ∉ Set.range f.base → y ∈ U

lemma

preimage_inf_compl_range_eq_bot

L488 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.preimage_inf_compl_range_eq_bot

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Frames
variable {X Y : Scheme.{u}}

Lean source · statement

lemma preimage_inf_compl_range_eq_bot (f : X ⟶ Y) [IsClosedImmersion f] (O : Y.Opens) :
    f ⁻¹ᵁ (O ⊓ ⟨(Set.range f.base)ᶜ, (IsClosedImmersion.isClosedEmbedding
      f).isClosed_range.isOpen_compl⟩) = ⊥

lemma

exists_isFrameOn_preimage

L498 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.exists_isFrameOn_preimage

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Frames
variable {X Y : Scheme.{u}}

Lean source · statement

lemma exists_isFrameOn_preimage (f : X ⟶ Y) [IsClosedImmersion f] {L : X.Modules} (hL :
  IsInvertible L) (y : Y) :
    ∃ U : Y.Opens, y ∈ U ∧ ∃ e : Γ(L, f ⁻¹ᵁ U), IsFrameOn e (f ⁻¹ᵁ U)

lemma

exists_unit_lift

L511 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.exists_unit_lift

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Frames
variable {X Y : Scheme.{u}}

Lean source · statement

lemma exists_unit_lift (f : X ⟶ Y) [IsClosedImmersion f] {O : Y.Opens} {y : Y} (hy : y ∈ O)
    (u : Γ(X, f ⁻¹ᵁ O)) (hu : IsUnit u) :
    ∃ (O' : Y.Opens) (hO' : O' ≤ O), y ∈ O' ∧ ∃ a : Γ(Y, O'), IsUnit a ∧
      f.app O' a = X.presheaf.map (homOfLE (f.preimage_mono hO')).op u

lemma

hom_ext_of_frames

L541 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.hom_ext_of_frames

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Frames
variable {X Y : Scheme.{u}}

Lean source · statement

lemma hom_ext_of_frames {M N : X.Modules} {f g : M ⟶ N} {ι : Type*} (𝒱 : ι → X.Opens) (hcov : ⨆ i,
  𝒱 i = ⊤)
    (p : ∀ i, Γ(M, 𝒱 i)) (hp : ∀ i, IsFrameOn (p i) (𝒱 i)) (h : ∀ i, f.app _ (p i) = g.app _ (p i))
      :
    f = g

def

trFun

L575 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.trFun

Documentation

Transport regular functions along the equality of inverse images in the commutative square.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Matched
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) {L₁ : V₁.Modules} (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

def trFun (U : W.Opens) (g : Γ(Z, j₁ ⁻¹ᵁ (i₁ ⁻¹ᵁ U))) : Γ(Z, j₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ U))

lemma

trFun_def

L578 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.trFun_def

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Matched
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) {L₁ : V₁.Modules} (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

lemma trFun_def (U : W.Opens) (g : Γ(Z, j₁ ⁻¹ᵁ (i₁ ⁻¹ᵁ U))) :
    trFun hsq U g = Z.presheaf.map (eqToHom (preimage_eq hsq U)).op g

def

ψ

L582 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.ψ

Documentation

The first section pulled to the intersection and transported through the gluing isomorphism.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Matched
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) {L₁ : V₁.Modules} (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

def ψ (U : W.Opens) (s₁ : Γ(L₁, i₁ ⁻¹ᵁ U)) : Γ((Modules.pullback j₂).obj L₂, j₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ U))

lemma

ψ_def

L585 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.ψ_def

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Matched
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) {L₁ : V₁.Modules} (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

lemma ψ_def (U : W.Opens) (s₁ : Γ(L₁, i₁ ⁻¹ᵁ U)) :
    ψ hsq L₂ φ U s₁ = tr hsq _ U (φ.hom.app _ (pullbackLocalSection j₁ s₁))

lemma

ψ_smul

L588 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.ψ_smul

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Matched
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) {L₁ : V₁.Modules} (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

lemma ψ_smul (U : W.Opens) (g : Γ(V₁, i₁ ⁻¹ᵁ U)) (s₁ : Γ(L₁, i₁ ⁻¹ᵁ U)) :
    ψ hsq L₂ φ U (g • s₁) = trFun hsq U (j₁.app _ g) • ψ hsq L₂ φ U s₁

lemma

ψ_add

L594 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.ψ_add

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Matched
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) {L₁ : V₁.Modules} (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

lemma ψ_add (U : W.Opens) (s₁ s₁' : Γ(L₁, i₁ ⁻¹ᵁ U)) :
    ψ hsq L₂ φ U (s₁ + s₁') = ψ hsq L₂ φ U s₁ + ψ hsq L₂ φ U s₁'

lemma

ψ_map

L598 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.ψ_map

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Matched
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) {L₁ : V₁.Modules} (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

lemma ψ_map {U V : W.Opens} (hVU : V ≤ U) (s₁ : Γ(L₁, i₁ ⁻¹ᵁ U)) :
    ψ hsq L₂ φ V (L₁.presheaf.map (homOfLE (i₁.preimage_mono hVU)).op s₁) =
      ((Modules.pullback j₂).obj L₂).presheaf.map (homOfLE (j₂.preimage_mono (i₂.preimage_mono
        hVU))).op
        (ψ hsq L₂ φ U s₁)

lemma

ψ_map_of_eq

L606 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.ψ_map_of_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_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Matched
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) {L₁ : V₁.Modules} (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

lemma ψ_map_of_eq {U V : W.Opens} (hVU : V ≤ U) {s₁ : Γ(L₁, i₁ ⁻¹ᵁ U)} {s₂ : Γ(L₂, i₂ ⁻¹ᵁ U)}
    {t : Γ(Z, j₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ U))} (h : ψ hsq L₂ φ U s₁ = t • pullbackLocalSection j₂ s₂) :
    ψ hsq L₂ φ V (L₁.presheaf.map (homOfLE (i₁.preimage_mono hVU)).op s₁) =
      Z.presheaf.map (homOfLE (j₂.preimage_mono (i₂.preimage_mono hVU))).op t •
        pullbackLocalSection j₂ (L₂.presheaf.map (homOfLE (i₂.preimage_mono hVU)).op s₂)

lemma

ψ_map_of_eq'

L613 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.ψ_map_of_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_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Matched
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) {L₁ : V₁.Modules} (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

lemma ψ_map_of_eq' {U V : W.Opens} (hVU : V ≤ U) {s₁ : Γ(L₁, i₁ ⁻¹ᵁ U)} {s₂ : Γ(L₂, i₂ ⁻¹ᵁ U)}
    (h : ψ hsq L₂ φ U s₁ = pullbackLocalSection j₂ s₂) :
    ψ hsq L₂ φ V (L₁.presheaf.map (homOfLE (i₁.preimage_mono hVU)).op s₁) =
      pullbackLocalSection j₂ (L₂.presheaf.map (homOfLE (i₂.preimage_mono hVU)).op s₂)

lemma

trFun_map

L619 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.trFun_map

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Matched
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) {L₁ : V₁.Modules} (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

lemma trFun_map {U V : W.Opens} (hVU : V ≤ U) (g : Γ(Z, j₁ ⁻¹ᵁ (i₁ ⁻¹ᵁ U))) :
    trFun hsq V (Z.presheaf.map (homOfLE (j₁.preimage_mono (i₁.preimage_mono hVU))).op g) =
      Z.presheaf.map (homOfLE (j₂.preimage_mono (i₂.preimage_mono hVU))).op (trFun hsq U g)

lemma

exists_unit

L629 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.exists_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_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Matched
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) {L₁ : V₁.Modules} (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {L₂ φ}

Lean source · statement

lemma exists_unit (U : W.Opens) {e₁ : Γ(L₁, i₁ ⁻¹ᵁ U)} {e₂ : Γ(L₂, i₂ ⁻¹ᵁ U)}
    (he₁ : IsFrameOn e₁ (i₁ ⁻¹ᵁ U)) (he₂ : IsFrameOn e₂ (i₂ ⁻¹ᵁ U)) :
    ∃ u : Γ(Z, j₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ U)), IsUnit u ∧ ψ hsq L₂ φ U e₁ = u • pullbackLocalSection j₂ e₂

lemma

exists_frames

L641 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.exists_frames

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Matched
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) {L₁ : V₁.Modules} (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {L₂ φ}
variable [IsClosedImmersion i₁] [IsClosedImmersion i₂] [IsClosedImmersion j₂]

Lean source · statement

lemma exists_frames (hL₁ : IsInvertible L₁) (hL₂ : IsInvertible L₂) (w : W) :
    ∃ U : W.Opens, w ∈ U ∧ ∃ (e₁ : Γ(L₁, i₁ ⁻¹ᵁ U)) (e₂ : Γ(L₂, i₂ ⁻¹ᵁ U)),
      IsFrameOn e₁ (i₁ ⁻¹ᵁ U) ∧ IsFrameOn e₂ (i₂ ⁻¹ᵁ U)

lemma

exists_matched_frames

L651 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.exists_matched_frames

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Matched
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) {L₁ : V₁.Modules} (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable {L₂ φ}
variable [IsClosedImmersion i₁] [IsClosedImmersion i₂] [IsClosedImmersion j₂]

Lean source · statement

lemma exists_matched_frames (hL₁ : IsInvertible L₁) (hL₂ : IsInvertible L₂) (w : W) :
    ∃ U : W.Opens, w ∈ U ∧ ∃ (e₁ : Γ(L₁, i₁ ⁻¹ᵁ U)) (e₂ : Γ(L₂, i₂ ⁻¹ᵁ U)),
      IsFrameOn e₁ (i₁ ⁻¹ᵁ U) ∧ IsFrameOn e₂ (i₂ ⁻¹ᵁ U) ∧ ψ hsq L₂ φ U e₁ = pullbackLocalSection j₂
        e₂

def

Milnor

L697 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.Milnor

Documentation

Sections on the ambient open are uniquely determined by compatible sections on the two pieces.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section GluedFrame
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  {hsq : j₁ ≫ i₁ = j₂ ≫ i₂} {L₁ : V₁.Modules} {L₂ : V₂.Modules}
  {φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂}

Lean source · statement

def Milnor (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (U : W.Opens) : Prop

lemma

c₁_map'

L702 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.c₁_map'

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section GluedFrame
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  {hsq : j₁ ≫ i₁ = j₂ ≫ i₂} {L₁ : V₁.Modules} {L₂ : V₂.Modules}
  {φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂}

Lean source · statement

lemma c₁_map' {U V : W.Opens} (hVU : V ≤ U) (s : Γ(glued hsq L₁ L₂ φ, U)) :
    c₁ ((glued hsq L₁ L₂ φ).presheaf.map (homOfLE hVU).op s) =
      L₁.presheaf.map (homOfLE (i₁.preimage_mono hVU)).op (c₁ s)

lemma

c₂_map'

L707 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.c₂_map'

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section GluedFrame
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  {hsq : j₁ ≫ i₁ = j₂ ≫ i₂} {L₁ : V₁.Modules} {L₂ : V₂.Modules}
  {φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂}

Lean source · statement

lemma c₂_map' {U V : W.Opens} (hVU : V ≤ U) (s : Γ(glued hsq L₁ L₂ φ, U)) :
    c₂ ((glued hsq L₁ L₂ φ).presheaf.map (homOfLE hVU).op s) =
      L₂.presheaf.map (homOfLE (i₂.preimage_mono hVU)).op (c₂ s)

theorem

isFrameOn_mk

L712 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.isFrameOn_mk

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section GluedFrame
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  {hsq : j₁ ≫ i₁ = j₂ ≫ i₂} {L₁ : V₁.Modules} {L₂ : V₂.Modules}
  {φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂}

Lean source · statement

theorem isFrameOn_mk {U : W.Opens} (hmil : ∀ V : W.Opens, V ≤ U → Milnor hsq V)
    {e₁ : Γ(L₁, i₁ ⁻¹ᵁ U)} {e₂ : Γ(L₂, i₂ ⁻¹ᵁ U)} (he₁ : IsFrameOn e₁ (i₁ ⁻¹ᵁ U))
    (he₂ : IsFrameOn e₂ (i₂ ⁻¹ᵁ U)) (h : ψ hsq L₂ φ U e₁ = pullbackLocalSection j₂ e₂) :
    IsFrameOn (mk e₁ e₂ h : Γ(glued hsq L₁ L₂ φ, U)) U

lemma

pullbackComp_inv_app_app_pullbackLocalSection

L763 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.pullbackComp_inv_app_app_pullbackLocalSection

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section CompCongr
variable {P Y X : Scheme.{u}}

Lean source · statement

lemma pullbackComp_inv_app_app_pullbackLocalSection (g : P ⟶ Y) (f : Y ⟶ X) (M : X.Modules) (U :
  X.Opens)
    (s : Γ(M, U)) :
    ((pullbackComp g f).inv.app M).app (g ⁻¹ᵁ (f ⁻¹ᵁ U)) (pullbackLocalSection (g ≫ f) s) =
      pullbackLocalSection g (pullbackLocalSection f s)

lemma

pullbackComp_hom_app_app_pullbackLocalSection

L772 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.pullbackComp_hom_app_app_pullbackLocalSection

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section CompCongr
variable {P Y X : Scheme.{u}}

Lean source · statement

lemma pullbackComp_hom_app_app_pullbackLocalSection (g : P ⟶ Y) (f : Y ⟶ X) (M : X.Modules) (U :
  X.Opens)
    (s : Γ(M, U)) :
    ((pullbackComp g f).hom.app M).app (g ⁻¹ᵁ (f ⁻¹ᵁ U)) (pullbackLocalSection g
      (pullbackLocalSection f s)) =
      pullbackLocalSection (g ≫ f) s

lemma

pullbackCongr_hom_app_app_pullbackLocalSection

L781 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.pullbackCongr_hom_app_app_pullbackLocalSection

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section CompCongr
variable {P Y X : Scheme.{u}}

Lean source · full declaration

lemma pullbackCongr_hom_app_app_pullbackLocalSection {f g : P ⟶ X} (h : f = g) (M : X.Modules) (U :
  X.Opens)
    (s : Γ(M, U)) :
    ((pullbackCongr h).hom.app M).app (f ⁻¹ᵁ U) (pullbackLocalSection f s) =
      ((Modules.pullback g).obj M).presheaf.map (eqToHom (show f ⁻¹ᵁ U = g ⁻¹ᵁ U by rw [h])).op
        (pullbackLocalSection g s) := by
  subst h
  simp only [pullbackCongr, eqToIso_refl, Iso.refl_hom, NatTrans.id_app, Scheme.Modules.Hom.id_app,
    eqToHom_refl, op_id, CategoryTheory.Functor.map_id]

def

α₁

L801 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.α₁

Documentation

The adjoint projection from the pullback of the glued module to the module on the first piece.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

def α₁ : (Modules.pullback i₁).obj (glued hsq L₁ L₂ φ) ⟶ L₁

def

α₂

L806 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.α₂

Documentation

The adjoint projection from the pullback of the glued module to the module on the second piece.

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

def α₂ : (Modules.pullback i₂).obj (glued hsq L₁ L₂ φ) ⟶ L₂

lemma

α₁_app

L809 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.α₁_app

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

lemma α₁_app {U : W.Opens} (s : Γ(glued hsq L₁ L₂ φ, U)) :
    (α₁ hsq L₁ L₂ φ).app (i₁ ⁻¹ᵁ U) (pullbackLocalSection i₁ s) = c₁ s

lemma

α₂_app

L813 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.α₂_app

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)

Lean source · statement

lemma α₂_app {U : W.Opens} (s : Γ(glued hsq L₁ L₂ φ, U)) :
    (α₂ hsq L₁ L₂ φ).app (i₂ ⁻¹ᵁ U) (pullbackLocalSection i₂ s) = c₂ s

theorem

exists_isInvertible

L819 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare.AlgebraicGeometry.Scheme.Modules.MilnorPatch.exists_isInvertible

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
namespace MilnorPatch
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
section Main
variable {W V₁ V₂ Z : Scheme.{u}} {i₁ : V₁ ⟶ W} {i₂ : V₂ ⟶ W} {j₁ : Z ⟶ V₁} {j₂ : Z ⟶ V₂}
  (hsq : j₁ ≫ i₁ = j₂ ≫ i₂) (L₁ : V₁.Modules) (L₂ : V₂.Modules)
  (φ : (Modules.pullback j₁).obj L₁ ≅ (Modules.pullback j₂).obj L₂)
variable [IsClosedImmersion i₁] [IsClosedImmersion i₂] [IsClosedImmersion j₂]

Lean source · statement

theorem exists_isInvertible (hmil : ∀ U : W.Opens, Milnor hsq U) (hL₁ : IsInvertible L₁)
    (hL₂ : IsInvertible L₂) :
    ∃ (L : W.Modules), IsInvertible L ∧
      ∃ (α₁ : (Modules.pullback i₁).obj L ≅ L₁) (α₂ : (Modules.pullback i₂).obj L ≅ L₂),
        (Modules.pullback j₁).map α₁.hom ≫ φ.hom =
          ((pullbackComp j₁ i₁).app L).hom ≫ ((pullbackCongr hsq).app L).hom ≫
            ((pullbackComp j₂ i₂).app L).inv ≫ (Modules.pullback j₂).map α₂.hom

theorem

exists_isInvertible_pullback_iso_of_milnorSquare

L1025 ↗

AlgebraicGeometry.Scheme.Modules.exists_isInvertible_pullback_iso_of_milnorSquare

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_isInvertible_pullback_iso_of_milnorSquare
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_.TopologicalSpace
open _root_.Opposite
open _root_.AlgebraicGeometry.Scheme.Modules AlgebraicGeometry.Scheme.Modules in

Lean source · full declaration

theorem _root_.AlgebraicGeometry.Scheme.Modules.exists_isInvertible_pullback_iso_of_milnorSquare
    {W V₁ V₂ Z : Scheme.{u}} (i₁ : V₁ ⟶ W) (i₂ : V₂ ⟶ W) (j₁ : Z ⟶ V₁) (j₂ : Z ⟶ V₂)
    [IsClosedImmersion i₁] [IsClosedImmersion i₂] [IsClosedImmersion j₂] (hsq : j₁ ≫ i₁ = j₂ ≫ i₂)
    (hmil : ∀ U : W.Opens,
      Function.Injective (fun f : Γ(W, U) => ((i₁.app U) f, (i₂.app U) f)) ∧
        ∀ (g₁ : Γ(V₁, i₁ ⁻¹ᵁ U)) (g₂ : Γ(V₂, i₂ ⁻¹ᵁ U)),
          Z.presheaf.map
              (eqToHom (show j₂ ⁻¹ᵁ (i₂ ⁻¹ᵁ U) = j₁ ⁻¹ᵁ (i₁ ⁻¹ᵁ U) by
                rw [← Scheme.Hom.comp_preimage, ← Scheme.Hom.comp_preimage, hsq])).op
            ((j₁.app (i₁ ⁻¹ᵁ U)) g₁) = (j₂.app (i₂ ⁻¹ᵁ U)) g₂ →
          ∃ f : Γ(W, U), (i₁.app U) f = g₁ ∧ (i₂.app U) f = g₂)
    (L₁ : V₁.Modules) (hL₁ : Scheme.Modules.IsInvertible L₁)
    (L₂ : V₂.Modules) (hL₂ : Scheme.Modules.IsInvertible L₂)
    (φ : (Scheme.Modules.pullback j₁).obj L₁ ≅ (Scheme.Modules.pullback j₂).obj L₂) :
    ∃ (L : W.Modules), Scheme.Modules.IsInvertible L ∧
      ∃ (α₁ : (Scheme.Modules.pullback i₁).obj L ≅ L₁) (α₂ : (Scheme.Modules.pullback i₂).obj L ≅
        L₂),
        (Scheme.Modules.pullback j₁).map α₁.hom ≫ φ.hom =
          ((Scheme.Modules.pullbackComp j₁ i₁).app L).hom ≫ ((Scheme.Modules.pullbackCongr hsq).app
            L).hom ≫
            ((Scheme.Modules.pullbackComp j₂ i₂).app L).inv ≫ (Scheme.Modules.pullback j₂).map
              α₂.hom :=
  AlgebraicGeometry.Scheme.Modules.MilnorPatch.exists_isInvertible hsq L₁ L₂ φ hmil hL₁ hL₂

Module documentation

Scheme Modules exists is Invertible pullback iso of milnor Square

Declarations