English
Constructs a CodescendsAlong instance from given hypotheses h1 and h2, encoding the transfer of properties along a pushout-like construction.
Русский
Строит экземпляр CodescendsAlong из данных гипотез, кодируя перенос свойств вдоль конструкции, подобной пушауту.
LaTeX
$$$\text{CodescendsAlong.mk}(h_1,h_2) := \text{построение экземпляра}.$$$
Lean4
theorem mk (h₁ : RespectsIso P)
(h₂ :
∀ ⦃R S T⦄ [CommRing R] [CommRing S] [CommRing T],
∀ [Algebra R S] [Algebra R T], Q (algebraMap R S) → P (algebraMap S (S ⊗[R] T)) → P (algebraMap R T)) :
CodescendsAlong P Q := by
introv R h hQ H
let e := h.symm.equiv
have : (e.symm : _ →+* _).comp (algebraMap R' S') = algebraMap R' (R' ⊗[R] S) :=
by
ext r
simp [e]
apply h₂ hQ
rw [← this]
exact h₁.1 _ _ H
