isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor

English

A criterion equates isSeparatedFor with existence of amalgamations: P is separated for R and every compatible family has an amalgamation iff P is isSheafFor R.

Русский

Критерий: раздельность вместе с существованием амальгамм означает выполнение условия sheaf.

LaTeX

$$(IsSeparatedFor P R ∧ ∀ x, x.Compatible → ∃ t, x.IsAmalgamation t) ↔ IsSheafFor P R$$

Lean4

/-- `P` is a sheaf for `R` iff it is separated for `R` and there exists an amalgamation. -/
theorem isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor :
    (IsSeparatedFor P R ∧ ∀ x : FamilyOfElements P R, x.Compatible → ∃ t, x.IsAmalgamation t) ↔ IsSheafFor P R :=
  by
  rw [IsSeparatedFor, ← forall_and]
  apply forall_congr'
  intro x
  constructor
  · intro z hx
    exact existsUnique_of_exists_of_unique (z.2 hx) z.1
  · intro h
    refine ⟨?_, ExistsUnique.exists ∘ h⟩
    intro t₁ t₂ ht₁ ht₂
    apply (h _).unique ht₁ ht₂
    exact is_compatible_of_exists_amalgamation x ⟨_, ht₂⟩

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