English
A locally-faithful and cover-dense functor preserves compatible families; i.e., compatibility of families is preserved under the pushforward/pullback through G.
Русский
Локально полный и плотный функтор сохраняет совместимые семейства; совместимость сохраняется при отображении через G.
LaTeX
$$$\mathrm{CompatiblePreserving}(K,G).$$$
Lean4
/-- A locally-fully-faithful and cover-dense functor preserves compatible families. -/
theorem compatiblePreserving [G.IsLocallyFaithful K] : CompatiblePreserving K G :=
by
constructor
intro ℱ Z T x hx Y₁ Y₂ X f₁ f₂ g₁ g₂ hg₁ hg₂ eq
apply Functor.IsCoverDense.ext G
intro W i
refine IsLocallyFull.ext G _ (i ≫ f₁) fun V₁ iVW iV₁Y₁ e₁ ↦ ?_
refine IsLocallyFull.ext G _ (G.map iVW ≫ i ≫ f₂) fun V₂ iV₂V₁ iV₂Y₂ e₂ ↦ ?_
refine IsLocallyFaithful.ext G _ (iV₂V₁ ≫ iV₁Y₁ ≫ g₁) (iV₂Y₂ ≫ g₂) (by simp [e₁, e₂, eq]) ?_
intro V₃ iV₃ e₄
simp only [← op_comp, ← FunctorToTypes.map_comp_apply, ← e₁, ← e₂, ← Functor.map_comp]
apply hx
simpa using e₄
