English
A strongly cocartesian arrow lying over an isomorphism is itself an isomorphism. If φ: a → b is strongly cocartesian over an isomorphism f: R ≅ S, then φ is an isomorphism.
Русский
Строго когартезианная стрелка над изоморфизмом является изоморфизмом. Если φ над изоморфизмом f, то φ — изоморфизм.
LaTeX
$$$[IsStronglyCocartesian\ p\ f\ φ] \land [IsIso\ f] \Rightarrow IsIso\ φ$$$
Lean4
/-- Given two commutative squares
```
a --φ--> b --ψ--> c
| | |
v v v
R --f--> S --g--> T
```
such that `φ ≫ ψ` and `φ` are strongly co-Cartesian, then so is `ψ`. -/
protected theorem of_comp [IsStronglyCocartesian p f φ] [IsStronglyCocartesian p (f ≫ g) (φ ≫ ψ)] [IsHomLift p g ψ] :
IsStronglyCocartesian p g ψ where
universal_property' := by
intro c' h τ hτ
use map p (f ≫ g) (φ ≫ ψ) (f' := f ≫ g ≫ h) (assoc f g h).symm (φ ≫ τ)
refine
⟨⟨inferInstance, ?_⟩, ?_⟩
/- The fact that `ψ ≫ π = τ` follows from `φ ≫ ψ ≫ π = φ ≫ τ` and the universal property of
`φ`. -/
·
apply
IsStronglyCocartesian.ext p f φ (g ≫ h) <| by
simp only [← assoc, fac]
-- Finally, uniqueness of `π` comes from the universal property of `φ ≫ ψ`.
· intro π' ⟨hπ'₁, hπ'₂⟩
apply map_uniq
simp [hπ'₂.symm]
