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σ₁₂
andσ₂₁
are inverses of each otherring_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 appropriatering_hom
to 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 aconj.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 #
-
For the typeclass
ring_hom_inv_pair σ₁₂ σ₂₁
,σ₂₁
is marked as anout_param
, as it must typically be found via the typeclass inference system. -
Likewise, for
ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃
,σ₁₃
is marked as anout_param
, for the same reason.
Tags #
ring_hom_comp_triple
, ring_hom_inv_pair
, ring_hom_surjective
Class that expresses the fact that three ring homomorphisms form a composition triple. This is used to handle composition of semilinear maps.
Instances of this typeclass
- comp_eq : ring_hom.comp σ' σ = ring_hom.id R₁
- comp_eq₂ : σ.comp σ' = ring_hom.id R₂
Class that expresses the fact that two ring homomorphisms are inverses of each other. This is
used to handle symm
for semilinear equivalences.
Instances of this typeclass
Construct a 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
would be 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.
- is_surjective : function.surjective ⇑σ
Class expressing the fact that a ring_hom
is surjective. This is needed in the context
of semilinear maps, where some lemmas require this.
Instances of this typeclass
This cannot be an instance as there is no way to infer σ₁₂
and σ₂₃
.