Common refinements of covering families

This file provides the cover-theoretic common refinement construction used by local trivializations. It reuses Mathlib's GrothendieckTopology.intersection_covering theorem; no formalization is vendored.

structure CategoryTheory.GrothendieckTopology.CoversTop.CommonRefinement {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {I₁ : Type u_1} {I₂ : Type u_2} (X₁ : I₁ → C) (X₂ : I₂ → C) : Type (max (max (max (u + 1) u_1) u_2) v)

A common refinement of two covering families.

Each object in the refined family admits arrows to one member of each original family.

• I : Type u

  The indexing type of the common refinement.

• X : self.I → C

  The objects in the common refinement.

• leftIndex : self.I → I₁

  The member of the first covering family above each refined object.

• left (i : self.I) : self.X i ⟶ X₁ (self.leftIndex i)

  The arrow from each refined object to its member of the first covering family.

• rightIndex : self.I → I₂

  The member of the second covering family above each refined object.

• right (i : self.I) : self.X i ⟶ X₂ (self.rightIndex i)

  The arrow from each refined object to its member of the second covering family.

• coversTop : J.CoversTop self.X

  The refined family covers the top.

noncomputable def CategoryTheory.GrothendieckTopology.CoversTop.commonRefinement {C : Type u} [Category.{v, u} C] {I₁ : Type u_1} {I₂ : Type u_2} {X₁ : I₁ → C} {X₂ : I₂ → C} {J : GrothendieckTopology C} (h₁ : J.CoversTop X₁) (h₂ : J.CoversTop X₂) : CommonRefinement J X₁ X₂

Construct a common refinement of two covering families.

The refined family is indexed by the objects admitting arrows to a member of each original family. Its covering property follows by applying intersection_covering to the two original sieves and then enlarging that intersection to the sieve generated by the refined family.

Equations

• One or more equations did not get rendered due to their size.