is_compatible_of_exists_amalgamation

English

Suppose R1 ≤ R2 are presieves on X, x ∈ FamilyOfElements P R2, t ∈ P(op X), and ht is an amalgamation of x for t. Then the restricted family x.restrict(h) is an amalgamation of t with respect to R1.

Русский

Пусть R1 ≤ R2 --- предрассыпь на X, x ∈ FamilyOfElements P R2, t ∈ P(op X) и ht амальгамма x для t. Тогда ограниченная совокупность x.restrict(h) является амальгаммой для t относительно R1.

LaTeX

$$(x.IsAmalgamation t) → ((x.restrict h).IsAmalgamation t)$$

Lean4

theorem is_compatible_of_exists_amalgamation (x : FamilyOfElements P R) (h : ∃ t, x.IsAmalgamation t) : x.Compatible :=
  by
  obtain ⟨t, ht⟩ := h
  intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ comm
  rw [← ht _ h₁, ← ht _ h₂, ← FunctorToTypes.map_comp_apply, ← op_comp, comm]
  simp

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