Module

Congr.lean

Nyll.SchemeTheory.WeilRestriction.Congr

1 declaration indexed from sourceView source ↗

Module documentation

Changing the arguments of relative internal Hom

Isomorphisms of the source and target induce a natural isomorphism of relative internal Hom presheaves. This identifies geometric pullbacks with their affine tensor-product presentations when constructing local representers.

Imports3

Nyll.SchemeTheory.WeilRestriction.Sheaf
Mathlib.CategoryTheory.Monoidal.Category
Mathlib.CategoryTheory.Yoneda

Imported by3

def

relativeInternalHomIso

L33 ↗

SchemeTheory.WeilRestriction.relativeInternalHomIso

Documentation

Relative internal Hom is contravariant in its source and covariant in its target.

Source context 5 commands

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

@[expose] public section
open CategoryTheory AlgebraicGeometry
noncomputable section
universe u
namespace SchemeTheory.WeilRestriction

Lean source · statement

def relativeInternalHomIso {S : Scheme.{u}} {U U' V V' : Over S}
    (eU : U ≅ U') (eV : V ≅ V') :
    relativeInternalHomFunctor U V ≅ relativeInternalHomFunctor U' V'

Module documentation

Changing the arguments of relative internal Hom

Declarations

relativeInternalHomIso