Lean4
/-- Define `NormalizationMonoid` on a structure from a `MonoidHom` inverse to `Associates.mk`. -/
def normalizationMonoidOfMonoidHomRightInverse [DecidableEq α] (f : Associates α →* α)
(hinv : Function.RightInverse f Associates.mk) : NormalizationMonoid α
where
normUnit
a := if a = 0 then 1 else Classical.choose (Associates.mk_eq_mk_iff_associated.1 (hinv (Associates.mk a)).symm)
normUnit_zero := if_pos rfl
normUnit_mul {a b} ha
hb := by
simp_rw [if_neg (mul_ne_zero ha hb), if_neg ha, if_neg hb, Units.ext_iff, Units.val_mul]
suffices
a * b * ↑(Classical.choose (associated_map_mk hinv (a * b))) =
a * ↑(Classical.choose (associated_map_mk hinv a)) * (b * ↑(Classical.choose (associated_map_mk hinv b)))
by
apply mul_left_cancel₀ (mul_ne_zero ha hb) _
simpa only [mul_assoc, mul_comm, mul_left_comm] using this
rw [map_mk_unit_aux hinv a, map_mk_unit_aux hinv (a * b), map_mk_unit_aux hinv b, ← MonoidHom.map_mul,
Associates.mk_mul_mk]
normUnit_coe_units
u := by
nontriviality α
simp_rw [if_neg (Units.ne_zero u), Units.ext_iff]
apply mul_left_cancel₀ (Units.ne_zero u)
rw [Units.mul_inv, map_mk_unit_aux hinv u,
Associates.mk_eq_mk_iff_associated.2 (associated_one_iff_isUnit.2 ⟨u, rfl⟩), Associates.mk_one, MonoidHom.map_one]
