Theorems · Definition · order theory

Function.mapPullback

{X₁ : Type u_1} →
  {X₂ : Type u_2} →
    {Y₁ : Sort u_3} →
      {Y₂ : Sort u_4} →
        {Z₁ : Type u_5} →
          {Z₂ : Type u_6} →
            {f₁ : X₁ → Y₁} →
              {g₁ : Z₁ → Y₁} →
                {f₂ : X₂ → Y₂} →
                  {g₂ : Z₂ → Y₂} →
                    (mapX : X₁ → X₂) →
                      (mapY : Y₁ → Y₂) →
                        (mapZ : Z₁ → Z₂) →
                          f₂ ∘ mapX = mapY ∘ f₁ →
                            g₂ ∘ mapZ = mapY ∘ g₁ → Function.Pullback f₁ g₁ → Function.Pullback f₂ g₂

Three functions between the three pairs of spaces $X_i, Y_i, Z_i$ that are compatible induce a function $X_1 \times_{Y_1} Z_1 \to X_2 \times_{Y_2} Z_2$.

Defined in

Mathlib.Data.Set.Prod

Cited by

2 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms