English
Given a uniform inducing map i and dense range, every uniform continuous ring hom f: α → γ extends to a ring hom from β to γ that preserves addition and multiplication.
Русский
Дано отображение i: α → β, плотное образующее и равномерно непрерывное гомоморфизм f: α → γ; он расп extends до гомоморфизма β → γ, сохраняющего сложение и умножение.
LaTeX
$$$$ \exists! \tilde{f} \in \mathrm{RingHom}(\beta, \gamma) \quad (\tilde{f} \circ i) = f $$$$
Lean4
/-- The dense inducing extension as a ring homomorphism. -/
noncomputable def extendRingHom {i : α →+* β} {f : α →+* γ} (ue : IsUniformInducing i) (dr : DenseRange i)
(hf : UniformContinuous f) : β →+* γ
where
toFun := (ue.isDenseInducing dr).extend f
map_one' := by
convert IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous 1
exacts [i.map_one.symm, f.map_one.symm]
map_zero' := by convert IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous 0 <;> simp only [map_zero]
map_add' := by
have h := (uniformContinuous_uniformly_extend ue dr hf).continuous
refine fun x y => DenseRange.induction_on₂ dr ?_ (fun a b => ?_) x y
· exact isClosed_eq (Continuous.comp h continuous_add) ((h.comp continuous_fst).add (h.comp continuous_snd))
· simp_rw [← i.map_add, IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous _, ← f.map_add]
map_mul' := by
have h := (uniformContinuous_uniformly_extend ue dr hf).continuous
refine fun x y => DenseRange.induction_on₂ dr ?_ (fun a b => ?_) x y
· exact isClosed_eq (Continuous.comp h continuous_mul) ((h.comp continuous_fst).mul (h.comp continuous_snd))
· simp_rw [← i.map_mul, IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous _, ← f.map_mul]
