English
If two SMulCandidates agree on restrictions to overlaps, they are equal; hence SMulCandidate is singleton up to equivalence.
Русский
Если два SMulCandidate совпадают на пересечьиях, они равны; значит SMulCandidate является синглтоном.
LaTeX
$$$ \text{Subsingleton } (SMulCandidate α φ r m) $$$
Lean4
instance : Nonempty (SMulCandidate α φ r m) :=
⟨by
let S := (Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m)
have hS : S ∈ J _ := by
apply J.intersection_covering
all_goals apply Presheaf.imageSieve_mem
have h₁ : S ≤ Presheaf.imageSieve α r := fun _ _ h => h.1
have h₂ : S ≤ Presheaf.imageSieve φ m := fun _ _ h => h.2
let r₀ := (Presieve.FamilyOfElements.localPreimage (whiskerRight α (forget _)) r).restrict h₁
let m₀ := (Presieve.FamilyOfElements.localPreimage (whiskerRight φ (forget _)) m).restrict h₂
have hr₀ : (r₀.map (whiskerRight α (forget _))).IsAmalgamation r :=
by
rw [Presieve.FamilyOfElements.restrict_map]
apply Presieve.isAmalgamation_restrict
apply Presieve.FamilyOfElements.isAmalgamation_map_localPreimage
have hm₀ : (m₀.map (whiskerRight φ (forget _))).IsAmalgamation m :=
by
rw [Presieve.FamilyOfElements.restrict_map]
apply Presieve.isAmalgamation_restrict
apply Presieve.FamilyOfElements.isAmalgamation_map_localPreimage
exact
SMulCandidate.mk' α φ r m S hS r₀ m₀ hr₀ hm₀ _
(Presieve.IsSheafFor.isAmalgamation (((sheafCompose J (forget _)).obj A).2.isSheafFor S hS)
(Presieve.FamilyOfElements.isCompatible_map_smul α φ A.isSeparated r m r₀ m₀ hr₀ hm₀))⟩
