compatible_singleton_iff — Mathlib

English

The equivalence respects sieveExtend on compatible families; restricting then extending yields the same data.

Русский

Эквивалентность сохраняется при расширении через sieveExtend для совместимых семейств.

LaTeX

$$$\\langle x.1.restrict\\dots x.2, \\dots\\rangle$ is an equivalence preserving sieveExtend$$

Lean4

theorem compatible_singleton_iff {X Y : C} (f : X ⟶ Y) (x : (singleton f).FamilyOfElements P) :
    x.Compatible ↔ ∀ {Z : C} (p₁ p₂ : Z ⟶ X), p₁ ≫ f = p₂ ≫ f → P.map p₁.op (x f ⟨⟩) = P.map p₂.op (x f ⟨⟩) :=
  by
  refine ⟨fun H Z p₁ p₂ h ↦ H _ _ _ _ h, fun H Y₁ Y₂ Z g₁ g₂ f₁ f₂ ↦ ?_⟩
  rintro ⟨rfl⟩ ⟨rfl⟩ h
  exact H _ _ h

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