refine — Mathlib

English

Refine a Meq witness along a refinement e: S ⟶ T of covers to obtain a more refined witness over S.

Русский

Уточнить свидетельство Meq вдоль уточнения e: S ⟶ T покрытий, получил более точное свидетельство над S.

LaTeX

$$$\text{refine}(x,e):\ Meq P S$$$

Lean4

/-- Refine a term of `Meq P T` with respect to a refinement `S ⟶ T` of covers. -/
def refine {X : C} {P : Cᵒᵖ ⥤ D} {S T : J.Cover X} (x : Meq P T) (e : S ⟶ T) : Meq P S :=
  ⟨fun I => x ⟨I.Y, I.f, (leOfHom e) _ I.hf⟩, fun I =>
    x.condition (GrothendieckTopology.Cover.Relation.mk' (I.r.map e))⟩

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