Module

Scheme_Modules_Hom_isIso_of_forall_exists_isIso_pullback_map.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_Hom_isIso_of_forall_exists_isIso_pullback_map

3 declarations indexed from sourceView source ↗

Module documentation

Detecting isomorphisms by local pullback

A module morphism is an isomorphism when its pullback is an isomorphism on an open neighborhood of each point.

Imports1

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_Hom_isIso_of_isIso_app_of_iSup_eq_top

Imported by4

lemma

restrictFunctor_map_app'

L47 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_Hom_isIso_of_forall_exists_isIso_pullback_map.AlgebraicGeometry.Scheme.Modules.restrictFunctor_map_app'

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_Hom_isIso_of_forall_exists_isIso_pullback_map
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}

Lean source · statement

lemma restrictFunctor_map_app' {M N : X.Modules} (φ : M ⟶ N) (U : X.Opens)
    (W : (U : Scheme.{u}).Opens) :
    ((restrictFunctor U.ι).map φ).app W = φ.app (U.ι ''ᵁ W)

lemma

isIso_app_of_isIso_pullback_ι_map

L51 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_Hom_isIso_of_forall_exists_isIso_pullback_map.AlgebraicGeometry.Scheme.Modules.isIso_app_of_isIso_pullback_ι_map

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_Hom_isIso_of_forall_exists_isIso_pullback_map
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}

Lean source · statement

lemma isIso_app_of_isIso_pullback_ι_map {M N : X.Modules} (φ : M ⟶ N) (U : X.Opens)
    (hU : IsIso ((Scheme.Modules.pullback U.ι).map φ)) (W : X.Opens) (hWU : W ≤ U) :
    IsIso (φ.app W)

theorem

isIso_of_forall_exists_isIso_pullback_map

L64 ↗

AlgebraicGeometry.Scheme.Modules.Hom.isIso_of_forall_exists_isIso_pullback_map

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_Hom_isIso_of_forall_exists_isIso_pullback_map
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X : Scheme.{u}}

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.Hom.isIso_of_forall_exists_isIso_pullback_map {M N :
  X.Modules} (φ : M ⟶ N)
    (h : ∀ x : X, ∃ U : X.Opens, x ∈ U ∧ IsIso ((Scheme.Modules.pullback U.ι).map φ)) :
    IsIso φ

Module documentation

Detecting isomorphisms by local pullback

Declarations

restrictFunctor_map_app'

isIso_app_of_isIso_pullback_ι_map

isIso_of_forall_exists_isIso_pullback_map