English
For X,Y,Z and f,g with IsIso f, IsOpenEmbedding (f ≫ g) iff IsOpenEmbedding g.
Русский
Для X,Y,Z и f,g с IsIso f, IsOpenEmbedding (f ≫ g) эквивалентно IsOpenEmbedding g.
LaTeX
$$$\\mathrm{IsOpenEmbedding}(f \\;\\mathrm{≫}\\; g) \\iff \\mathrm{IsOpenEmbedding}(g)$ при $IsIso(f)$$$
Lean4
/-- Implementation: If `π` is a morphism in `TopCat` which is a quotient map, then it is an effective
epimorphism. The theorem `TopCat.effectiveEpi_iff_isQuotientMap` should be used instead of
this definition.
-/
noncomputable def effectiveEpiStructOfQuotientMap {B X : TopCat.{u}} (π : X ⟶ B) (hπ : IsQuotientMap π) :
EffectiveEpiStruct π where
/- `IsQuotientMap.lift` gives the required morphism -/
desc e
h :=
ofHom <|
hπ.lift e.hom fun a b hab ↦
CategoryTheory.congr_fun
(h (ofHom ⟨fun _ ↦ a, continuous_const⟩) (ofHom ⟨fun _ ↦ b, continuous_const⟩) (by ext; exact hab)) a
fac e
h :=
hom_ext
(hπ.lift_comp e.hom fun a b hab ↦
CategoryTheory.congr_fun
(h (ofHom ⟨fun _ ↦ a, continuous_const⟩) (ofHom ⟨fun _ ↦ b, continuous_const⟩) (by ext; exact hab)) a)
/- Uniqueness follows from the fact that `IsQuotientMap.lift` is an equivalence (given by
`IsQuotientMap.liftEquiv`). -/
uniq e h g
hm :=
by
suffices
g =
ofHom
(hπ.liftEquiv
⟨e.hom, fun a b hab ↦
CategoryTheory.congr_fun
(h (ofHom ⟨fun _ ↦ a, continuous_const⟩) (ofHom ⟨fun _ ↦ b, continuous_const⟩) (by ext; exact hab)) a⟩)
by assumption
apply hom_ext
rw [hom_ofHom, ← Equiv.symm_apply_eq hπ.liftEquiv]
ext
simp only [IsQuotientMap.liftEquiv_symm_apply_coe, ContinuousMap.comp_apply, ← hm]
rfl
