nontrivial_of_isPushout_of_isField

English

Let A be a field, and f: A → B, g: A → C with B and C nontrivial. If D is a pushout of f and g, then D is nontrivial.

Русский

Пусть A – поле, f: A → B, g: A → C, причем B и C не тривиальны. Если D является гранично-обобщенным графом (пуш-аутом) для f и g, то D не тривиален.

LaTeX

$$$\text{IsField}(A) \;\Rightarrow\; \Big(\text{IsPushout}(f,g,inl,inr) \rightarrow (\text{Nontrivial}(B) \wedge \text{Nontrivial}(C) \rightarrow \text{Nontrivial}(D))\Big)$$$

Lean4

theorem nontrivial_of_isPushout_of_isField {A B C D : CommRingCat.{u}} (hA : IsField A) {f : A ⟶ B} {g : A ⟶ C}
    {inl : B ⟶ D} {inr : C ⟶ D} [Nontrivial B] [Nontrivial C] (h : IsPushout f g inl inr) : Nontrivial D :=
  by
  letI : Field A := hA.toField
  algebraize [f.hom, g.hom]
  let e : D ≅ .of (B ⊗[A] C) :=
    IsColimit.coconePointUniqueUpToIso h.isColimit (CommRingCat.pushoutCoconeIsColimit A B C)
  let e' : D ≃ B ⊗[A] C := e.commRingCatIsoToRingEquiv.toEquiv
  exact e'.nontrivial

Похожие утверждения