Collapsing covers

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

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

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

Equations

• 𝒰.sigma = { I₀ := PUnit.{?u.34 + 1}, X := fun (x : PUnit.{?u.34 + 1}) => ∐ 𝒰.X, f := fun (x : PUnit.{?u.34 + 1}) => CategoryTheory.Limits.Sigma.desc 𝒰.f, mem₀ := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.sigma_I₀ {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsZariskiLocalAtSource P] [UnivLE.{v, u}] (𝒰 : Cover (precoverage P) S) : 𝒰.sigma.I₀ = PUnit.{v + 1}

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.sigma_f {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsZariskiLocalAtSource P] [UnivLE.{v, u}] (𝒰 : Cover (precoverage P) S) (x✝ : PUnit.{v + 1}) : 𝒰.sigma.f x✝ = CategoryTheory.Limits.Sigma.desc 𝒰.f

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.sigma_X {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsZariskiLocalAtSource P] [UnivLE.{v, u}] (𝒰 : Cover (precoverage P) S) (x✝ : PUnit.{v + 1}) : 𝒰.sigma.X x✝ = ∐ 𝒰.X

instance AlgebraicGeometry.Scheme.Cover.instUniqueI₀Sigma {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsZariskiLocalAtSource P] [UnivLE.{v, u}] (𝒰 : Cover (precoverage P) S) : Unique 𝒰.sigma.I₀

Equations

• 𝒰.instUniqueI₀Sigma = inferInstanceAs (Unique PUnit.{?u.34 + 1})

noncomputable def AlgebraicGeometry.Scheme.Cover.toSigma {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsZariskiLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] (𝒰 : Cover (precoverage P) S) : 𝒰 ⟶ 𝒰.sigma

𝒰 refines the single object cover defined by 𝒰.

Equations

• 𝒰.toSigma = { idx := fun (x : 𝒰.I₀) => default, app := fun (i : 𝒰.I₀) => CategoryTheory.Limits.Sigma.ι 𝒰.X i, app_prop := ⋯, w := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.toSigma_app {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsZariskiLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] (𝒰 : Cover (precoverage P) S) (i : 𝒰.I₀) : 𝒰.toSigma.app i = CategoryTheory.Limits.Sigma.ι 𝒰.X i

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.toSigma_idx {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsZariskiLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] (𝒰 : Cover (precoverage P) S) (x✝ : 𝒰.I₀) : 𝒰.toSigma.idx x✝ = default

noncomputable def AlgebraicGeometry.Scheme.Cover.Hom.sigma {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsZariskiLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] {𝒰 𝒱 : Cover (precoverage 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.

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.Hom.sigma_idx {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsZariskiLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] {𝒰 𝒱 : Cover (precoverage P) S} (f : 𝒰 ⟶ 𝒱) (x✝ : 𝒰.sigma.I₀) : (sigma f).idx x✝ = default

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.Hom.sigma_app {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsZariskiLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] {𝒰 𝒱 : Cover (precoverage P) S} (f : 𝒰 ⟶ 𝒱) (x✝ : 𝒰.sigma.I₀) : (sigma f).app x✝ = CategoryTheory.Limits.Sigma.desc fun (j : 𝒰.I₀) => CategoryTheory.CategoryStruct.comp (f.app j) (CategoryTheory.Limits.Sigma.ι 𝒱.X (f.idx j))

noncomputable def AlgebraicGeometry.Scheme.Cover.sigmaFunctor {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsZariskiLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] : CategoryTheory.Functor (Cover (precoverage P) S) (Cover (precoverage 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.

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.sigmaFunctor_obj {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsZariskiLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] (𝒰 : Cover (precoverage P) S) : sigmaFunctor.obj 𝒰 = 𝒰.sigma

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.sigmaFunctor_map {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} [IsZariskiLocalAtSource P] [UnivLE.{v, u}] [P.IsMultiplicative] {X✝ Y✝ : Cover (precoverage P) S} (f : X✝ ⟶ Y✝) : sigmaFunctor.map f = Hom.sigma f