English
The full subcategory induced by the filtered closure of a family of objects is filtered and small.
Русский
Полная подкатегория, индуцированная фильтрованной замыкостью семейства объектов, является фильтрованной и мелкой.
LaTeX
$$$[\text{IsFilteredOrEmpty}(C)] (f : \alpha \to C) \Rightarrow \text{Small}(\text{filteredClosure } f).\text{FullSubcategory}$$$
Lean4
theorem small_fullSubcategory_filteredClosure : Small.{max v w} (filteredClosure f).FullSubcategory :=
by
refine
small_of_injective_of_exists (FilteredClosureSmall.abstractFilteredClosureRealization f)
(fun _ _ => ObjectProperty.FullSubcategory.ext) ?_
rintro ⟨j, h⟩
induction h with
| base x =>
refine ⟨⟨0, ?_⟩, ?_⟩
· simp only [FilteredClosureSmall.bundledAbstractFilteredClosure]
exact ULift.up x
· simp only [FilteredClosureSmall.abstractFilteredClosureRealization]
rw! [FilteredClosureSmall.bundledAbstractFilteredClosure]
rfl
| max hj₁ hj₂ ih ih' =>
rcases ih with ⟨⟨n, x⟩, rfl⟩
rcases ih' with ⟨⟨m, y⟩, rfl⟩
refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
· simp only [FilteredClosureSmall.bundledAbstractFilteredClosure]
refine FilteredClosureSmall.InductiveStep.max ?_ ?_ x y
all_goals apply Nat.lt_succ_of_le
exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]
· simp only [FilteredClosureSmall.abstractFilteredClosureRealization]
rw! [FilteredClosureSmall.bundledAbstractFilteredClosure]
rfl
| coeq hj₁ hj₂ g g' ih ih' =>
rcases ih with ⟨⟨n, x⟩, rfl⟩
rcases ih' with ⟨⟨m, y⟩, rfl⟩
refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
· simp only [FilteredClosureSmall.bundledAbstractFilteredClosure]
refine FilteredClosureSmall.InductiveStep.coeq ?_ ?_ x y g g'
all_goals apply Nat.lt_succ_of_le
exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]
· simp only [FilteredClosureSmall.abstractFilteredClosureRealization]
rw! [FilteredClosureSmall.bundledAbstractFilteredClosure]
rfl
