Propositional typeclasses on several ring homs #
This file contains three typeclasses used in the definition of (semi)linear maps:
ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃, which expresses the fact that
σ₂₃.comp σ₁₂ = σ₁₃
ring_hom_inv_pair σ₁₂ σ₂₁, which states that
σ₂₁are inverses of each other
ring_hom_surjective σ, which states that
σis surjective These typeclasses ensure that objects such as
σ₂₃.comp σ₁₂never end up in the type of a semilinear map; instead, the typeclass system directly finds the appropriate
ring_homto use. A typical use-case is conjugate-linear maps, i.e. when
σ = complex.conj; this system ensures that composing two conjugate-linear maps is a linear map, and not a
conj.comp conj-linear map.
Instances of these typeclasses mostly involving
ring_hom.id are also provided:
ring_hom_inv_pair (ring_hom.id R) (ring_hom.id R)
[ring_hom_inv_pair σ₁₂ σ₂₁] : ring_hom_comp_triple σ₁₂ σ₂₁ (ring_hom.id R₁)
ring_hom_comp_triple (ring_hom.id R₁) σ₁₂ σ₁₂
ring_hom_comp_triple σ₁₂ (ring_hom.id R₂) σ₁₂
ring_hom_surjective (ring_hom.id R)
[ring_hom_inv_pair σ₁ σ₂] : ring_hom_surjective σ₁
Implementation notes #
Class that expresses the fact that three ring homomorphisms form a composition triple. This is used to handle composition of semilinear maps.
Class that expresses the fact that two ring homomorphisms are inverses of each other. This is
used to handle
symm for semilinear equivalences.
ring_hom_inv_pair from both directions of a ring equiv.
This is not an instance, as for equivalences that are involutions, a better instance
ring_hom_inv_pair e e. Indeed, this declaration is not currently used in mathlib.
Swap the direction of a
ring_hom_inv_pair. This is not an instance as it would loop, and better
instances are often available and may often be preferrable to using this one. Indeed, this
declaration is not currently used in mathlib.
Class expressing the fact that a
ring_hom is surjective. This is needed in the context
of semilinear maps, where some lemmas require this.
This cannot be an instance as there is no way to infer