Theorems · Definition · category theory

ComplexShape.Embedding.AreComplementary.equiv

{ι : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      {c : ComplexShape ι} →
        {c₁ : ComplexShape ι₁} →
          {c₂ : ComplexShape ι₂} → {e₁ : c₁.Embedding c} → {e₂ : c₂.Embedding c} → e₁.AreComplementary e₂ → ι₁ ⊕ ι₂ ≃ ι

Given complementary embeddings of complex shapes e₁ : Embedding c₁ c and e₂ : Embedding c₂ c, this is the obvious bijection ι₁ ⊕ ι₂ ≃ ι from the sum of the index types of c₁ and c₂ to the index type of c.

Defined in

Mathlib.Algebra.Homology.Embedding.AreComplementary

Cited by

7 results in Mathlib

Foundations

Depth 13 from the axioms · uses Classical.choice