instSubsingletonSMulCandidate — Mathlib

English

There is a unique SMulCandidate given the data, following from the subsingleton property.

Русский

Существует единственный SMulCandidate при данных данных, следует из свойства одиночности.

LaTeX

$$$ \text{Unique } (SMulCandidate α φ r m) $$$

Lean4

instance : Subsingleton (SMulCandidate α φ r m) where
  allEq := by
    rintro ⟨x₁, h₁⟩ ⟨x₂, h₂⟩
    simp only [SMulCandidate.mk.injEq]
    let S := (Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m)
    have hS : S ∈ J _ := by
      apply J.intersection_covering
      all_goals apply Presheaf.imageSieve_mem
    apply A.isSeparated _ _ hS
    intro Y f ⟨⟨r₀, hr₀⟩, ⟨m₀, hm₀⟩⟩
    rw [h₁ f.op r₀ hr₀ m₀ hm₀, h₂ f.op r₀ hr₀ m₀ hm₀]

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