unique_nonDegenerate_dim — Mathlib

English

If two representations of the same x by non-degenerate data exist, their target dimensions coincide.

Русский

Если два представления одного и того же x через недегенеративные данные существуют, целевые размерности совпадают.

LaTeX

$$$ \forall x, \exists f_1, \exists f_2: \text{epi}, x = X.map f_1.op y_1 = X.map f_2.op y_2 \Rightarrow m_1 = m_2 $$$

Lean4

theorem unique_nonDegenerate_dim (x : X _⦋n⦌) {m₁ m₂ : ℕ} (f₁ : ⦋n⦌ ⟶ ⦋m₁⦌) [Epi f₁] (y₁ : X.nonDegenerate m₁)
    (hy₁ : x = X.map f₁.op y₁) (f₂ : ⦋n⦌ ⟶ ⦋m₂⦌) [Epi f₂] (y₂ : X.nonDegenerate m₂) (hy₂ : x = X.map f₂.op y₂) :
    m₁ = m₂ := by
  obtain ⟨⟨hf₁⟩⟩ := isSplitEpi_of_epi f₁
  obtain ⟨⟨hf₂⟩⟩ := isSplitEpi_of_epi f₂
  exact le_antisymm (le hf₁ hy₁ hy₂) (le hf₂ hy₂ hy₁)

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