English
Notable extension lemma for equalities on closures of sets regarding MonoidHom.
Русский
Замыкание левой части равенств для моноидных гомоморфизмов.
LaTeX
$$Teoretical extension lemma for closure equality of homomorphisms$$
Lean4
/-- Let `s` be a subset of a monoid `M` such that the closure of `s` is the whole monoid.
Then `MonoidHom.ofClosureEqTopRight` defines a monoid homomorphism from `M` asking for
a proof of `f (x * y) = f x * f y` only for `y ∈ s`. -/
@[to_additive /-- Let `s` be a subset of an additive monoid `M` such that the closure of `s` is
the whole monoid. Then `AddMonoidHom.ofClosureEqTopRight` defines an additive monoid
homomorphism from `M` asking for a proof of `f (x + y) = f x + f y` only for `y ∈ s`. -/
]
def ofClosureMEqTopRight {M N} [Monoid M] [Monoid N] {s : Set M} (f : M → N) (hs : closure s = ⊤) (h1 : f 1 = 1)
(hmul : ∀ (x), ∀ y ∈ s, f (x * y) = f x * f y) : M →* N
where
toFun := f
map_one' := h1
map_mul' x
y :=
dense_induction _ hs (fun y hy x => hmul x y hy) (by simp [h1])
(fun y₁ y₂ (h₁ : ∀ _, f _ = f _ * f _) (h₂ : ∀ _, f _ = f _ * f _) x => by simp [← mul_assoc, h₁, h₂]) y x
