compatibleEquivGenerateSieveCompatible

English

If x is a compatible family and f is a morphism of presheaves P → Q, then the image x.map f is compatible.

Русский

Если x — совместимое семейство, и f — морфизм праформ, тогда изображение x.map f совместимо.

LaTeX

$$$\\text{theorem } map(f) : x.Compatible \\Rightarrow (x.map f).Compatible$$$

Lean4

/-- Compatible families of elements for a presheaf of types `P` and a presieve `R`
are in 1-1 correspondence with compatible families for the same presheaf and
the sieve generated by `R`, through extension and restriction. -/
@[simps]
noncomputable def compatibleEquivGenerateSieveCompatible :
    { x : FamilyOfElements P R // x.Compatible } ≃ { x : FamilyOfElements P (generate R : Presieve X) // x.Compatible }
    where
  toFun x := ⟨x.1.sieveExtend, x.2.sieveExtend⟩
  invFun x := ⟨x.1.restrict (le_generate R), x.2.restrict _⟩
  left_inv x := Subtype.ext (restrict_extend x.2)
  right_inv x := Subtype.ext (extend_restrict x.2)

Похожие утверждения