Documentation

Mathlib.AlgebraicGeometry.Cover.Sigma

Collapsing covers #

We define the endofunctor on Scheme.Cover P that collapses a cover to a single object cover.

source
noncomputable def AlgebraicGeometry.Scheme.Cover.sigma {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsLocalAtSource P] [UnivLE.{v, u}] (𝒰 : Cover P S) :
Cover P S

If 𝒰 is a cover of S, this is the single object cover where the covering object is the disjoint union.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Cover.sigma_J {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsLocalAtSource P] [UnivLE.{v, u}] (𝒰 : Cover P S) :
    𝒰.sigma.J = PUnit.{v + 1}
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Cover.sigma_obj {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsLocalAtSource P] [UnivLE.{v, u}] (𝒰 : Cover P S) (x✝ : PUnit.{v + 1}) :
    𝒰.sigma.obj x✝ = ∐ 𝒰.obj
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Cover.sigma_f {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsLocalAtSource P] [UnivLE.{v, u}] (𝒰 : Cover P S) (x✝ : ↥S) :
    𝒰.sigma.f x✝ = default
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Cover.sigma_map {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsLocalAtSource P] [UnivLE.{v, u}] (𝒰 : Cover P S) (x✝ : PUnit.{v + 1}) :
    𝒰.sigma.map x✝ = CategoryTheory.Limits.Sigma.desc 𝒰.map
    source
    instance AlgebraicGeometry.Scheme.Cover.instUniqueJSigma {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsLocalAtSource P] [UnivLE.{v, u}] (𝒰 : Cover P S) :
    Unique 𝒰.sigma.J
    Equations
    source
    noncomputable def AlgebraicGeometry.Scheme.Cover.toSigma {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] (𝒰 : Cover P S) :
    𝒰 ⟶ 𝒰.sigma

    𝒰 refines the single object cover defined by 𝒰.

    Equations
    Instances For
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.Cover.toSigma_idx {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] (𝒰 : Cover P S) (x✝ : 𝒰.J) :
      𝒰.toSigma.idx x✝ = default
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.Cover.toSigma_app {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] (𝒰 : Cover P S) (i : 𝒰.J) :
      𝒰.toSigma.app i = CategoryTheory.Limits.Sigma.ι 𝒰.obj i
      source
      noncomputable def AlgebraicGeometry.Scheme.Cover.Hom.sigma {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] {𝒰 𝒱 : Cover P S} (f : 𝒰 ⟶ 𝒱) :
      𝒰.sigma ⟶ 𝒱.sigma

      A refinement of coverings induces a refinement on the single object coverings.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.Cover.Hom.sigma_idx {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] {𝒰 𝒱 : Cover P S} (f : 𝒰 ⟶ 𝒱) (x✝ : 𝒰.sigma.J) :
        (sigma f).idx x✝ = default
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.Cover.Hom.sigma_app {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] {𝒰 𝒱 : Cover P S} (f : 𝒰 ⟶ 𝒱) (x✝ : 𝒰.sigma.J) :
        (sigma f).app x✝ = CategoryTheory.Limits.Sigma.desc fun (j : 𝒰.J) => CategoryTheory.CategoryStruct.comp (f.app j) (CategoryTheory.Limits.Sigma.ι 𝒱.obj (f.idx j))
        source
        noncomputable def AlgebraicGeometry.Scheme.Cover.sigmaFunctor {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] :
        CategoryTheory.Functor (Cover P S) (Cover P S)

        Collapsing a cover to a single object cover is functorial.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem AlgebraicGeometry.Scheme.Cover.sigmaFunctor_obj {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] (𝒰 : Cover P S) :
          sigmaFunctor.obj 𝒰 = 𝒰.sigma
          source
          @[simp]
          theorem AlgebraicGeometry.Scheme.Cover.sigmaFunctor_map {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] {X✝ Y✝ : Cover P S} (f : X✝ ⟶ Y✝) :
          sigmaFunctor.map f = Hom.sigma f