NYLL
Module

tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom
11 declarations indexed from sourceView source ↗

Module documentation

tilde pullback map pullback Spec Iso hom comp pullback Spec Iso hom

Imports2
Imported by2

Declarations

theorem

main

L58 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom.AlgebraicGeometry.TildePullbackCompAux.main
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace TildePullbackCompAux
open _root_.AlgebraicGeometry
open CategoryTheory
universe v₁ v₂ v₃ v₄ v₅ v₆ u₁ u₂ u₃ u₄ u₅ u₆
variable {A : Type u₁} {B : Type u₂} {C : Type u₃} {X : Type u₄} {Y : Type u₅} {Z : Type u₆}
  [Category.{v₁} A] [Category.{v₂} B] [Category.{v₃} C]
  [Category.{v₄} X] [Category.{v₅} Y] [Category.{v₆} Z]
  {FR : A ⥤ X} {GR : X ⥤ A} {FS : B ⥤ Y} {GS : Y ⥤ B} {FT : C ⥤ Z} {GT : Z ⥤ C}
  (tR : FR ⊣ GR) (tS : FS ⊣ GS) (tT : FT ⊣ GT)
  {Eφ : A ⥤ B} {Rφ : B ⥤ A} {Eψ : B ⥤ C} {Rψ : C ⥤ B} {Eφψ : A ⥤ C} {Rφψ : C ⥤ A}
  (eφ : Eφ ⊣ Rφ) (eψ : Eψ ⊣ Rψ) (eφψ : Eφψ ⊣ Rφψ)
  {Pφ : X ⥤ Y} {Qφ : Y ⥤ X} {Pψ : Y ⥤ Z} {Qψ : Z ⥤ Y} {Pφψ : X ⥤ Z} {Qφψ : Z ⥤ X}
  (pφ : Pφ ⊣ Qφ) (pψ : Pψ ⊣ Qψ) (pφψ : Pφψ ⊣ Qφψ)
  (dφ : Qφ ⋙ GR ≅ GS ⋙ Rφ) (dψ : Qψ ⋙ GS ≅ GT ⋙ Rψ) (dφψ : Qφψ ⋙ GR ≅ GT ⋙ Rφψ)
  (q : Qφψ ⟶ Qψ ⋙ Qφ) (r : Rφψ ⟶ Rψ ⋙ Rφ)
  (M : A)
  (βφ : Pφ.obj (FR.obj M) ⟶ FS.obj (Eφ.obj M))
  (βψ : Pψ.obj (FS.obj (Eφ.obj M)) ⟶ FT.obj (Eψ.obj (Eφ.obj M)))
  (βφψ : Pφψ.obj (FR.obj M) ⟶ FT.obj (Eφψ.obj M))
  (κ : (Pφ ⋙ Pψ).obj (FR.obj M) ⟶ Pφψ.obj (FR.obj M))
  (ε : Eφψ.obj M ⟶ (Eφ ⋙ Eψ).obj M)
Lean source · statement
theorem main
    (hφ : (tR.comp pφ).unit.app M ≫ (Qφ ⋙ GR).map βφ ≫ dφ.hom.app _ =
      eφ.unit.app M ≫ Rφ.map (tS.unit.app _))
    (hψ : (tS.comp pψ).unit.app (Eφ.obj M) ≫ (Qψ ⋙ GS).map βψ ≫ dψ.hom.app _ =
      eψ.unit.app _ ≫ Rψ.map (tT.unit.app _))
    (hφψ : (tR.comp pφψ).unit.app M ≫ (Qφψ ⋙ GR).map βφψ ≫ dφψ.hom.app _ =
      eφψ.unit.app M ≫ Rφψ.map (tT.unit.app _))
    (hκ : (pφ.comp pψ).unit.app (FR.obj M) ≫ (Qψ ⋙ Qφ).map κ = pφψ.unit.app _ ≫ q.app _)
    (hε : eφψ.unit.app M ≫ Rφψ.map ε ≫ r.app _ = eφ.unit.app M ≫ Rφ.map (eψ.unit.app _))
    (hcoh : ∀ N : Z, GR.map (q.app N) ≫ dφ.hom.app (Qψ.obj N) ≫ Rφ.map (dψ.hom.app N) =
      dφψ.hom.app N ≫ r.app (GT.obj N)) :
    Pψ.map βφ ≫ βψ = κ ≫ βφψ ≫ FT.map ε
theorem

pushforwardCongr_rfl

L152 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom.AlgebraicGeometry.TildePullbackCompAux.pushforwardCongr_rfl
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace TildePullbackCompAux
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {X Y Z : Scheme.{u}}
Lean source · statement
theorem pushforwardCongr_rfl (f : X ⟶ Y) :
    Scheme.Modules.pushforwardCongr (rfl : f = f) = Iso.refl _
theorem

comp_unit_app_comp_map_pullbackComp

L157 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom.AlgebraicGeometry.TildePullbackCompAux.comp_unit_app_comp_map_pullbackComp
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace TildePullbackCompAux
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {X Y Z : Scheme.{u}}
Lean source · statement
theorem comp_unit_app_comp_map_pullbackComp (f : X ⟶ Y) (g : Y ⟶ Z) (A : Z.Modules) :
    ((pullbackPushforwardAdjunction g).comp (pullbackPushforwardAdjunction f)).unit.app A ≫
        (pushforward f ⋙ pushforward g).map ((pullbackComp f g).hom.app A) =
      (pullbackPushforwardAdjunction (f ≫ g)).unit.app A ≫ (pushforwardComp f g).inv.app _
theorem

comp_unit_app_comp_map_pullbackComp_pullbackCongr

L172 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom.AlgebraicGeometry.TildePullbackCompAux.comp_unit_app_comp_map_pullbackComp_pullbackCongr
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace TildePullbackCompAux
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {X Y Z : Scheme.{u}}
Lean source · statement
theorem comp_unit_app_comp_map_pullbackComp_pullbackCongr (f : X ⟶ Y) (g : Y ⟶ Z) {k : X ⟶ Z}
    (h : f ≫ g = k) (A : Z.Modules) :
    ((pullbackPushforwardAdjunction g).comp (pullbackPushforwardAdjunction f)).unit.app A ≫
        (pushforward f ⋙ pushforward g).map ((pullbackComp f g).hom.app A ≫ (pullbackCongr
          h).hom.app A) =
      (pullbackPushforwardAdjunction k).unit.app A ≫
        ((pushforwardCongr h).inv ≫ (pushforwardComp f g).inv).app ((pullback k).obj A)
theorem

moduleSpecΓFunctor_map_pushforwardCongr_inv_apply

L186 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom.AlgebraicGeometry.TildePullbackCompAux.moduleSpecΓFunctor_map_pushforwardCongr_inv_apply
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace TildePullbackCompAux
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {X Y Z : Scheme.{u}}
variable {R : CommRingCat.{u}}
Lean source · statement
theorem moduleSpecΓFunctor_map_pushforwardCongr_inv_apply {f g : X ⟶ Spec R} (hf : f = g)
    (N : X.Modules) (y : (moduleSpecΓFunctor (R := R)).obj ((pushforward g).obj N)) :
    ((moduleSpecΓFunctor (R := R)).map ((pushforwardCongr hf).inv.app N)).hom y = y
theorem

pushforwardSpecCompΓIso_hom_app_apply

L192 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom.AlgebraicGeometry.TildePullbackCompAux.pushforwardSpecCompΓIso_hom_app_apply
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace TildePullbackCompAux
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicGeometry.Scheme.Modules
section Generic
variable {X Y Z : Scheme.{u}}
variable {R : CommRingCat.{u}}
Lean source · statement
theorem pushforwardSpecCompΓIso_hom_app_apply {S : CommRingCat.{u}} (φ : R ⟶ S) (N : (Spec
  S).Modules)
    (y : (moduleSpecΓFunctor (R := R)).obj ((pushforward (Spec.map φ)).obj N)) :
    ((pushforwardSpecCompΓIso φ).hom.app N :
      (moduleSpecΓFunctor (R := R)).obj ((pushforward (Spec.map φ)).obj N) ⟶
        (ModuleCat.restrictScalars φ.hom).obj ((moduleSpecΓFunctor (R := S)).obj N)).hom y = y
theorem

hε

L206 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom.AlgebraicGeometry.TildePullbackCompAux.hε
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace TildePullbackCompAux
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicGeometry.Scheme.Modules
section Concrete
variable {R S T : CommRingCat.{u}} (φ : R ⟶ S) (ψ : S ⟶ T)
Lean source · statement
theorem hε (M : ModuleCat.{u} R) :
    (ModuleCat.extendRestrictScalarsAdj (φ ≫ ψ).hom).unit.app M ≫
        (ModuleCat.restrictScalars (φ ≫ ψ).hom).map ((ModuleCat.extendScalarsComp φ.hom
          ψ.hom).hom.app M) ≫
        (ModuleCat.restrictScalarsComp φ.hom ψ.hom).hom.app
          ((ModuleCat.extendScalars ψ.hom).obj ((ModuleCat.extendScalars φ.hom).obj M)) =
      (ModuleCat.extendRestrictScalarsAdj φ.hom).unit.app M ≫
        (ModuleCat.restrictScalars φ.hom).map ((ModuleCat.extendRestrictScalarsAdj ψ.hom).unit.app
          ((ModuleCat.extendScalars φ.hom).obj M))
theorem

tail3_apply

L225 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom.AlgebraicGeometry.TildePullbackCompAux.tail3_apply
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace TildePullbackCompAux
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicGeometry.Scheme.Modules
section Concrete
variable {R S T : CommRingCat.{u}} (φ : R ⟶ S) (ψ : S ⟶ T)
Lean source · statement
theorem tail3_apply (N : (Spec T).Modules)
    (z : (moduleSpecΓFunctor (R := R)).obj ((pushforward (Spec.map ψ ≫ Spec.map φ)).obj N)) :
    ((ModuleCat.restrictScalars φ.hom).map ((pushforwardSpecCompΓIso ψ).hom.app N)).hom
      (((pushforwardSpecCompΓIso φ).hom.app ((pushforward (Spec.map ψ)).obj N)).hom
        (((moduleSpecΓFunctor (R := R)).map ((pushforwardComp (Spec.map ψ) (Spec.map φ)).inv.app
          N)).hom z)) =
      z
theorem

rhs_apply

L233 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom.AlgebraicGeometry.TildePullbackCompAux.rhs_apply
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace TildePullbackCompAux
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicGeometry.Scheme.Modules
section Concrete
variable {R S T : CommRingCat.{u}} (φ : R ⟶ S) (ψ : S ⟶ T)
Lean source · statement
theorem rhs_apply (N : (Spec T).Modules)
    (y : (moduleSpecΓFunctor (R := R)).obj ((pushforward (Spec.map (φ ≫ ψ))).obj N)) :
    ((pushforwardSpecCompΓIso (φ ≫ ψ)).hom.app N ≫
      (ModuleCat.restrictScalarsComp φ.hom ψ.hom).hom.app ((moduleSpecΓFunctor (R := T)).obj
        N)).hom y = y
theorem

hcoh

L239 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom.AlgebraicGeometry.TildePullbackCompAux.hcoh
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace TildePullbackCompAux
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicGeometry.Scheme.Modules
section Concrete
variable {R S T : CommRingCat.{u}} (φ : R ⟶ S) (ψ : S ⟶ T)
Lean source · statement
theorem hcoh (N : (Spec T).Modules) :
    (moduleSpecΓFunctor (R := R)).map
        (((pushforwardCongr (Spec.map_comp φ ψ).symm).inv ≫
            (pushforwardComp (Spec.map ψ) (Spec.map φ)).inv).app N) ≫
      (pushforwardSpecCompΓIso φ).hom.app ((pushforward (Spec.map ψ)).obj N) ≫
      (ModuleCat.restrictScalars φ.hom).map ((pushforwardSpecCompΓIso ψ).hom.app N) =
    (pushforwardSpecCompΓIso (φ ≫ ψ)).hom.app N ≫
      (ModuleCat.restrictScalarsComp φ.hom ψ.hom).hom.app ((moduleSpecΓFunctor (R := T)).obj N)
theorem

pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom

L260 ↗
AlgebraicGeometry.tilde.pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace tilde_pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open AlgebraicGeometry.TildePullbackCompAux _root_.AlgebraicGeometry.Scheme.Modules in
Lean source · statement
theorem _root_.AlgebraicGeometry.tilde.pullback_map_pullbackSpecIso_hom_comp_pullbackSpecIso_hom
    {R S T : CommRingCat.{u}} (φ : R ⟶ S) (ψ : S ⟶ T) (M : ModuleCat.{u} R) :
    (Scheme.Modules.pullback (Spec.map ψ)).map (tilde.pullbackSpecIso φ M).hom ≫
        (tilde.pullbackSpecIso ψ ((ModuleCat.extendScalars φ.hom).obj M)).hom =
      (Scheme.Modules.pullbackComp (Spec.map ψ) (Spec.map φ)).hom.app (tilde M) ≫
        (Scheme.Modules.pullbackCongr (Spec.map_comp φ ψ).symm).hom.app (tilde M) ≫
        (tilde.pullbackSpecIso (φ ≫ ψ) M).hom ≫
        (tilde.functor T).map ((ModuleCat.extendScalarsComp φ.hom ψ.hom).hom.app M)

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