NYLL
Module

PresheafInternalHom.lean

Nyll.SchemeTheory.Modules.PresheafInternalHom
42 declarations indexed from sourceView source ↗

Module documentation

Internal Hom of module presheaves

The internal Hom is constructed from families of linear maps compatible with restriction. Currying and uncurrying give the tensor-left adjunction, and hence the monoidal closed structure on module presheaves over a presheaf of commutative rings.

Imports1
  • Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Imported by43

Declarations

lemma

map_id_apply

L36 ↗
PresheafOfModules.InternalHom.map_id_apply
Source context 6 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
Lean source · statement
lemma map_id_apply (M : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) (X : Cᵒᵖ) (x : M.obj X) :
    M.map (𝟙 X) x = x
abbrev

PiFamily

L42 ↗
PresheafOfModules.InternalHom.PiFamily
Documentation

Families of linear maps indexed by arrows from X in the opposite category.

Source context 6 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
Lean source · statement
abbrev PiFamily (X : Cᵒᵖ) : Type (max u u' v')
def

IsNatural

L47 ↗
PresheafOfModules.InternalHom.IsNatural
Documentation

Compatibility of a family of linear maps with restriction along subsequent arrows.

Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
Lean source · statement
def IsNatural {X : Cᵒᵖ} (φ : PiFamily F N X) : Prop
def

naturalFamilies

L51 ↗
PresheafOfModules.InternalHom.naturalFamilies
Documentation

The additive subgroup of families compatible with restriction.

Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
Lean source · full declaration
def naturalFamilies (X : Cᵒᵖ) : AddSubgroup (PiFamily F N X) where
  carrier := {φ | IsNatural φ}
  zero_mem' := by
    intro Y Z f g x
    simp only [Pi.zero_apply, LinearMap.zero_apply]
    exact (N.map g).hom.map_zero
  add_mem' := by
    intro φ ψ hφ hψ Y Z f g x
    exact ((N.map g).hom.map_add (φ f x) (ψ f x)).trans
      (congrArg₂ (fun a b : N.obj Z => a + b) (hφ f g x) (hψ f g x))
  neg_mem' := by
    intro φ hφ Y Z f g x
    exact ((N.map g).hom.map_neg (φ f x)).trans
      (congrArg (fun a : N.obj Z => -a) (hφ f g x))
lemma

naturalFamilies_ext

L68 ↗
PresheafOfModules.InternalHom.naturalFamilies_ext
Source context 8 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
Lean source · statement
lemma naturalFamilies_ext {X : Cᵒᵖ} {φ ψ : naturalFamilies F N X}
    (h : ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (x : F.obj Y), φ.1 f x = ψ.1 f x) : φ = ψ
lemma

naturality

L72 ↗
PresheafOfModules.InternalHom.naturality
Source context 8 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
Lean source · statement
lemma naturality {X : Cᵒᵖ} (φ : naturalFamilies F N X) ⦃Y Z : Cᵒᵖ⦄ (f : X ⟶ Y) (g : Y ⟶ Z)
    (x : F.obj Y) : N.map g (φ.1 f x) = φ.1 (f ≫ g) (F.map g x)
lemma

congr_app

L75 ↗
PresheafOfModules.InternalHom.congr_app
Source context 8 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
Lean source · statement
lemma congr_app {X : Cᵒᵖ} (φ : naturalFamilies F N X) {Y : Cᵒᵖ} {f g : X ⟶ Y} (h : f = g)
    (x : F.obj Y) : φ.1 f x = φ.1 g x
instance

(anonymous instance)

L78 ↗
Source context 8 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
Lean source · full declaration
instance (X : Cᵒᵖ) : SMul (R.obj X) (naturalFamilies F N X) where
  smul r φ := ⟨fun Y f => R.map f r • φ.1 f, by
    intro Y Z f g x
    simp only [LinearMap.smul_apply]
    rw [N.map_smul]
    erw [φ.2 f g x]
    congr 1
    rw [Functor.map_comp]
    rfl⟩
lemma

smul_app

L88 ↗
PresheafOfModules.InternalHom.smul_app
Source context 8 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
Lean source · statement
lemma smul_app {X : Cᵒᵖ} (r : R.obj X) (φ : naturalFamilies F N X) {Y : Cᵒᵖ} (f : X ⟶ Y)
    (x : F.obj Y) : (r • φ).1 f x = R.map f r • φ.1 f x
lemma

add_app

L90 ↗
PresheafOfModules.InternalHom.add_app
Source context 8 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
Lean source · statement
lemma add_app {X : Cᵒᵖ} (φ ψ : naturalFamilies F N X) {Y : Cᵒᵖ} (f : X ⟶ Y)
    (x : F.obj Y) : (φ + ψ).1 f x = φ.1 f x + ψ.1 f x
lemma

zero_app

L92 ↗
PresheafOfModules.InternalHom.zero_app
Source context 8 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
Lean source · statement
lemma zero_app {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X ⟶ Y)
    (x : F.obj Y) : (0 : naturalFamilies F N X).1 f x = 0
lemma

neg_app

L94 ↗
PresheafOfModules.InternalHom.neg_app
Source context 8 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
Lean source · statement
lemma neg_app {X : Cᵒᵖ} (φ : naturalFamilies F N X) {Y : Cᵒᵖ} (f : X ⟶ Y)
    (x : F.obj Y) : (-φ).1 f x = - φ.1 f x
lemma

sub_app

L96 ↗
PresheafOfModules.InternalHom.sub_app
Source context 8 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
Lean source · statement
lemma sub_app {X : Cᵒᵖ} (φ ψ : naturalFamilies F N X) {Y : Cᵒᵖ} (f : X ⟶ Y)
    (x : F.obj Y) : (φ - ψ).1 f x = φ.1 f x - ψ.1 f x
instance

(anonymous instance)

L99 ↗
Source context 8 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
Lean source · full declaration
instance (X : Cᵒᵖ) : Module (R.obj X) (naturalFamilies F N X) where
  one_smul φ := by ext Y f x; simp
  mul_smul r s φ := by ext Y f x; simp [mul_smul]
  smul_zero r := by ext Y f x; simp
  smul_add r φ ψ := by ext Y f x; simp
  add_smul r s φ := by ext Y f x; simp [add_smul]
  zero_smul φ := by ext Y f x; simp
def

restrict

L110 ↗
PresheafOfModules.InternalHom.restrict
Documentation

Restriction of natural families by precomposing their indexing arrows.

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
variable (F N)
Lean source · full declaration
def restrict {X X' : Cᵒᵖ} (h : X ⟶ X') : naturalFamilies F N X →+ naturalFamilies F N X' where
  toFun φ := ⟨fun Y f => φ.1 (h ≫ f), fun Y Z f g x => by
    rw [φ.2 (h ≫ f) g x, Category.assoc]⟩
  map_zero' := rfl
  map_add' _ _ := rfl
lemma

restrict_app

L116 ↗
PresheafOfModules.InternalHom.restrict_app
Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
variable (F N)
Lean source · statement
lemma restrict_app {X X' : Cᵒᵖ} (h : X ⟶ X') (φ : naturalFamilies F N X) {Y : Cᵒᵖ}
    (f : X' ⟶ Y) (x : F.obj Y) : (restrict F N h φ).1 f x = φ.1 (h ≫ f) x
def

presheaf

L120 ↗
PresheafOfModules.InternalHom.presheaf
Documentation

The presheaf of additive groups of natural families of linear maps.

Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
variable (F N)
Lean source · full declaration
def presheaf : Cᵒᵖ ⥤ Ab.{max u u' v'} where
  obj X := AddCommGrpCat.of (naturalFamilies F N X)
  map h := AddCommGrpCat.ofHom (restrict F N h)
  map_id X := by
    ext φ Y f x
    change φ.1 (𝟙 X ≫ f) x = φ.1 f x
    rw [Category.id_comp]
  map_comp h h' := by
    ext φ Y f x
    change φ.1 ((h ≫ h') ≫ f) x = φ.1 (h ≫ (h' ≫ f)) x
    rw [Category.assoc]
lemma

presheaf_map_apply

L132 ↗
PresheafOfModules.InternalHom.presheaf_map_apply
Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
variable (F N)
Lean source · statement
lemma presheaf_map_apply {X X' : Cᵒᵖ} (h : X ⟶ X') (φ : naturalFamilies F N X) {Y : Cᵒᵖ}
    (f : X' ⟶ Y) (x : F.obj Y) : ((presheaf F N).map h φ).1 f x = φ.1 (h ≫ f) x
instance

(anonymous instance)

L135 ↗
Source context 9 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
variable (F N)
Lean source · statement
instance (X : Cᵒᵖ) : Module ((R ⋙ forget₂ CommRingCat RingCat).obj X) ((presheaf F N).obj X)
def

postcomp

L140 ↗
PresheafOfModules.InternalHom.postcomp
Documentation

Postcomposition of each linear map in a natural family by a module-presheaf morphism.

Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
variable (F N)
variable {N} in
Lean source · full declaration
def postcomp {N' : PresheafOfModules.{u} (R ⋙ forget₂ _ _)} (ψ : N ⟶ N') (X : Cᵒᵖ) :
    naturalFamilies F N X →+ naturalFamilies F N' X where
  toFun φ := ⟨fun Y f =>
    { toFun := fun x => ψ.app Y (φ.1 f x)
      map_add' := fun x x' => by simp
      map_smul' := fun r x => by
        rw [(φ.1 f).map_smul]
        exact (ψ.app Y).hom.map_smul r _ }, by
    intro Y Z f g x
    change N'.map g (ψ.app Y (φ.1 f x)) = ψ.app Z (φ.1 (f ≫ g) (F.map g x))
    rw [← naturality_apply, φ.2 f g x]⟩
  map_zero' := by ext Y f x; exact (ψ.app Y).hom.map_zero
  map_add' φ φ' := by ext Y f x; exact (ψ.app Y).hom.map_add _ _
lemma

postcomp_app

L154 ↗
PresheafOfModules.InternalHom.postcomp_app
Source context 10 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
namespace InternalHom
variable {F N} in
variable {F N}
variable (F N)
variable {N} in
Lean source · statement
lemma postcomp_app {N' : PresheafOfModules.{u} (R ⋙ forget₂ _ _)} (ψ : N ⟶ N') {X : Cᵒᵖ}
    (φ : naturalFamilies F N X) {Y : Cᵒᵖ} (f : X ⟶ Y) (x : F.obj Y) :
    (postcomp F ψ X φ).1 f x = ψ.app Y (φ.1 f x)
def

ihomObj

L163 ↗
PresheafOfModules.ihomObj
Documentation

The module presheaf of natural families of local linear maps from F to N.

Source context 6 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
open InternalHom
Lean source · statement
def ihomObj : PresheafOfModules.{max u u' v'} (R ⋙ forget₂ _ _)
lemma

ihomObj_map_val

L172 ↗
PresheafOfModules.ihomObj_map_val
Source context 6 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
open InternalHom
Lean source · statement
lemma ihomObj_map_val {X X' : Cᵒᵖ} (h : X ⟶ X') (φ : (ihomObj F N).obj X) {Y : Cᵒᵖ}
    (f : X' ⟶ Y) (x : F.obj Y) :
    ((ihomObj F N).map h φ).1 f x = φ.1 (h ≫ f) x
def

ihomMap

L178 ↗
PresheafOfModules.ihomMap
Documentation

The internal-Hom morphism induced by postcomposition in its second argument.

Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
open InternalHom
variable {N} in
Lean source · statement
def ihomMap {N' : PresheafOfModules.{u} (R ⋙ forget₂ _ _)} (ψ : N ⟶ N') :
    ihomObj F N ⟶ ihomObj F N'
lemma

ihomMap_app_val

L187 ↗
PresheafOfModules.ihomMap_app_val
Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
open InternalHom
variable {N} in
Lean source · statement
lemma ihomMap_app_val {N' : PresheafOfModules.{u} (R ⋙ forget₂ _ _)} (ψ : N ⟶ N')
    {X : Cᵒᵖ} (φ : (ihomObj F N).obj X) {Y : Cᵒᵖ} (f : X ⟶ Y) (x : F.obj Y) :
    ((ihomMap F ψ).app X φ).1 f x = ψ.app Y (φ.1 f x)
def

ihomFunctor

L192 ↗
PresheafOfModules.ihomFunctor
Documentation

The internal-Hom functor with fixed first argument F.

Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
open InternalHom
variable {N} in
Lean source · full declaration
def ihomFunctor :
    PresheafOfModules.{u} (R ⋙ forget₂ _ _) ⥤ PresheafOfModules.{max u u' v'} (R ⋙ forget₂ _ _)
      where
  obj N := ihomObj F N
  map ψ := ihomMap F ψ
  map_id N := by
    ext X φ
    apply naturalFamilies_ext
    intro Y f y; rfl
  map_comp ψ ψ' := by
    ext X φ
    apply naturalFamilies_ext
    intro Y f y; rfl
lemma

ihomFunctor_obj

L206 ↗
PresheafOfModules.ihomFunctor_obj
Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
open InternalHom
variable {N} in
Lean source · statement
lemma ihomFunctor_obj (N' : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) :
    (ihomFunctor F).obj N' = ihomObj F N'
lemma

ihomFunctor_map

L208 ↗
PresheafOfModules.ihomFunctor_map
Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section general
variable {C : Type u'} [Category.{v'} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F N : PresheafOfModules.{u} (R ⋙ forget₂ _ _))
open InternalHom
variable {N} in
Lean source · statement
lemma ihomFunctor_map {N' N'' : PresheafOfModules.{u} (R ⋙ forget₂ _ _)} (ψ : N' ⟶ N'') :
    (ihomFunctor F).map ψ = ihomMap F ψ
instance

commRingAt

L221 ↗
PresheafOfModules.commRingAt
Source context 5 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section closed

-- Keep the bundled-ring comparison at the same transparency as Mathlib's
-- `PresheafOfModulesOfCommRing.Monoidal.tensorObjMap`.
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}
Lean source · statement
instance commRingAt (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ CommRingCat RingCat).obj X)
def

curryFamily

L227 ↗
PresheafOfModules.InternalHom.curryFamily
Documentation

The natural family obtained by currying a tensor morphism against the section y.

Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section closed

-- Keep the bundled-ring comparison at the same transparency as Mathlib's
-- `PresheafOfModulesOfCommRing.Monoidal.tensorObjMap`.
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}
local instance commRingAt (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (R.obj X))
namespace InternalHom
Lean source · statement
def curryFamily (θ : F ⊗ G ⟶ N) {X : Cᵒᵖ} (y : G.obj X) : naturalFamilies F N X
lemma

curryFamily_app

L244 ↗
PresheafOfModules.InternalHom.curryFamily_app
Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section closed

-- Keep the bundled-ring comparison at the same transparency as Mathlib's
-- `PresheafOfModulesOfCommRing.Monoidal.tensorObjMap`.
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}
local instance commRingAt (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (R.obj X))
namespace InternalHom
Lean source · statement
lemma curryFamily_app (θ : F ⊗ G ⟶ N) {X : Cᵒᵖ} (y : G.obj X) {Y : Cᵒᵖ} (f : X ⟶ Y)
    (x : F.obj Y) : (curryFamily F θ y).1 f x = θ.app Y (x ⊗ₜ[R.obj Y] G.map f y)
def

curry'

L252 ↗
PresheafOfModules.curry'
Documentation

The internal-Hom morphism obtained by currying a tensor morphism.

Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section closed

-- Keep the bundled-ring comparison at the same transparency as Mathlib's
-- `PresheafOfModulesOfCommRing.Monoidal.tensorObjMap`.
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}
local instance commRingAt (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (R.obj X))
open InternalHom
Lean source · statement
def curry' (θ : F ⊗ G ⟶ N) : G ⟶ ihomObj F N
lemma

curry'_app_val

L282 ↗
PresheafOfModules.curry'_app_val
Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section closed

-- Keep the bundled-ring comparison at the same transparency as Mathlib's
-- `PresheafOfModulesOfCommRing.Monoidal.tensorObjMap`.
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}
local instance commRingAt (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (R.obj X))
open InternalHom
Lean source · statement
lemma curry'_app_val (θ : F ⊗ G ⟶ N) {X : Cᵒᵖ} (y : G.obj X) {Y : Cᵒᵖ} (f : X ⟶ Y)
    (x : F.obj Y) : ((curry' F θ).app X y).1 f x = θ.app Y (x ⊗ₜ[R.obj Y] G.map f y)
def

uncurryApp

L286 ↗
PresheafOfModules.uncurryApp
Documentation

The component of the uncurried tensor morphism, evaluated using the identity indexing arrow.

Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section closed

-- Keep the bundled-ring comparison at the same transparency as Mathlib's
-- `PresheafOfModulesOfCommRing.Monoidal.tensorObjMap`.
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}
local instance commRingAt (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (R.obj X))
open InternalHom
Lean source · statement
def uncurryApp (κ : G ⟶ ihomObj F N) (X : Cᵒᵖ) : (F ⊗ G).obj X ⟶ N.obj X
lemma

tensorObj_map_tmul'

L301 ↗
PresheafOfModules.tensorObj_map_tmul'
Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section closed

-- Keep the bundled-ring comparison at the same transparency as Mathlib's
-- `PresheafOfModulesOfCommRing.Monoidal.tensorObjMap`.
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}
local instance commRingAt (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (R.obj X))
open InternalHom
Lean source · full declaration
lemma tensorObj_map_tmul' {X Y : Cᵒᵖ} (g : X ⟶ Y) (x : F.obj X) (y : G.obj X) :
    DFunLike.coe (α := (F.obj X ⊗ G.obj X :))
      (β := fun _ => (ModuleCat.restrictScalars (R.map g).hom).obj (F.obj Y ⊗ G.obj Y))
      (ModuleCat.Hom.hom (R := ↑(R.obj X)) ((F ⊗ G).map g)) (x ⊗ₜ[R.obj X] y) =
    F.map g x ⊗ₜ[R.obj Y] G.map g y := rfl
lemma

uncurryApp_tmul

L307 ↗
PresheafOfModules.uncurryApp_tmul
Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section closed

-- Keep the bundled-ring comparison at the same transparency as Mathlib's
-- `PresheafOfModulesOfCommRing.Monoidal.tensorObjMap`.
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}
local instance commRingAt (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (R.obj X))
open InternalHom
Lean source · full declaration
lemma uncurryApp_tmul (κ : G ⟶ ihomObj F N) (X : Cᵒᵖ) (x : F.obj X) (y : G.obj X) :
    DFunLike.coe (α := (F.obj X ⊗ G.obj X :)) (β := fun _ => N.obj X)
      (uncurryApp F κ X).hom (x ⊗ₜ[R.obj X] y) = (κ.app X y).1 (𝟙 X) x := by
  erw [ModuleCat.MonoidalCategory.tensorLift_tmul (R := R.obj X)]
def

uncurry'

L313 ↗
PresheafOfModules.uncurry'
Documentation

The tensor morphism obtained by uncurrying an internal-Hom morphism.

Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section closed

-- Keep the bundled-ring comparison at the same transparency as Mathlib's
-- `PresheafOfModulesOfCommRing.Monoidal.tensorObjMap`.
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}
local instance commRingAt (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (R.obj X))
open InternalHom
Lean source · full declaration
def uncurry' (κ : G ⟶ ihomObj F N) : F ⊗ G ⟶ N where
  app X := uncurryApp F κ X
  naturality {X Y} g := ModuleCat.MonoidalCategory.tensor_ext (fun x y => by
    have hκ := naturality_apply κ g y
    have hev := congrArg
      (fun φ : naturalFamilies F N Y => φ.1 (𝟙 Y) (F.map g x)) hκ
    exact (congrArg (uncurryApp F κ Y) (tensorObj_map_tmul' F (G := G) g x y)).trans
      ((uncurryApp_tmul F κ Y (F.map g x) (G.map g y)).trans
        (hev.trans
          ((ihomObj_map_val F N g (κ.app X y) (𝟙 Y) (F.map g x)).trans
            ((congr_app (κ.app X y)
              ((Category.comp_id g).trans (Category.id_comp g).symm) (F.map g x)).trans
              (((κ.app X y).2 (𝟙 X) g x).symm.trans
                (congrArg (N.map g) (uncurryApp_tmul F κ X x y).symm)))))))
lemma

uncurry'_app_tmul

L328 ↗
PresheafOfModules.uncurry'_app_tmul
Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section closed

-- Keep the bundled-ring comparison at the same transparency as Mathlib's
-- `PresheafOfModulesOfCommRing.Monoidal.tensorObjMap`.
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}
local instance commRingAt (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (R.obj X))
open InternalHom
Lean source · full declaration
lemma uncurry'_app_tmul (κ : G ⟶ ihomObj F N) {X : Cᵒᵖ} (x : F.obj X) (y : G.obj X) :
    DFunLike.coe (α := (F.obj X ⊗ G.obj X :)) (β := fun _ => N.obj X)
      ((uncurry' F κ).app X).hom (x ⊗ₜ[R.obj X] y) = (κ.app X y).1 (𝟙 X) x :=
  uncurryApp_tmul F κ X x y
lemma

uncurry'_curry'

L333 ↗
PresheafOfModules.uncurry'_curry'
Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section closed

-- Keep the bundled-ring comparison at the same transparency as Mathlib's
-- `PresheafOfModulesOfCommRing.Monoidal.tensorObjMap`.
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}
local instance commRingAt (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (R.obj X))
open InternalHom
Lean source · statement
lemma uncurry'_curry' (θ : F ⊗ G ⟶ N) : uncurry' F (curry' F θ) = θ
lemma

curry'_uncurry'

L341 ↗
PresheafOfModules.curry'_uncurry'
Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section closed

-- Keep the bundled-ring comparison at the same transparency as Mathlib's
-- `PresheafOfModulesOfCommRing.Monoidal.tensorObjMap`.
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}
local instance commRingAt (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (R.obj X))
open InternalHom
Lean source · statement
lemma curry'_uncurry' (κ : G ⟶ ihomObj F N) : curry' F (uncurry' F κ) = κ
def

tensorIhomAdj

L350 ↗
PresheafOfModules.tensorIhomAdj
Documentation

The tensor-left and internal-Hom adjunction given by currying and uncurrying.

Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section closed

-- Keep the bundled-ring comparison at the same transparency as Mathlib's
-- `PresheafOfModulesOfCommRing.Monoidal.tensorObjMap`.
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}
local instance commRingAt (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (R.obj X))
open InternalHom
Lean source · statement
def tensorIhomAdj : tensorLeft F ⊣ ihomFunctor F
instance

instMonoidalClosed

L369 ↗
PresheafOfModules.instMonoidalClosed
Source context 7 commands

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

universe u v' u'
open CategoryTheory MonoidalCategory Limits Opposite
namespace PresheafOfModules
section closed

-- Keep the bundled-ring comparison at the same transparency as Mathlib's
-- `PresheafOfModulesOfCommRing.Monoidal.tensorObjMap`.
variable {C : Type u} [Category.{u} C] {R : Cᵒᵖ ⥤ CommRingCat.{u}}
  (F : PresheafOfModules.{u} (R ⋙ forget₂ _ _)) {G N : PresheafOfModules.{u} (R ⋙ forget₂ _ _)}
local instance commRingAt (X : Cᵒᵖ) : CommRing ((R ⋙ forget₂ CommRingCat RingCat).obj X) :=
  inferInstanceAs (CommRing (R.obj X))
open InternalHom
Lean source · full declaration
instance instMonoidalClosed :
    MonoidalClosed (PresheafOfModules.{u} (R ⋙ forget₂ _ _)) where
  closed F := { rightAdj := ihomFunctor F, adj := tensorIhomAdj F }

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