NYLL
Module

Scheme_Modules_isIso_baseChangeHom_iff_of_isPullback.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isIso_baseChangeHom_iff_of_isPullback
6 declarations indexed from sourceView source ↗

Module documentation

Independence of a Cartesian presentation of base change

The isomorphism property of a module base-change comparison is independent of the chosen scheme realizing the same Cartesian square.

Imports2
Imported by4

Declarations

theorem

invE5_map_eqToHom_comp_app

L45 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_iff_of_isPullback.AlgebraicGeometry.Scheme.Modules.invE5_map_eqToHom_comp_app
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChangeHom_iff_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
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
Lean source · statement
theorem invE5_map_eqToHom_comp_app {Y : Scheme.{u}} {M N : Y.Modules} (φ : M ⟶ N) {U V : Y.Opens}
    (e : U = V) :
    M.presheaf.map (eqToHom e).op ≫ φ.app U = φ.app V ≫ N.presheaf.map (eqToHom e).op
theorem

invE5_inv_app_map_eqToHom_id_hom_app

L50 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_iff_of_isPullback.AlgebraicGeometry.Scheme.Modules.invE5_inv_app_map_eqToHom_id_hom_app
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChangeHom_iff_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
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
Lean source · statement
theorem invE5_inv_app_map_eqToHom_id_hom_app {Y : Scheme.{u}} {P Q : Y.Modules} (c : P ≅ Q) {W₁
    W₃ : Y.Opens}
    (e : W₃ = W₁) :
    c.inv.app W₁ ≫ P.presheaf.map (eqToHom e).op ≫ 𝟙 _ ≫ c.hom.app W₃ = Q.presheaf.map (eqToHom
        e).op
theorem

invE5_ext_of_unit_app_comp

L58 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_iff_of_isPullback.AlgebraicGeometry.Scheme.Modules.invE5_ext_of_unit_app_comp
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChangeHom_iff_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
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
Lean source · statement
theorem invE5_ext_of_unit_app_comp {T T' : Scheme.{u}} (ψ : T' ⟶ T) {M : T.Modules} {N : T'.Modules}
    (f₁ f₂ : (Modules.pullback ψ).obj M ⟶ N)
    (h : ∀ U : T.Opens, ((pullbackPushforwardAdjunction ψ).unit.app M).app U ≫ f₁.app (ψ ⁻¹ᵁ U) =
      ((pullbackPushforwardAdjunction ψ).unit.app M).app U ≫ f₂.app (ψ ⁻¹ᵁ U)) : f₁ = f₂
def

invE5_pushforwardIsoEquivalence

L69 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_iff_of_isPullback.AlgebraicGeometry.Scheme.Modules.invE5_pushforwardIsoEquivalence
Documentation

The equivalence of module sheaves on isomorphic schemes given by pushforward along e.hom and e.inv.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChangeHom_iff_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
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
Lean source · statement
def invE5_pushforwardIsoEquivalence {Y Y' : Scheme.{u}} (e : Y ≅ Y') : Y.Modules ≌
    Y'.Modules
theorem

invE5_baseChangeHom_iso_comp

L77 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isIso_baseChangeHom_iff_of_isPullback.AlgebraicGeometry.Scheme.Modules.invE5_baseChangeHom_iso_comp
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChangeHom_iff_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
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
Lean source · statement
theorem invE5_baseChangeHom_iso_comp {X T T' X₁ X₂ : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T}
    {π₂ : X₂ ⟶ T'} {g₂ : X₂ ⟶ X} (θ : X₁ ≅ X₂) (h₂ : g₂ ≫ π = π₂ ≫ ψ)
    (h₁ : (θ.hom ≫ g₂) ≫ π = (θ.hom ≫ π₂) ≫ ψ) (F : X.Modules) :
    baseChangeHom h₁ F =
      baseChangeHom h₂ F ≫ (pushforward π₂).map ((pullbackPushforwardAdjunction θ.hom).unit.app
          ((Modules.pullback g₂).obj F)) ≫
        (pushforwardComp θ.hom π₂).hom.app ((Modules.pullback θ.hom).obj ((Modules.pullback
            g₂).obj F)) ≫
          (pushforward (θ.hom ≫ π₂)).map ((pullbackComp θ.hom g₂).hom.app F)
theorem

isIso_baseChangeHom_iff_of_isPullback

L140 ↗
AlgebraicGeometry.Scheme.Modules.isIso_baseChangeHom_iff_of_isPullback
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isIso_baseChangeHom_iff_of_isPullback
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
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
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.isIso_baseChangeHom_iff_of_isPullback
    {X T T' X₁ X₂ : Scheme.{u}} {π : X ⟶ T} {ψ : T' ⟶ T}
    {π₁ : X₁ ⟶ T'} {g₁ : X₁ ⟶ X} {π₂ : X₂ ⟶ T'} {g₂ : X₂ ⟶ X}
    (h₁ : IsPullback g₁ π₁ π ψ) (h₂ : IsPullback g₂ π₂ π ψ) (F : X.Modules) :
    IsIso (Scheme.Modules.baseChangeHom h₁.w F) ↔ IsIso (Scheme.Modules.baseChangeHom h₂.w F)

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