NYLL
Module

Scheme_Modules_unitAutSection_comap_refinement_eq_appLE.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_unitAutSection_comap_refinement_eq_appLE
54 declarations indexed from sourceView source ↗

Module documentation

Compatibility of transition sections with refinement and pullback

Imports13
Imported by2

Declarations

lemma

comp_square_right

L44 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.comp_square_right
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
Lean source · statement
lemma comp_square_right {C : Type*} [Category C]
    {A B D E F G : C} {f : A ⟶ B} {g : B ⟶ D} {k : A ⟶ E} {l : E ⟶ D}
    (hfg : f ≫ g = k ≫ l) (h : D ⟶ F) (i : F ⟶ G) :
    f ≫ (g ≫ h) ≫ i = k ≫ l ≫ h ≫ i
lemma

comp_unit_cancel

L51 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.comp_unit_cancel
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
Lean source · statement
lemma comp_unit_cancel {C : Type*} [Category C]
    {A B D E F G H : C} (e : A ≅ B) (b : B ⟶ D) (f : D ⟶ E)
    (z : F ≅ E) (c : F ⟶ G) (d : G ⟶ H) (v : E ⟶ H)
    (hu : z.hom ≫ v = c ≫ d) :
    b ≫ f ≫ v = e.inv ≫ (e.hom ≫ b ≫ f ≫ z.inv ≫ c) ≫ d
lemma

comp_hom_id_inv

L59 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.comp_hom_id_inv
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
Lean source · statement
lemma comp_hom_id_inv {C : Type*} [Category C] {A B D : C}
    (e : A ≅ B) (f : A ⟶ D) : e.hom ≫ (𝟙 B ≫ e.inv ≫ f) = f
def

uapp

L108 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules.uapp
Documentation

The map on global ring sections induced by an automorphism of the structure module.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
def uapp (W : Y.Opens)
    (e : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
      Scheme.{u}).ringCatSheaf))
    (x : (W : Scheme.{u}).presheaf.obj (op ⊤)) : (W : Scheme.{u}).presheaf.obj (op ⊤)
theorem

unitAutSection_eq

L116 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules.unitAutSection_eq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_eq (W : Y.Opens)
    (e : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
      Scheme.{u}).ringCatSheaf)) :
    unitAutSection W e = W.topIso.hom.hom (uapp W e 1)
theorem

uapp_mul

L123 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules.uapp_mul
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem uapp_mul (W : Y.Opens)
    (e : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
      Scheme.{u}).ringCatSheaf))
    (x y : (W : Scheme.{u}).presheaf.obj (op ⊤)) : uapp W e (x * y) = x * uapp W e y
theorem

uapp_trans

L132 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules.uapp_trans
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem uapp_trans (W : Y.Opens)
    (e e' : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W :
      Scheme.{u}) : TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
      Scheme.{u}).ringCatSheaf))
    (x : (W : Scheme.{u}).presheaf.obj (op ⊤)) : uapp W (e ≪≫ e') x = uapp W e' (uapp W e x)
theorem

uapp_refl

L141 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules.uapp_refl
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem uapp_refl (W : Y.Opens) (x : (W : Scheme.{u}).presheaf.obj (op ⊤)) : uapp W (Iso.refl _) x
  = x
theorem

unitAutSection_trans

L146 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules.unitAutSection_trans
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_trans (W : Y.Opens)
    (e e' : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W :
      Scheme.{u}) : TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
      Scheme.{u}).ringCatSheaf)) :
    unitAutSection W (e ≪≫ e') = unitAutSection W e * unitAutSection W e'
theorem

unitAutSection_refl

L155 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules.unitAutSection_refl
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_refl (W : Y.Opens) :
    unitAutSection W (Iso.refl _) = 1
theorem

unitAutSection_symm_mul

L159 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules.unitAutSection_symm_mul
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_symm_mul (W : Y.Opens)
    (e : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
      Scheme.{u}).ringCatSheaf)) :
    unitAutSection W e.symm * unitAutSection W e = 1
theorem

unitAutSection_mul_symm

L167 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules.unitAutSection_mul_symm
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_mul_symm (W : Y.Opens)
    (e : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
      Scheme.{u}).ringCatSheaf)) :
    unitAutSection W e * unitAutSection W e.symm = 1
theorem

isUnit_unitAutSection

L175 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules.isUnit_unitAutSection
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem isUnit_unitAutSection (W : Y.Opens)
    (e : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
      Scheme.{u}).ringCatSheaf)) :
    IsUnit (unitAutSection W e)
lemma

pullbackCongr_hom_app_eq

L197 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.pullbackCongr_hom_app_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · full declaration
lemma pullbackCongr_hom_app_eq {q q' : T ⟶ A'} (H : q = q') (N : A'.Modules) :
    (pullbackCongr H).hom.app N = eqToHom (by rw [H]) := by
  subst H
  simp only [pullbackCongr, eqToIso_refl, Iso.refl_hom, NatTrans.id_app, eqToHom_refl]
lemma

pullbackCongr_inv_app_eq

L202 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.pullbackCongr_inv_app_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · full declaration
lemma pullbackCongr_inv_app_eq {q q' : T ⟶ A'} (H : q = q') (N : A'.Modules) :
    (pullbackCongr H).inv.app N = eqToHom (by rw [H]) := by
  subst H
  simp only [pullbackCongr, eqToIso_refl, Iso.refl_inv, NatTrans.id_app, eqToHom_refl]
lemma

pullbackCongr_app_hom_eq

L207 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.pullbackCongr_app_hom_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · full declaration
lemma pullbackCongr_app_hom_eq {q q' : T ⟶ A'} (H : q = q') (N : A'.Modules) :
    ((pullbackCongr H).app N).hom = eqToHom (by rw [H]) :=
  pullbackCongr_hom_app_eq H N
lemma

pullbackCongr_app_inv_eq

L211 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.pullbackCongr_app_inv_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · full declaration
lemma pullbackCongr_app_inv_eq {q q' : T ⟶ A'} (H : q = q') (N : A'.Modules) :
    ((pullbackCongr H).app N).inv = eqToHom (by rw [H]) :=
  pullbackCongr_inv_app_eq H N
lemma

assoc_app

L215 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.assoc_app
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · full declaration
lemma assoc_app {W : Scheme.{u}} (f : T' ⟶ T) (g : T ⟶ W) (h : W ⟶ A') (N : A'.Modules) :
    (Scheme.Modules.pullback f).map ((pullbackComp g h).inv.app N) ≫
      (pullbackComp f g).hom.app ((Scheme.Modules.pullback h).obj N) ≫ (pullbackComp (f ≫ g)
        h).hom.app N =
    (pullbackComp f (g ≫ h)).hom.app N ≫ eqToHom (by rw [Category.assoc]) := by
  have := NatTrans.congr_app (pseudofunctor_associativity f g h) N
  simp only [NatTrans.comp_app, Functor.whiskerRight_app, Functor.whiskerLeft_app,
    Functor.associator_hom_app,
    eqToHom_app] at this
  erw [Category.id_comp] at this
  exact (Iso.inv_comp_eq ((pullbackComp f (g ≫ h)).app N)).1 this
lemma

assoc_app''

L227 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.assoc_app''
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · full declaration
lemma assoc_app'' {W : Scheme.{u}} (f : T' ⟶ T) (g : T ⟶ W) (h : W ⟶ A') (N : A'.Modules) :
    (Scheme.Modules.pullback f).map ((pullbackComp g h).inv.app N) =
      (pullbackComp f (g ≫ h)).hom.app N ≫ eqToHom
        (by rw [Category.assoc]) ≫ (pullbackComp (f ≫ g) h).inv.app N ≫
        (pullbackComp f g).inv.app ((Scheme.Modules.pullback h).obj N) := by
  have h1 := assoc_app f g h N
  let α : (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback g).obj
    ((Scheme.Modules.pullback h).obj N)) ≅
      (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback (g ≫ h)).obj N) :=
    (Scheme.Modules.pullback f).mapIso ((pullbackComp g h).app N)
  let β : (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback g).obj
    ((Scheme.Modules.pullback h).obj N)) ≅
      (Scheme.Modules.pullback (f ≫ g)).obj ((Scheme.Modules.pullback h).obj N) :=
    (pullbackComp f g).app ((Scheme.Modules.pullback h).obj N)
  let γ : (Scheme.Modules.pullback (f ≫ g)).obj ((Scheme.Modules.pullback h).obj N) ≅
      (Scheme.Modules.pullback ((f ≫ g) ≫ h)).obj N := (pullbackComp (f ≫ g) h).app N
  let δ : (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback (g ≫ h)).obj N) ≅
      (Scheme.Modules.pullback (f ≫ g ≫ h)).obj N := (pullbackComp f (g ≫ h)).app N
  let η : (Scheme.Modules.pullback (f ≫ g ≫ h)).obj N ≅ (Scheme.Modules.pullback ((f ≫ g) ≫ h)).obj
    N :=
    eqToIso (by rw [Category.assoc])
  have h2 : α.symm ≪≫ β ≪≫ γ = δ ≪≫ η := Iso.ext h1
  have h3 : α.symm = δ ≪≫ η ≪≫ γ.symm ≪≫ β.symm := by
    calc α.symm = (α.symm ≪≫ β ≪≫ γ) ≪≫ (γ.symm ≪≫ β.symm) := by simp
      _ = (δ ≪≫ η) ≪≫ (γ.symm ≪≫ β.symm) := by rw [h2]
      _ = δ ≪≫ η ≪≫ γ.symm ≪≫ β.symm := by simp
  have h4 := congrArg Iso.hom h3
  simpa [α, β, γ, δ, η, eqToIso] using h4
lemma

comp_congr_right

L256 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.comp_congr_right
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · full declaration
lemma comp_congr_right (f : T' ⟶ T) {g g' : T ⟶ A'} (H : g = g') (N : A'.Modules) :
    (pullbackComp f g).inv.app N ≫ eqToHom (by rw [H]) ≫ (pullbackComp f g').hom.app N =
      eqToHom (by rw [H]) := by
  subst H
  simpa only [eqToHom_refl, Category.comp_id, Category.id_comp] using
    (pullbackComp f g).inv_hom_id_app N
lemma

comp_congr_left

L263 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.comp_congr_left
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · full declaration
lemma comp_congr_left {f f' : T' ⟶ T} (H : f = f') (g : T ⟶ A') (N : A'.Modules) :
    (pullbackComp f g).inv.app N ≫
        eqToHom (show (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback g).obj N) =
          (Scheme.Modules.pullback f').obj ((Scheme.Modules.pullback g).obj N) by rw [H]) =
      eqToHom (by rw [H]) ≫ (pullbackComp f' g).inv.app N := by
  subst H; simp
lemma

congr_unit

L270 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.congr_unit
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · statement
lemma congr_unit {f f' : T' ⟶ T} (H : f = f') :
    (pullbackCongr H).hom.app ((SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (T : TopCat)) T.ringCatSheaf)) ≫ (pullbackUnitIso
      f').hom =
      (pullbackUnitIso f).hom
lemma

congr_nat

L279 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.congr_nat
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · statement
lemma congr_nat {f f' : T' ⟶ T} (H : f = f') {M N : T.Modules} (φ : M ⟶ N) :
    (pullbackCongr H).hom.app M ≫ (Scheme.Modules.pullback f').map φ =
      (Scheme.Modules.pullback f).map φ ≫ (pullbackCongr H).hom.app N
def

toU

L301 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.toU
Documentation

A ring section regarded as a section of the structure module.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
section conj
variable {X Z : Scheme.{u}} (φ : X ⟶ Z)
Lean source · statement
def toU (U : Z.Opens) (g : Z.presheaf.obj (op U)) :
    Γ(((SheafOfModules.unit (J := _root_.Opens.grothendieckTopology (Z : TopCat))
      Z.ringCatSheaf) : Z.Modules), U)
theorem

pullbackUnitIso_hom_app_pls

L305 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.pullbackUnitIso_hom_app_pls
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
section conj
variable {X Z : Scheme.{u}} (φ : X ⟶ Z)
Lean source · statement
theorem pullbackUnitIso_hom_app_pls (U : Z.Opens) (g : Z.presheaf.obj (op U)) :
    (pullbackUnitIso φ).hom.app (φ ⁻¹ᵁ U) (pullbackLocalSection φ (toU U g)) =
      toU (φ ⁻¹ᵁ U) ((φ.app U).hom g)
theorem

pullbackUnitIso_inv_app_one

L315 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.pullbackUnitIso_inv_app_one
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
section conj
variable {X Z : Scheme.{u}} (φ : X ⟶ Z)
Lean source · statement
theorem pullbackUnitIso_inv_app_one (U : Z.Opens) :
    (pullbackUnitIso φ).inv.app (φ ⁻¹ᵁ U) (toU (φ ⁻¹ᵁ U) 1) = pullbackLocalSection φ (toU U 1)
def

uASm

L328 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.uASm
Documentation

The ring section corresponding to an automorphism of the structure module.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
Lean source · statement
def uASm (W : Y.Opens)
    (E : @Iso ((W : Scheme.{u}).Modules) _ ((SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
      Scheme.{u}).ringCatSheaf))
      ((SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
        TopCat)) (W : Scheme.{u}).ringCatSheaf))) : Γ(Y, W)
theorem

uASm_trans

L344 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.uASm_trans
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
section uasMod
variable (W : Y.Opens)
  (E E' : @Iso ((W : Scheme.{u}).Modules) _ ((SheafOfModules.unit (J :=
    _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
    Scheme.{u}).ringCatSheaf))
    ((SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf)))
Lean source · statement
theorem uASm_trans : uASm W (E ≪≫ E') = uASm W E * uASm W E'
theorem

isUnit_uASm

L346 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.isUnit_uASm
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
section uasMod
variable (W : Y.Opens)
  (E E' : @Iso ((W : Scheme.{u}).Modules) _ ((SheafOfModules.unit (J :=
    _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
    Scheme.{u}).ringCatSheaf))
    ((SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf)))
Lean source · statement
theorem isUnit_uASm : IsUnit (uASm W E)
theorem

uASm_eq

L348 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.uASm_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
section uasMod
variable (W : Y.Opens)
  (E E' : @Iso ((W : Scheme.{u}).Modules) _ ((SheafOfModules.unit (J :=
    _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
    Scheme.{u}).ringCatSheaf))
    ((SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf)))
Lean source · statement
theorem uASm_eq : uASm W E = W.topIso.hom.hom (uapp W E 1)
lemma

presheaf_map_op_apply_eq

L352 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.presheaf_map_op_apply_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
Lean source · statement
lemma presheaf_map_op_apply_eq {U V : Y.Opens} (f g : U ⟶ V) (x : Y.presheaf.obj (op V)) :
    (Y.presheaf.map f.op).hom x = (Y.presheaf.map g.op).hom x
lemma

presheaf_comp_apply_eq

L356 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.presheaf_comp_apply_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
Lean source · statement
lemma presheaf_comp_apply_eq {U V V' W : Y.Opens} (f : V ⟶ U) (g : W ⟶ V) (f' : V' ⟶ U) (g' : W ⟶
  V')
    (x : Y.presheaf.obj (op U)) :
    (Y.presheaf.map f.op ≫ Y.presheaf.map g.op).hom x = (Y.presheaf.map f'.op ≫ Y.presheaf.map
      g'.op).hom x
theorem

unitAutSection_conj

L364 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.unitAutSection_conj
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_conj {W W' : Y.Opens} (h' : W' ≤ W)
    (E : @Iso ((W : Scheme.{u}).Modules) _ ((SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
      Scheme.{u}).ringCatSheaf))
      ((SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
        TopCat)) (W : Scheme.{u}).ringCatSheaf))) :
    uASm W' ((pullbackUnitIso (Y.homOfLE h')).symm ≪≫
        (Scheme.Modules.pullback (Y.homOfLE h')).mapIso E ≪≫ pullbackUnitIso (Y.homOfLE h')) =
      (Y.presheaf.map (homOfLE h').op).hom (uASm W E)
def

genRestrict

L395 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.genRestrict
Documentation

Transports a module trivialisation through a commuting pullback square.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
section G
variable {Y V B : Scheme.{u}} (𝓜 : Y.Modules)
Lean source · statement
def genRestrict (ι : V ⟶ Y) (j : B ⟶ Y) (k : B ⟶ V) (e : k ≫ ι = j)
    (τ : (Scheme.Modules.pullback ι).obj 𝓜 ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (V : TopCat)) V.ringCatSheaf)) :
    (Scheme.Modules.pullback j).obj 𝓜 ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (B : TopCat)) B.ringCatSheaf)
theorem

genRestrict_comp

L403 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.genRestrict_comp
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
section G
variable {Y V B : Scheme.{u}} (𝓜 : Y.Modules)
Lean source · statement
theorem genRestrict_comp (ι : V ⟶ Y) (j : B ⟶ Y) (k : B ⟶ V) (e : k ≫ ι = j)
    (τ : (Scheme.Modules.pullback ι).obj 𝓜 ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (V : TopCat)) V.ringCatSheaf))
    {B' : Scheme.{u}} (q : B' ⟶ B) (j' : B' ⟶ Y) (e' : q ≫ j = j') (k' : B' ⟶ V) (Hk : q ≫ k = k')
    (e'' : k' ≫ ι = j') :
    genRestrict 𝓜 ι j' k' e'' τ =
      ((pullbackComp q j).app 𝓜 ≪≫ (pullbackCongr e').app 𝓜).symm ≪≫
        (Scheme.Modules.pullback q).mapIso (genRestrict 𝓜 ι j k e τ) ≪≫ pullbackUnitIso q
lemma

conj_symm_trans_conj

L447 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.conj_symm_trans_conj
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
section isoAlgebra
variable {C D : Type*} [Category C] [Category D] (F : C ⥤ D)
Lean source · statement
lemma conj_symm_trans_conj {M : C} {N U : D} {I : C} (κ : F.obj M ≅ N) (ε : F.obj I ≅ U) (Ra Rb : M
  ≅ I) :
    (κ.symm ≪≫ F.mapIso Ra ≪≫ ε).symm ≪≫ (κ.symm ≪≫ F.mapIso Rb ≪≫ ε) =
      ε.symm ≪≫ F.mapIso (Ra.symm ≪≫ Rb) ≪≫ ε
lemma

symm_trans_trans_symm_trans

L456 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.symm_trans_trans_symm_trans
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
section isoAlgebra
variable {C D : Type*} [Category C] [Category D] (F : C ⥤ D)
Lean source · statement
lemma symm_trans_trans_symm_trans {M I : C} (Ra Rb Rc : M ≅ I) :
    (Ra.symm ≪≫ Rb) ≪≫ (Rb.symm ≪≫ Rc) = Ra.symm ≪≫ Rc
theorem

restrict_eq_genRestrict

L466 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.restrict_eq_genRestrict
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem restrict_eq_genRestrict {a : 𝒱.ι} {W : Y.Opens} (h : W ≤ 𝒱.U a) :
    τ.restrict h = genRestrict 𝓜 (𝒱.U a).ι W.ι (Y.homOfLE h) (Y.homOfLE_ι h) (τ a)
def

κiso

L470 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.κiso
Documentation

The canonical comparison between iterated restriction and restriction to the smaller open.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
def κiso (𝓜 : Y.Modules) {W W' : Y.Opens} (h' : W' ≤ W) :
    (Scheme.Modules.pullback (Y.homOfLE h')).obj ((Scheme.Modules.pullback W.ι).obj 𝓜) ≅
      (Scheme.Modules.pullback W'.ι).obj 𝓜
theorem

restrict_trans

L475 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.restrict_trans
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem restrict_trans {a : 𝒱.ι} {W W' : Y.Opens} (h : W ≤ 𝒱.U a) (h' : W' ≤ W) :
    τ.restrict (h'.trans h) =
      (κiso 𝓜 h').symm ≪≫
        (Scheme.Modules.pullback (Y.homOfLE h')).mapIso (τ.restrict h) ≪≫ pullbackUnitIso
          (Y.homOfLE h')
def

θ

L486 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.θ
Documentation

The transition section obtained by comparing two local trivialisations.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
def θ (W : Y.Opens) (a b : 𝒱.ι) (ha : W ≤ 𝒱.U a) (hb : W ≤ 𝒱.U b) : Γ(Y, W)
theorem

transition_eq_θ

L489 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.transition_eq_θ
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem transition_eq_θ (s : 𝒱.Idx 1) :
    τ.transition s = θ τ (𝒱.inter s) (s.1 0) (s.1 1) (𝒱.inter_le s 0) (𝒱.inter_le s 1)
theorem

θ_res

L492 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.θ_res
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem θ_res {W W' : Y.Opens} (h' : W' ≤ W) (a b : 𝒱.ι) (ha : W ≤ 𝒱.U a) (hb : W ≤ 𝒱.U b) :
    (Y.presheaf.map (homOfLE h').op).hom (θ τ W a b ha hb) = θ τ W' a b (h'.trans ha) (h'.trans hb)
theorem

θ_mul

L501 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.θ_mul
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem θ_mul (W : Y.Opens) (a b c : 𝒱.ι) (ha : W ≤ 𝒱.U a) (hb hb' : W ≤ 𝒱.U b) (hc : W ≤ 𝒱.U c) :
    θ τ W a b ha hb * θ τ W b c hb' hc = θ τ W a c ha hc
theorem

isUnit_transition

L507 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.isUnit_transition
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem isUnit_transition (s : 𝒱.Idx 1) : IsUnit (τ.transition s)
theorem

cocycle

L510 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL.cocycle
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem cocycle (r : 𝒱.Idx 2) :
    (Y.presheaf.map (homOfLE (𝒱.inter_le_inter_face r 2)).op).hom (τ.transition (𝒱.face r 2)) *
        (Y.presheaf.map (homOfLE (𝒱.inter_le_inter_face r 0)).op).hom (τ.transition (𝒱.face r 0)) =
      (Y.presheaf.map (homOfLE (𝒱.inter_le_inter_face r 1)).op).hom (τ.transition (𝒱.face r 1))
theorem

genRestrict_congr_k

L531 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TLC4.genRestrict_congr_k
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLC4
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL
section generic
variable {Y Y' : Scheme.{u}} (𝓜 : Y.Modules) (h : Y' ⟶ Y)
Lean source · statement
theorem genRestrict_congr_k {V B : Scheme.{u}} (ι : V ⟶ Y) (j : B ⟶ Y) {k k' : B ⟶ V} (H : k = k')
    (e : k ≫ ι = j) (e' : k' ≫ ι = j)
    (τc : (Scheme.Modules.pullback ι).obj 𝓜 ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (V : TopCat)) V.ringCatSheaf)) :
    genRestrict 𝓜 ι j k e τc = genRestrict 𝓜 ι j k' e' τc
theorem

genRestrict_precomp

L539 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TLC4.genRestrict_precomp
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLC4
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL
section generic
variable {Y Y' : Scheme.{u}} (𝓜 : Y.Modules) (h : Y' ⟶ Y)
Lean source · statement
theorem genRestrict_precomp {V V' B : Scheme.{u}} (ι : V ⟶ Y) (ι' : V' ⟶ Y') (k₁ : V' ⟶ V)
    (e₁ : k₁ ≫ ι = ι' ≫ h)
    (τc : (Scheme.Modules.pullback ι).obj 𝓜 ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (V : TopCat)) V.ringCatSheaf))
    (j : B ⟶ Y') (k₂ : B ⟶ V') (e₂ : k₂ ≫ ι' = j) (e₃ : (k₂ ≫ k₁) ≫ ι = j ≫ h) :
    genRestrict ((Scheme.Modules.pullback h).obj 𝓜) ι' j k₂ e₂
        ((pullbackComp ι' h).app 𝓜 ≪≫ genRestrict 𝓜 ι (ι' ≫ h) k₁ e₁ τc) =
      (pullbackComp j h).app 𝓜 ≪≫ genRestrict 𝓜 ι (j ≫ h) (k₂ ≫ k₁) e₃ τc
theorem

comap_eq_genRestrict

L579 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TLC4.comap_eq_genRestrict
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLC4
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL
section comapAsGen
variable {Y Y' : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
  (h : Y' ⟶ Y) [IsAffineHom h]
Lean source · statement
theorem comap_eq_genRestrict (c : 𝒱.ι) :
    τ.comap h c = (pullbackComp (h ⁻¹ᵁ 𝒱.U c).ι h).app 𝓜 ≪≫
      genRestrict 𝓜 (𝒱.U c).ι ((h ⁻¹ᵁ 𝒱.U c).ι ≫ h) (h ∣_ 𝒱.U c) (morphismRestrict_ι h (𝒱.U c)) (τ
        c)
theorem

pullbackComp_trans_genRestrict_rfl

L603 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.FFT2.pullbackComp_trans_genRestrict_rfl
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace FFT2
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TLC4
section generic
variable {Y V B : Scheme.{u}} (𝓜 : Y.Modules)
Lean source · statement
theorem pullbackComp_trans_genRestrict_rfl (ι : V ⟶ Y) (k : B ⟶ V)
    (τc : (Scheme.Modules.pullback ι).obj 𝓜 ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (V : TopCat)) V.ringCatSheaf)) :
    (pullbackComp k ι).app 𝓜 ≪≫ genRestrict 𝓜 ι (k ≫ ι) k rfl τc =
      (Scheme.Modules.pullback k).mapIso τc ≪≫ pullbackUnitIso k
lemma

trans_symm_trans_trans

L613 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.FFT2.trans_symm_trans_trans
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace FFT2
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TLC4
section generic
variable {Y V B : Scheme.{u}} (𝓜 : Y.Modules)
Lean source · statement
lemma trans_symm_trans_trans {C : Type*} [Category C] {P Q R : C} (c : P ≅ Q) (G₁ G₂ : Q ≅ R) :
    (c ≪≫ G₁).symm ≪≫ (c ≪≫ G₂) = G₁.symm ≪≫ G₂
theorem

appLE_uASm

L622 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.FFT2.appLE_uASm
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace FFT2
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TLC4
section lemmaB
variable {Y Y' : Scheme.{u}} (h : Y' ⟶ Y)
Lean source · statement
theorem appLE_uASm {W : Y.Opens} {W' : Y'.Opens} (hle : W' ≤ h ⁻¹ᵁ W)
    (E : @Iso ((W : Scheme.{u}).Modules) _ ((SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
      Scheme.{u}).ringCatSheaf))
      ((SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
        TopCat)) (W : Scheme.{u}).ringCatSheaf))) :
    (h.appLE W W' hle).hom (uASm W E) =
      uASm W' ((pullbackUnitIso (h.resLE W W' hle)).symm ≪≫
        (Scheme.Modules.pullback (h.resLE W W' hle)).mapIso E ≪≫ pullbackUnitIso (h.resLE W W'
          hle))
theorem

core

L660 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.FFT2.core
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace FFT2
open _root_.AlgebraicGeometry.Scheme.Modules
open
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TL
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.PV1TLC4
Lean source · statement
theorem core {X X' X₀ X₀' : Scheme.{u}}
    (g : X₀ ⟶ X) (g' : X₀' ⟶ X') (h : X' ⟶ X) (h₀ : X₀' ⟶ X₀) (hh₀ : h₀ ≫ g = g' ≫ h)
    (M : X.Modules) (U : X.Opens) (Ww : X'.Opens) (U' : X₀.Opens) (W' : X₀'.Opens)
    (gU : (U' : Scheme.{u}) ⟶ (U : Scheme.{u})) (egU : gU ≫ U.ι = U'.ι ≫ g)
    (gW : (W' : Scheme.{u}) ⟶ (Ww : Scheme.{u})) (egW : gW ≫ Ww.ι = W'.ι ≫ g')
    (r : (Ww : Scheme.{u}) ⟶ (U : Scheme.{u})) (e₁ : r ≫ U.ι = Ww.ι ≫ h)
    (hle : W' ≤ h₀ ⁻¹ᵁ U')
    (τa : (Scheme.Modules.pullback U.ι).obj M ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology ((U : Scheme.{u}) : TopCat)) (U :
      Scheme.{u}).ringCatSheaf))
    (φ₀ : (Scheme.Modules.pullback g).obj M ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (X₀ : TopCat)) X₀.ringCatSheaf))
    (TW : (Scheme.Modules.pullback W'.ι).obj ((Scheme.Modules.pullback g').obj
      ((Scheme.Modules.pullback h).obj M)) ≅
      (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W' : Scheme.{u}) :
        TopCat)) (W' : Scheme.{u}).ringCatSheaf))
    (hTW : TW = (pullbackComp W'.ι g').app ((Scheme.Modules.pullback h).obj M) ≪≫
      genRestrict ((Scheme.Modules.pullback h).obj M) Ww.ι (W'.ι ≫ g') gW egW
        ((pullbackComp Ww.ι h).app M ≪≫ genRestrict M U.ι (Ww.ι ≫ h) r e₁ τa))
    (TU : (Scheme.Modules.pullback U'.ι).obj ((Scheme.Modules.pullback g).obj M) ≅
      (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((U' : Scheme.{u}) :
        TopCat)) (U' : Scheme.{u}).ringCatSheaf))
    (hTU : TU = (pullbackComp U'.ι g).app M ≪≫ genRestrict M U.ι (U'.ι ≫ g) gU egU τa) :
    uASm W' (TW.symm ≪≫ ((Scheme.Modules.pullback W'.ι).mapIso
        ((pullbackComp g' h).app M ≪≫ (pullbackCongr hh₀.symm).app M ≪≫ ((pullbackComp h₀ g).app
          M).symm ≪≫
          (Scheme.Modules.pullback h₀).mapIso φ₀ ≪≫ pullbackUnitIso h₀) ≪≫ pullbackUnitIso W'.ι)) =
      (h₀.appLE U' W' hle).hom (uASm U' (TU.symm ≪≫
        ((Scheme.Modules.pullback U'.ι).mapIso φ₀ ≪≫ pullbackUnitIso U'.ι)))
theorem

unitAutSection_comap_refinement_eq_appLE

L733 ↗
AlgebraicGeometry.Scheme.Modules.unitAutSection_comap_refinement_eq_appLE
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
open _root_.AlgebraicGeometry.Scheme.Modules
  _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.UnitAutRefinement.AlgebraicGeometry.Scheme.Modules
  PV1TL PV1TLC4 FFT2 in
Lean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.Modules.unitAutSection_comap_refinement_eq_appLE
    {X X' X₀ X₀' : Scheme.{u}}
    (g : X₀ ⟶ X) [IsAffineHom g] (g' : X₀' ⟶ X') [IsAffineHom g']
    (h : X' ⟶ X) (h₀ : X₀' ⟶ X₀) (hh₀ : h₀ ≫ g = g' ≫ h)
    (𝒰 : X.OrderedAffineCover) (𝒲 : X'.OrderedAffineCover) (lam : 𝒲.ι → 𝒰.ι)
    (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒰.U (lam w))
    (M : X.Modules) (τ : Scheme.Modules.CechTrivialisation 𝒰 M)
    (τ' : Scheme.Modules.CechTrivialisation 𝒲 ((Scheme.Modules.pullback h).obj M))
    (w : 𝒲.ι) (hτ' : τ' w = (((Scheme.Modules.pullbackComp (𝒲.U w).ι h).app M) ≪≫
          ((Scheme.Modules.pullbackCongr
              (show (𝒲.U w).ι ≫ h = (X'.homOfLE (hlam w) ≫ (h ∣_ 𝒰.U (lam w))) ≫ (𝒰.U (lam w)).ι by
                rw [Category.assoc, morphismRestrict_ι, ← Category.assoc, Scheme.homOfLE_ι])).app
                  M) ≪≫
          ((Scheme.Modules.pullbackComp (X'.homOfLE (hlam w) ≫ (h ∣_ 𝒰.U (lam w))) (𝒰.U (lam
            w)).ι).app M).symm ≪≫
          (Scheme.Modules.pullback (X'.homOfLE (hlam w) ≫ (h ∣_ 𝒰.U (lam w)))).mapIso (τ (lam w)) ≪≫
          Scheme.Modules.pullbackUnitIso (X'.homOfLE (hlam w) ≫ (h ∣_ 𝒰.U (lam w)))))
    (φ₀ : (Scheme.Modules.pullback g).obj M ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (X₀ : TopCat)) X₀.ringCatSheaf)) :
    Scheme.Modules.unitAutSection ((𝒲.comap g').U w)
        ((τ'.comap g' w).symm ≪≫
          ((Scheme.Modules.pullback ((𝒲.comap g').U w).ι).mapIso (((Scheme.Modules.pullbackComp g'
            h).app M) ≪≫
          ((Scheme.Modules.pullbackCongr hh₀.symm).app M) ≪≫
          ((Scheme.Modules.pullbackComp h₀ g).app M).symm ≪≫
          (Scheme.Modules.pullback h₀).mapIso φ₀ ≪≫
          Scheme.Modules.pullbackUnitIso h₀) ≪≫
            Scheme.Modules.pullbackUnitIso ((𝒲.comap g').U w).ι)) =
      (h₀.appLE ((𝒰.comap g).U (lam w)) ((𝒲.comap g').U w)
          (show g' ⁻¹ᵁ 𝒲.U w ≤ h₀ ⁻¹ᵁ (g ⁻¹ᵁ 𝒰.U (lam w)) by
            rw [← Scheme.Hom.comp_preimage, hh₀, Scheme.Hom.comp_preimage]
            exact fun p hp => hlam w hp)).hom
        (Scheme.Modules.unitAutSection ((𝒰.comap g).U (lam w))
          ((τ.comap g (lam w)).symm ≪≫
            ((Scheme.Modules.pullback ((𝒰.comap g).U (lam w)).ι).mapIso φ₀ ≪≫
              Scheme.Modules.pullbackUnitIso ((𝒰.comap g).U (lam w)).ι))) := by
  have e₁ : (X'.homOfLE (hlam w) ≫ (h ∣_ 𝒰.U (lam w))) ≫ (𝒰.U (lam w)).ι = (𝒲.U w).ι ≫ h := by
    rw [Category.assoc, morphismRestrict_ι, ← Category.assoc, Scheme.homOfLE_ι]
  have hτ'w : τ' w = (pullbackComp (𝒲.U w).ι h).app M ≪≫
      genRestrict M (𝒰.U (lam w)).ι ((𝒲.U w).ι ≫ h) (X'.homOfLE (hlam w) ≫ (h ∣_ 𝒰.U (lam w))) e₁
        (τ (lam w)) := by
    rw [hτ']
    apply Iso.ext
    dsimp only [genRestrict, Iso.trans, Iso.symm, Iso.app, Functor.mapIso]
    rw [pullbackCongr_hom_app_eq, pullbackCongr_inv_app_eq]
  exact core g g' h h₀ hh₀ M (𝒰.U (lam w)) (𝒲.U w) ((𝒰.comap g).U (lam w)) ((𝒲.comap g').U w)
    (g ∣_ 𝒰.U (lam w)) (morphismRestrict_ι g (𝒰.U (lam w))) (g' ∣_ 𝒲.U w) (morphismRestrict_ι g'
      (𝒲.U w))
    (X'.homOfLE (hlam w) ≫ (h ∣_ 𝒰.U (lam w))) e₁ _ (τ (lam w)) φ₀
    (τ'.comap g' w) (by rw [comap_eq_genRestrict τ' g' w, hτ'w]; rfl)
    (τ.comap g (lam w)) (comap_eq_genRestrict τ g (lam w))

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