Nyll.EtaleFundamentalGroups.FiniteEtale.InternalHom

Module documentation

Finite étale internal Hom

Stacks Project, Tag 0BL7: the relative internal Hom of two finite étale schemes is represented by a finite étale scheme. Its pullback represents the internal Hom of the pulled-back schemes after every base change.

The statement uses the usual product functor on Over S and Yoneda. The construction and its local-to-global proofs live in SchemeTheory.

theorem

exists_internalHom

L36 ↗

AlgebraicGeometry.FiniteEtale.exists_internalHom

Documentation

The internal Hom of finite étale schemes is finite étale, compatibly with arbitrary base change.

Source context 4 commands

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

@[expose] public section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem exists_internalHom (S : Scheme.{u}) (U V : FiniteEtale S) :
    ∃ W : FiniteEtale S,
      Nonempty
        (((MonoidalCategory.tensorRight ((FiniteEtale.forget S).obj U)).op ⋙
          yoneda.obj ((FiniteEtale.forget S).obj V)).RepresentableBy
            ((FiniteEtale.forget S).obj W)) ∧
      ∀ (T : Scheme.{u}) (f : T ⟶ S),
        Nonempty
          (((MonoidalCategory.tensorRight
            ((FiniteEtale.forget T).obj ((FiniteEtale.pullback f).obj U))).op ⋙
              yoneda.obj ((FiniteEtale.forget T).obj ((FiniteEtale.pullback f).obj
                V))).RepresentableBy
                ((FiniteEtale.forget T).obj ((FiniteEtale.pullback f).obj W)))

Module documentation

Finite étale internal Hom

Declarations

exists_internalHom