closure_range_union_range_eq_top_of_isPushout

English

If a pushout square exists, then the closure of the union of the ranges of the two structure maps equals the top element in the relevant subring lattice.

Русский

Если задан пуш-аут, то замыкание объединения образов двух отображений в соответствующей частичной структуре кольца равно топу.

LaTeX

$$$\operatorname{closure}(\mathrm{range}(a) \cup \mathrm{range}(b)) = \top$$$

Lean4

theorem closure_range_union_range_eq_top_of_isPushout {R A B X : CommRingCat.{u}} {f : R ⟶ A} {g : R ⟶ B} {a : A ⟶ X}
    {b : B ⟶ X} (H : IsPushout f g a b) : Subring.closure (Set.range a ∪ Set.range b) = ⊤ :=
  by
  algebraize [f.hom, g.hom]
  let e := ((isPushout_tensorProduct R A B).isoIsPushout _ _ H).commRingCatIsoToRingEquiv
  rw [← Subring.comap_map_eq_self_of_injective e.symm.injective (.closure _), RingHom.map_closure, ← top_le_iff, ←
    Subring.map_le_iff_le_comap, Set.image_union]
  simp only [AlgHom.toRingHom_eq_coe, ← Set.range_comp, ← RingHom.coe_comp]
  rw [← hom_comp, ← hom_comp, IsPushout.inl_isoIsPushout_inv, IsPushout.inr_isoIsPushout_inv, hom_ofHom, hom_ofHom]
  exact le_top.trans (Algebra.TensorProduct.closure_range_union_range_eq_top R A B).ge

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