English
Pullback of IsDomain along an injective function: if α is a domain and there exists an injective hom from β to α preserving structure, then β is a domain.
Русский
Вытягивание свойства интеграла по инъективной функции: если α — домен, существует инъективное гомоморфизм β в α, сохраняющий структуру, значит β — домен.
LaTeX
$$$[ \text{Semiring } \alpha] [\text{IsDomain } \alpha] [\text{Semiring } \beta]\; \big( f: F \big) \;\big( \text{hf}: \operatorname{Injective} f \big) \Rightarrow \operatorname{IsDomain}(\beta)$$$
Lean4
/-- Pullback `IsDomain` instance along an injective function. -/
protected theorem isDomain [Semiring α] [IsDomain α] [Semiring β] {F} [FunLike F β α] [MonoidWithZeroHomClass F β α]
(f : F) (hf : Injective f) : IsDomain β
where
__ := domain_nontrivial f (map_zero _) (map_one _)
__ := hf.isCancelMulZero f (map_zero _) (map_mul _)
