English
There is an equivalence between any two fibers of a surjective monoid hom.
Русский
Существует эквивалентность между любыми двумя фибрами сюръективного моноидного гомоморфизма.
LaTeX
$$f.fiberEquivOfSurjective hf h h' : f^{-1}({h}) ≃ f^{-1}({h'})$$
Lean4
/-- If `s` is a subgroup of the group `α`, and `t` is a subset of `α ⧸ s`, then there is a
(typically non-canonical) bijection between the preimage of `t` in `α` and the product `s × t`. -/
@[to_additive preimageMkEquivAddSubgroupProdSet /--
If `s` is a subgroup of the additive group `α`, and `t` is a subset of `α ⧸ s`, then
there is a (typically non-canonical) bijection between the preimage of `t` in `α` and the product
`s × t`. -/
]
noncomputable def preimageMkEquivSubgroupProdSet (s : Subgroup α) (t : Set (α ⧸ s)) : QuotientGroup.mk ⁻¹' t ≃ s × t
where
toFun
a :=
⟨⟨((Quotient.out (QuotientGroup.mk a)) : α)⁻¹ * a,
leftRel_apply.mp (@Quotient.exact' _ (leftRel s) _ _ <| Quotient.out_eq' _)⟩,
⟨QuotientGroup.mk a, a.2⟩⟩
invFun
a :=
⟨Quotient.out a.2.1 * a.1.1,
show QuotientGroup.mk _ ∈ t by
rw [mk_mul_of_mem _ a.1.2, out_eq']
exact a.2.2⟩
left_inv := fun ⟨a, _⟩ => Subtype.eq <| show _ * _ = a by simp
right_inv := fun ⟨⟨a, ha⟩, ⟨x, hx⟩⟩ => by ext <;> simp [ha]
