proposition: Lemma invert_homomorphism A B f `{∀ a, Equiv (A a)} `{∀ a, Equiv (B a)} {ao: AlgebraOps σ A} {bo: AlgebraOps σ B} {fh: HomoMorphism A B f} `{inv: ∀ a, Inverse (f a)}: (∀ a, Bijective (f a)) → HomoMorphism A B f → HomoMorphism B A inv.
proof: Proof. Proof with try assumption; try apply _. intros ? [? ? ? ?]. constructor... intro. generalize (ao o) (bo o) (preserves _ _ f o) (algebra_propers o: Proper (=) (ao o)) (algebra_propers o: Proper (=) (bo o)). induction (σ o); simpl. intros. apply (injective (f t)). pose proof (surjective (f t) o1 o1 (reflexivity o1)). transitivity o1... symmetry... intros P Q R S T x. apply IHo0. eapply Preservation_proper''; eauto; intros; try apply _. symmetry. now apply T, (surjective (f t) x x). apply S. reflexivity. apply T. reflexivity. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra