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
    Instances For
      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
      @[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
      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
              Instances For
                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
                @[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
                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
                  Instances For
                    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
                    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