English
If two consecutive strongly Cartesian steps f → f' and g → g' hold with φ', φ'', then the composed map equals the map for the composite base.
Русский
Если два последовательных шага сильно-Картезианских маппингов соблюдают φ' и φ'', тогда отображение-образец композиции совпадает с отображением композиции оснований.
LaTeX
$$$\\text{map\_comp\_map}\\\\{R' R''}\\\\{a' a''} \\,\\\\{f' f''} \\,\\\\{g g'} \\,\\\\{H H'} \\,\\\\{φ' φ''} :\\\\$$
Lean4
/-- When its possible to compare the two, the composition of two `IsStronglyCartesian.map` will also
be given by a `IsStronglyCartesian.map`. In other words, given diagrams
```
a'' a' a --φ--> b
| | | |
v v v v
R'' --g'--> R' --g--> R --f--> S
```
and
```
a' --φ'--> b
| |
v v
R' --f'--> S
```
and
```
a'' --φ''--> b
| |
v v
R'' --f''--> S
```
such that `φ` and `φ'` are strongly Cartesian morphisms, and such that `f' = g ≫ f` and
`f'' = g' ≫ f'`. Then composing the induced map from `a'' ⟶ a'` with the induced map from
`a' ⟶ a` gives the induced map from `a'' ⟶ a`. -/
@[reassoc (attr := simp)]
theorem map_comp_map {R' R'' : 𝒮} {a' a'' : 𝒳} {f' : R' ⟶ S} {f'' : R'' ⟶ S} {g : R' ⟶ R} {g' : R'' ⟶ R'}
(H : f' = g ≫ f) (H' : f'' = g' ≫ f') (φ' : a' ⟶ b) (φ'' : a'' ⟶ b) [IsStronglyCartesian p f' φ']
[IsHomLift p f'' φ''] :
map p f' φ' H' φ'' ≫ map p f φ H φ' = map p f φ (show f'' = (g' ≫ g) ≫ f by rwa [assoc, ← H]) φ'' :=
by
apply map_uniq p f φ
simp only [assoc, fac]
