English
Two triples (T1, p) and (T2, q) in the pullback carrier are equal if and only if there exists an equality e: T1 = T2 such that mapping along tensorCongr(e) relates the two Spec components. This is a characterization of equality in the pullback carrier via a base-map equality and a tensor congruence.
Русский
Два элемента пары в носителе схеми-pullback равны тогда и только тогда, когда существует равенство e: T1 = T2, такое что отображение через tensorCongr(e) связывает соответствующие компоненты Spec.
LaTeX
$$$T_1 = T_2 \;\Leftrightarrow\; \exists e: T_1.1 = T_2.1, (\mathrm{Spec.map} (\mathrm{Triplet.tensorCongr} e).inv).base T_1.2 = T_2.2$$$
Lean4
/-- A helper lemma to work with `AlgebraicGeometry.Scheme.Pullback.carrierEquiv`. -/
theorem carrierEquiv_eq_iff {T₁ T₂ : Σ T : Triplet f g, Spec T.tensor} :
T₁ = T₂ ↔ ∃ e : T₁.1 = T₂.1, (Spec.map (Triplet.tensorCongr e).inv).base T₁.2 = T₂.2 :=
by
constructor
· rintro rfl
simp
· obtain ⟨T, _⟩ := T₁
obtain ⟨T', _⟩ := T₂
rintro ⟨rfl : T = T', e⟩
simpa [e]
