Documentation

Mathlib.RingTheory.Coalgebra.Hom

Homomorphisms of R-coalgebras #

This file defines bundled homomorphisms of R-coalgebras. We largely mimic Mathlib/Algebra/Algebra/Hom.lean.

Main definitions #

Notations #

structure CoalgHom (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] extends A →ₗ[R] B :
Type (max u_2 u_3)

Given R-modules A, B with comultiplication maps Δ_A, Δ_B and counit maps ε_A, ε_B, an R-coalgebra homomorphism A →ₗc[R] B is an R-linear map f such that ε_B ∘ f = ε_A and (f ⊗ f) ∘ Δ_A = Δ_B ∘ f.

Instances For

Given R-modules A, B with comultiplication maps Δ_A, Δ_B and counit maps ε_A, ε_B, an R-coalgebra homomorphism A →ₗc[R] B is an R-linear map f such that ε_B ∘ f = ε_A and (f ⊗ f) ∘ Δ_A = Δ_B ∘ f.

Equations

Given R-modules A, B with comultiplication maps Δ_A, Δ_B and counit maps ε_A, ε_B, an R-coalgebra homomorphism A →ₗc[R] B is an R-linear map f such that ε_B ∘ f = ε_A and (f ⊗ f) ∘ Δ_A = Δ_B ∘ f.

Equations
  • One or more equations did not get rendered due to their size.
class CoalgHomClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [FunLike F A B] extends SemilinearMapClass F (RingHom.id R) A B :

CoalgHomClass F R A B asserts F is a type of bundled coalgebra homomorphisms from A to B.

Instances
def CoalgHomClass.toCoalgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [FunLike F A B] [CoalgHomClass F R A B] (f : F) :

Turn an element of a type F satisfying CoalgHomClass F R A B into an actual CoalgHom. This is declared as the default coercion from F to A →ₗc[R] B.

Equations
  • f = { toFun := f, map_add' := , map_smul' := , counit_comp := , map_comp_comul := }
instance CoalgHomClass.instCoeToCoalgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [FunLike F A B] [CoalgHomClass F R A B] :
Equations
@[simp]
theorem CoalgHomClass.counit_comp_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [FunLike F A B] [CoalgHomClass F R A B] (f : F) (x : A) :
@[simp]
theorem CoalgHomClass.map_comp_comul_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [FunLike F A B] [CoalgHomClass F R A B] (f : F) (x : A) :
instance CoalgHom.funLike {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] :
FunLike (A →ₗc[R] B) A B
Equations
instance CoalgHom.coalgHomClass {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] :
def CoalgHom.Simps.apply {R : Type u_6} {α : Type u_7} {β : Type u_8} [CommSemiring R] [AddCommMonoid α] [Module R α] [AddCommMonoid β] [Module R β] [CoalgebraStruct R α] [CoalgebraStruct R β] (f : α →ₗc[R] β) :
αβ

See Note [custom simps projection]

Equations
@[simp]
theorem CoalgHom.coe_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {F : Type u_6} [FunLike F A B] [CoalgHomClass F R A B] (f : F) :
f = f
@[simp]
theorem CoalgHom.coe_mk {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A →ₗ[R] B} (h : CoalgebraStruct.counit ∘ₗ f = CoalgebraStruct.counit) (h₁ : TensorProduct.map f f ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ f) :
{ toLinearMap := f, counit_comp := h, map_comp_comul := h₁ } = f
theorem CoalgHom.coe_mks {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : AB} (h₁ : ∀ (x y : A), f (x + y) = f x + f y) (h₂ : ∀ (m : R) (x : A), { toFun := f, map_add' := h₁ }.toFun (m x) = (RingHom.id R) m { toFun := f, map_add' := h₁ }.toFun x) (h₃ : CoalgebraStruct.counit ∘ₗ { toFun := f, map_add' := h₁, map_smul' := h₂ } = CoalgebraStruct.counit) (h₄ : TensorProduct.map { toFun := f, map_add' := h₁, map_smul' := h₂ } { toFun := f, map_add' := h₁, map_smul' := h₂ } ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ { toFun := f, map_add' := h₁, map_smul' := h₂ }) :
{ toFun := f, map_add' := h₁, map_smul' := h₂, counit_comp := h₃, map_comp_comul := h₄ } = f
@[simp]
theorem CoalgHom.coe_linearMap_mk {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A →ₗ[R] B} (h : CoalgebraStruct.counit ∘ₗ f = CoalgebraStruct.counit) (h₁ : TensorProduct.map f f ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ f) :
{ toLinearMap := f, counit_comp := h, map_comp_comul := h₁ } = f
@[simp]
theorem CoalgHom.toLinearMap_eq_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₗc[R] B) :
f.toLinearMap = f
@[simp]
theorem CoalgHom.coe_toLinearMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₗc[R] B) :
f = f
theorem CoalgHom.coe_toAddMonoidHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₗc[R] B) :
f = f
theorem CoalgHom.coe_fn_inj {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {φ₁ φ₂ : A →ₗc[R] B} :
φ₁ = φ₂ φ₁ = φ₂
theorem CoalgHom.coe_linearMap_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] :
Function.Injective fun (x : A →ₗc[R] B) => x
theorem CoalgHom.congr_fun {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {φ₁ φ₂ : A →ₗc[R] B} (H : φ₁ = φ₂) (x : A) :
φ₁ x = φ₂ x
theorem CoalgHom.congr_arg {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (φ : A →ₗc[R] B) {x y : A} (h : x = y) :
φ x = φ y
theorem CoalgHom.ext {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {φ₁ φ₂ : A →ₗc[R] B} (H : ∀ (x : A), φ₁ x = φ₂ x) :
φ₁ = φ₂
theorem CoalgHom.ext_of_ring {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] {f g : R →ₗc[R] A} (h : f 1 = g 1) :
f = g
@[simp]
theorem CoalgHom.mk_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A →ₗc[R] B} (h₁ : ∀ (x y : A), f (x + y) = f x + f y) (h₂ : ∀ (m : R) (x : A), { toFun := f, map_add' := h₁ }.toFun (m x) = (RingHom.id R) m { toFun := f, map_add' := h₁ }.toFun x) (h₃ : CoalgebraStruct.counit ∘ₗ { toFun := f, map_add' := h₁, map_smul' := h₂ } = CoalgebraStruct.counit) (h₄ : TensorProduct.map { toFun := f, map_add' := h₁, map_smul' := h₂ } { toFun := f, map_add' := h₁, map_smul' := h₂ } ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ { toFun := f, map_add' := h₁, map_smul' := h₂ }) :
{ toFun := f, map_add' := h₁, map_smul' := h₂, counit_comp := h₃, map_comp_comul := h₄ } = f
def CoalgHom.copy {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₗc[R] B) (f' : AB) (h : f' = f) :

Copy of a CoalgHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations
  • f.copy f' h = { toLinearMap := (↑f).copy f' h, counit_comp := , map_comp_comul := }
@[simp]
theorem CoalgHom.coe_copy {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₗc[R] B) (f' : AB) (h : f' = f) :
(f.copy f' h) = f'
theorem CoalgHom.copy_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₗc[R] B) (f' : AB) (h : f' = f) :
f.copy f' h = f
def CoalgHom.id (R : Type u_1) (A : Type u_2) [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] :

Identity map as a CoalgHom.

Equations
@[simp]
theorem CoalgHom.id_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] (a : A) :
(CoalgHom.id R A) a = a
@[simp]
theorem CoalgHom.coe_id {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] :
(CoalgHom.id R A) = id
@[simp]
def CoalgHom.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [AddCommMonoid C] [Module R C] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] (φ₁ : B →ₗc[R] C) (φ₂ : A →ₗc[R] B) :

Composition of coalgebra homomorphisms.

Equations
  • φ₁.comp φ₂ = { toLinearMap := φ₁ ∘ₗ φ₂, counit_comp := , map_comp_comul := }
@[simp]
theorem CoalgHom.comp_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [AddCommMonoid C] [Module R C] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] (φ₁ : B →ₗc[R] C) (φ₂ : A →ₗc[R] B) (a✝ : A) :
(φ₁.comp φ₂) a✝ = φ₁ (φ₂ a✝)
@[simp]
theorem CoalgHom.coe_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [AddCommMonoid C] [Module R C] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] (φ₁ : B →ₗc[R] C) (φ₂ : A →ₗc[R] B) :
(φ₁.comp φ₂) = φ₁ φ₂
@[simp]
theorem CoalgHom.comp_toLinearMap {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [AddCommMonoid C] [Module R C] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] (φ₁ : B →ₗc[R] C) (φ₂ : A →ₗc[R] B) :
(φ₁.comp φ₂) = φ₁ ∘ₗ φ₂
@[simp]
theorem CoalgHom.comp_id {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (φ : A →ₗc[R] B) :
φ.comp (CoalgHom.id R A) = φ
@[simp]
theorem CoalgHom.id_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (φ : A →ₗc[R] B) :
(CoalgHom.id R B).comp φ = φ
theorem CoalgHom.comp_assoc {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [AddCommMonoid C] [Module R C] [AddCommMonoid D] [Module R D] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] [CoalgebraStruct R D] (φ₁ : C →ₗc[R] D) (φ₂ : B →ₗc[R] C) (φ₃ : A →ₗc[R] B) :
(φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)
theorem CoalgHom.map_smul_of_tower {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (φ : A →ₗc[R] B) {R' : Type u_6} [SMul R' A] [SMul R' B] [LinearMap.CompatibleSMul A B R' R] (r : R') (x : A) :
φ (r x) = r φ x
instance CoalgHom.End {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] :
Equations
theorem CoalgHom.End_toOne_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] :
theorem CoalgHom.End_toSemigroup_toMul_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] (φ₁ φ₂ : A →ₗc[R] A) :
φ₁ * φ₂ = φ₁.comp φ₂
@[simp]
theorem CoalgHom.one_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] (x : A) :
1 x = x
@[simp]
theorem CoalgHom.mul_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] (φ ψ : A →ₗc[R] A) (x : A) :
(φ * ψ) x = φ (ψ x)

The counit of a coalgebra as a CoalgHom.

Equations
@[simp]
theorem Coalgebra.counitCoalgHom_apply (R : Type u) (A : Type v) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (x : A) :
theorem Coalgebra.ext_to_ring {R : Type u} (A : Type v) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (f g : A →ₗc[R] R) :
f = g
def Coalgebra.Repr.induced {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] {a : A} (repr : Repr R a) {F : Type u_1} [FunLike F A B] [CoalgHomClass F R A B] (φ : F) :
Repr R (φ a)

If φ : A → B is a coalgebra map and a = ∑ xᵢ ⊗ yᵢ, then φ a = ∑ φ xᵢ ⊗ φ yᵢ

Equations
@[simp]
theorem Coalgebra.Repr.induced_index {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] {a : A} (repr : Repr R a) {F : Type u_1} [FunLike F A B] [CoalgHomClass F R A B] (φ : F) :
(repr.induced φ).index = repr.index
@[simp]
theorem Coalgebra.Repr.induced_left {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] {a : A} (repr : Repr R a) {F : Type u_1} [FunLike F A B] [CoalgHomClass F R A B] (φ : F) (a✝ : repr.ι) :
(repr.induced φ).left a✝ = (φ repr.left) a✝
@[simp]
theorem Coalgebra.Repr.induced_ι {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] {a : A} (repr : Repr R a) {F : Type u_1} [FunLike F A B] [CoalgHomClass F R A B] (φ : F) :
(repr.induced φ).ι = repr.ι
@[simp]
theorem Coalgebra.Repr.induced_right {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] {a : A} (repr : Repr R a) {F : Type u_1} [FunLike F A B] [CoalgHomClass F R A B] (φ : F) (a✝ : repr.ι) :
(repr.induced φ).right a✝ = (φ repr.right) a✝