isLocallyInjective_iff_equalizerSieve_mem_imp

English

Extends the local fullness property along larger categorical structures using the WEqualsLocallyBijective framework.

Русский

Расширяем локальную полноту по более крупным категориальным структурам через систему WEqualsLocallyBijective.

LaTeX

$$$\text{IsLocallyFull}(G,K)\text{ extended by }WEqualsLocallyBijective$$$

Lean4

theorem isLocallyInjective_iff_equalizerSieve_mem_imp :
    IsLocallyInjective J φ ↔
      ∀ ⦃X : Cᵒᵖ⦄ (x y : ToType (F₁.obj X)),
        equalizerSieve (φ.app _ x) (φ.app _ y) ∈ J X.unop → equalizerSieve x y ∈ J X.unop :=
  by
  constructor
  · intro _ X x y h
    let S := equalizerSieve (φ.app _ x) (φ.app _ y)
    let T : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X.unop⦄ (_ : S f), Sieve Y := fun Y f _ =>
      equalizerSieve (F₁.map f.op x) ((F₁.map f.op y))
    refine J.superset_covering ?_ (J.transitive h (Sieve.bind S.1 T) ?_)
    · rintro Y f ⟨Z, a, g, hg, ha, rfl⟩
      simpa using ha
    · intro Y f hf
      refine J.superset_covering (Sieve.le_pullback_bind S.1 T _ hf) (equalizerSieve_mem J φ _ _ ?_)
      rw [NatTrans.naturality_apply, NatTrans.naturality_apply]
      exact hf
  · intro hφ
    exact ⟨fun {X} x y h => hφ x y (by simp [h])⟩

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