NYLL
Module

Scheme_Modules_pullbackUnitIso_conj_app_top_one_eq_appTop.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_pullbackUnitIso_conj_app_top_one_eq_appTop
9 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules pullback Unit Iso conj app top one eq app Top

Imports6
Imported by8

Declarations

def

unitConj

L66 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation.AlgebraicGeometry.Scheme.Modules.unitConj
Documentation

Conjugate the pullback of a unit-module automorphism by the canonical unit comparison.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation
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
section conj
variable {S S' : Scheme.{u}} (p : S' ⟶ S)
Lean source · statement
def unitConj
    (E : SheafOfModules.unit S.ringCatSheaf ≅ SheafOfModules.unit S.ringCatSheaf) :
    @Iso S'.Modules _ (SheafOfModules.unit S'.ringCatSheaf) (SheafOfModules.unit S'.ringCatSheaf)
def

pls

L72 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation.AlgebraicGeometry.Scheme.Modules.pls
Documentation

Pull back a local module section using the unit of the pullback-pushforward adjunction.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation
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
section conj
variable {S S' : Scheme.{u}} (p : S' ⟶ S)
Lean source · statement
def pls {L : S.Modules} {U : S.Opens} (s : Γ(L, U)) :
    Γ((pullback p).obj L, p ⁻¹ᵁ U)
lemma

pls_app

L76 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation.AlgebraicGeometry.Scheme.Modules.pls_app
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation
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
section conj
variable {S S' : Scheme.{u}} (p : S' ⟶ S)
Lean source · statement
lemma pls_app {L L' : S.Modules} {U : S.Opens} (θ : L ⟶ L') (s : Γ(L, U)) :
    pls p (θ.app U s) = ((pullback p).map θ).app (p ⁻¹ᵁ U) (pls p s)
lemma

pls_smul

L84 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation.AlgebraicGeometry.Scheme.Modules.pls_smul
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation
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
section conj
variable {S S' : Scheme.{u}} (p : S' ⟶ S)
Lean source · statement
lemma pls_smul {L : S.Modules} {U : S.Opens} (r : Γ(S, U)) (s : Γ(L, U)) :
    pls p (r • s) = p.app U r • pls p s
lemma

app_pls

L89 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation.AlgebraicGeometry.Scheme.Modules.app_pls
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation
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
section conj
variable {S S' : Scheme.{u}} (p : S' ⟶ S)
Lean source · statement
lemma app_pls {L : S.Modules} {N : S'.Modules} (g : (pullback p).obj L ⟶ N) {U : S.Opens} (s :
  Γ(L, U)) :
    g.app (p ⁻¹ᵁ U) (pls p s) =
      (((pullbackPushforwardAdjunction p).homEquiv L N g).app U s : Γ(N, p ⁻¹ᵁ U))
lemma

pullbackUnitIso_hom_app_pls

L96 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation.AlgebraicGeometry.Scheme.Modules.pullbackUnitIso_hom_app_pls
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation
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
section conj
variable {S S' : Scheme.{u}} (p : S' ⟶ S)
Lean source · full declaration
lemma pullbackUnitIso_hom_app_pls {U : S.Opens} (s : Γ(SheafOfModules.unit S.ringCatSheaf, U)) :
    (pullbackUnitIso p).hom.app (p ⁻¹ᵁ U) (pls p s) =
      (show Γ(SheafOfModules.unit S'.ringCatSheaf, p ⁻¹ᵁ U) from (p.app U).hom s) := by
  have h1 : (pullbackUnitIso p).hom =
      ((pullbackPushforwardAdjunction p).homEquiv _ _).symm
        (SheafOfModules.unitToPushforwardObjUnit p.toRingCatSheafHom) := rfl
  erw [h1, app_pls, Equiv.apply_symm_apply]
  rfl
lemma

pullbackUnitIso_inv_app_one

L105 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation.AlgebraicGeometry.Scheme.Modules.pullbackUnitIso_inv_app_one
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation
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
section conj
variable {S S' : Scheme.{u}} (p : S' ⟶ S)
Lean source · full declaration
lemma pullbackUnitIso_inv_app_one :
    (pullbackUnitIso p).inv.app ⊤ (1 : S'.presheaf.obj (op ⊤)) =
      (show Γ((pullback p).obj (SheafOfModules.unit S.ringCatSheaf), ⊤) from
        pls p (show Γ(SheafOfModules.unit S.ringCatSheaf, ⊤) from (1 : S.presheaf.obj (op ⊤))))
          := by
  have hinj : Function.Injective ((pullbackUnitIso p).hom.app ⊤) := by
    have hi (z : Γ((pullback p).obj (SheafOfModules.unit S.ringCatSheaf), ⊤)) :
        (pullbackUnitIso p).inv.app ⊤ ((pullbackUnitIso p).hom.app ⊤ z) = z :=
      congrArg (fun k : (pullback p).obj (SheafOfModules.unit S.ringCatSheaf) ⟶
          (pullback p).obj (SheafOfModules.unit S.ringCatSheaf) => k.val.app (op ⊤) z)
        (pullbackUnitIso p).hom_inv_id
    intro x y hxy
    exact (hi x).symm.trans ((congrArg ((pullbackUnitIso p).inv.app ⊤) hxy).trans (hi y))
  apply hinj
  have h2 := pullbackUnitIso_hom_app_pls p (U := ⊤)
    (show Γ(SheafOfModules.unit S.ringCatSheaf, ⊤) from (1 : S.presheaf.obj (op ⊤)))
  have hinv : (pullbackUnitIso p).hom.app ⊤
      ((pullbackUnitIso p).inv.app ⊤ (1 : S'.presheaf.obj (op ⊤))) =
        (1 : S'.presheaf.obj (op ⊤)) :=
    congrArg (fun k : (SheafOfModules.unit S'.ringCatSheaf : S'.Modules) ⟶
        (SheafOfModules.unit S'.ringCatSheaf : S'.Modules) =>
      k.val.app (op ⊤) (1 : S'.presheaf.obj (op ⊤))) (pullbackUnitIso p).inv_hom_id
  exact hinv.trans (h2.trans (map_one (p.app ⊤).hom)).symm
theorem

unitConj_app_one

L129 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation.AlgebraicGeometry.Scheme.Modules.unitConj_app_one
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation
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
section conj
variable {S S' : Scheme.{u}} (p : S' ⟶ S)
Lean source · statement
theorem unitConj_app_one (E : SheafOfModules.unit S.ringCatSheaf ≅ SheafOfModules.unit
  S.ringCatSheaf) :
    Scheme.Modules.Hom.app (unitConj p E).hom ⊤ (1 : S'.presheaf.obj (op ⊤)) =
      p.appTop.hom ((E.hom.val.app (op ⊤)).hom (1 : S.presheaf.obj (op ⊤)))
theorem

pullbackUnitIso_conj_app_top_one_eq_appTop

L156 ↗
AlgebraicGeometry.Scheme.Modules.pullbackUnitIso_conj_app_top_one_eq_appTop
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.PullbackUnitConjugation
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.pullbackUnitIso_conj_app_top_one_eq_appTop
    {S S' : Scheme.{u}} (p : S' ⟶ S)
    (e : SheafOfModules.unit S.ringCatSheaf ≅ SheafOfModules.unit S.ringCatSheaf) :
    ((((Scheme.Modules.pullbackUnitIso p).symm ≪≫ (Scheme.Modules.pullback p).mapIso e ≪≫
          Scheme.Modules.pullbackUnitIso p :
            SheafOfModules.unit S'.ringCatSheaf ≅ SheafOfModules.unit
              S'.ringCatSheaf)).hom.val.app (op ⊤)).hom
        (1 : S'.presheaf.obj (op ⊤)) =
      p.appTop.hom ((e.hom.val.app (op ⊤)).hom (1 : S.presheaf.obj (op ⊤)))

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