NYLL
Module

Scheme_Modules_baseChangeHom_comp_vertical.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_baseChangeHom_comp_vertical
4 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules base Change Hom comp vertical

Imports1
Imported by2

Declarations

theorem

pvE5_map_eqToHom_comp_app

L39 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_baseChangeHom_comp_vertical.AlgebraicGeometry.Scheme.Modules.pvE5_map_eqToHom_comp_app
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_baseChangeHom_comp_vertical
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 pvE5_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

pvE5_map_eqToHom_comp_map_eqToHom_comp_id

L44 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_baseChangeHom_comp_vertical.AlgebraicGeometry.Scheme.Modules.pvE5_map_eqToHom_comp_map_eqToHom_comp_id
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_baseChangeHom_comp_vertical
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 pvE5_map_eqToHom_comp_map_eqToHom_comp_id {Y : Scheme.{u}} (M : Y.Modules) {A₁ A₂ B₁ :
  Y.Opens}
    (a : A₁ = A₂) (b : B₁ = A₁) :
    M.presheaf.map (eqToHom a).op ≫ M.presheaf.map (eqToHom b).op ≫ 𝟙 _ =
      M.presheaf.map (eqToHom (b.trans a)).op
theorem

pvE5_ext_of_unit_app_comp

L51 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_baseChangeHom_comp_vertical.AlgebraicGeometry.Scheme.Modules.pvE5_ext_of_unit_app_comp
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_baseChangeHom_comp_vertical
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 pvE5_ext_of_unit_app_comp {T T' : Scheme.{u}} (ψ : T' ⟶ T) {M : T.Modules} {N : T'.Modules}
    (f₁ f₂ : (Scheme.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₂
theorem

baseChangeHom_comp_vertical

L63 ↗
AlgebraicGeometry.Scheme.Modules.baseChangeHom_comp_vertical
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_baseChangeHom_comp_vertical
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
open AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_baseChangeHom_comp_vertical
open AlgebraicGeometry.Scheme.Modules
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.baseChangeHom_comp_vertical
    {X Y T X' Y' T' : Scheme.{u}} {ρ : X ⟶ Y} {σ : Y ⟶ T} {ρ' : X' ⟶ Y'} {σ' : Y' ⟶ T'}
    {g' : X' ⟶ X} {k' : Y' ⟶ Y} {ψ : T' ⟶ T}
    (htop : g' ≫ ρ = ρ' ≫ k') (hbot : k' ≫ σ = σ' ≫ ψ) (h : g' ≫ (ρ ≫ σ) = (ρ' ≫ σ') ≫ ψ)
    (F : X.Modules) :
    Scheme.Modules.baseChangeHom h F =
      (Scheme.Modules.pullback ψ).map ((Scheme.Modules.pushforwardComp ρ σ).inv.app F) ≫
        Scheme.Modules.baseChangeHom hbot ((Scheme.Modules.pushforward ρ).obj F) ≫
          (Scheme.Modules.pushforward σ').map (Scheme.Modules.baseChangeHom htop F) ≫
            (Scheme.Modules.pushforwardComp ρ' σ').hom.app ((Scheme.Modules.pullback g').obj F)

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