Homomorphisms of R-coalgebras

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

Main definitions

• CoalgHom R A B: the type of R-coalgebra morphisms from A to B.
• Coalgebra.counitCoalgHom R A : A →ₗc[R] R: the counit of a coalgebra as a coalgebra homomorphism.

Notations

• A →ₗc[R] B : R-algebra homomorphism from A to B.

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 LinearMap : 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.

• toFun : A → B
• map_add' : ∀ (x y : A), self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' : ∀ (m : R) (x : A), self.toFun (m • x) = (RingHom.id R) m • self.toFun x
• counit_comp : Coalgebra.counit ∘ₗ self.toLinearMap = Coalgebra.counit
• map_comp_comul : TensorProduct.map self.toLinearMap self.toLinearMap ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ self.toLinearMap

def «term_→ₗc_» : Lean.TrailingParserDescr

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

• «term_→ₗc_» = Lean.ParserDescr.trailingNode `term_→ₗc_ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ₗc ") (Lean.ParserDescr.cat `term 25))

def «term_→ₗc[_]_» : Lean.TrailingParserDescr

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 : Prop

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

• map_add : ∀ (f : F) (x y : A), f (x + y) = f x + f y
• map_smulₛₗ : ∀ (f : F) (c : R) (x : A), f (c • x) = (RingHom.id R) c • f x
• counit_comp : ∀ (f : F), Coalgebra.counit ∘ₗ ↑f = Coalgebra.counit
• map_comp_comul : ∀ (f : F), TensorProduct.map ↑f ↑f ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ ↑f

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) : A →ₗc[R] B

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 = let __src := ↑f; { toLinearMap := { toAddHom := { 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] : CoeHead F (A →ₗc[R] B)

Equations

• CoalgHomClass.instCoeToCoalgHom = { coe := CoalgHomClass.toCoalgHom }

@[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) : Coalgebra.counit (f x) = Coalgebra.counit x

@[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) : (TensorProduct.map ↑f ↑f) (Coalgebra.comul x) = Coalgebra.comul (f x)

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

• CoalgHom.funLike = { coe := fun (f : A →ₗc[R] B) => f.toFun, coe_injective' := ⋯ }

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] : CoalgHomClass (A →ₗc[R] B) R A B

Equations

• ⋯ = ⋯

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

• CoalgHom.Simps.apply f = ⇑f

@[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 : Coalgebra.counit ∘ₗ f = Coalgebra.counit) (h₁ : TensorProduct.map f f ∘ₗ Coalgebra.comul = Coalgebra.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 : A → 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₃ : Coalgebra.counit ∘ₗ { toAddHom := { toFun := f, map_add' := h₁ }, map_smul' := h₂ } = Coalgebra.counit) (h₄ : TensorProduct.map { toAddHom := { toFun := f, map_add' := h₁ }, map_smul' := h₂ } { toAddHom := { toFun := f, map_add' := h₁ }, map_smul' := h₂ } ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ { toAddHom := { toFun := f, map_add' := h₁ }, map_smul' := h₂ }) : ⇑{ toLinearMap := { toAddHom := { 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 : Coalgebra.counit ∘ₗ f = Coalgebra.counit) (h₁ : TensorProduct.map f f ∘ₗ Coalgebra.comul = Coalgebra.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_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 DFunLike.coe

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} {φ₂ : 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.coe_addMonoidHom_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 AddMonoidHomClass.toAddMonoidHom

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} {φ₂ : 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 : A} {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} {φ₂ : A →ₗc[R] B} (H : ∀ (x : A), φ₁ x = φ₂ x) : φ₁ = φ₂

theorem CoalgHom.ext_iff {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} {φ₂ : A →ₗc[R] B} : φ₁ = φ₂ ↔ ∀ (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 : R →ₗc[R] A} {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₃ : Coalgebra.counit ∘ₗ { toAddHom := { toFun := ⇑f, map_add' := h₁ }, map_smul' := h₂ } = Coalgebra.counit) (h₄ : TensorProduct.map { toAddHom := { toFun := ⇑f, map_add' := h₁ }, map_smul' := h₂ } { toAddHom := { toFun := ⇑f, map_add' := h₁ }, map_smul' := h₂ } ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ { toAddHom := { toFun := ⇑f, map_add' := h₁ }, map_smul' := h₂ }) : { toLinearMap := { toAddHom := { toFun := ⇑f, map_add' := h₁ }, map_smul' := h₂ }, counit_comp := h₃, map_comp_comul := h₄ } = f

@[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

def CoalgHom.id (R : Type u_1) (A : Type u_2) [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] : A →ₗc[R] A

Identity map as a CoalgHom.

Equations

• CoalgHom.id R A = let __src := LinearMap.id; { toLinearMap := __src, counit_comp := ⋯, map_comp_comul := ⋯ }

@[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]

theorem CoalgHom.id_toLinearMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] : ↑(CoalgHom.id R A) = LinearMap.id

@[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), (CoalgHom.comp φ₁ φ₂) a = φ₁ (φ₂ a)

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) : A →ₗc[R] C

Composition of coalgebra homomorphisms.

Equations

• CoalgHom.comp φ₁ φ₂ = let __src := ↑φ₁ ∘ₗ ↑φ₂; { toLinearMap := __src, counit_comp := ⋯, map_comp_comul := ⋯ }

@[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) : ⇑(CoalgHom.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) : ↑(CoalgHom.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) : CoalgHom.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.comp (CoalgHom.id R B) φ = φ

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) : CoalgHom.comp (CoalgHom.comp φ₁ φ₂) φ₃ = CoalgHom.comp φ₁ (CoalgHom.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

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) (φ₂ : A →ₗc[R] A) : φ₁ * φ₂ = CoalgHom.comp φ₁ φ₂

theorem CoalgHom.End_toOne_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] : 1 = CoalgHom.id R A

instance CoalgHom.End {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] : Monoid (A →ₗc[R] A)

Equations

• CoalgHom.End = Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯

@[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) (ψ : A →ₗc[R] A) (x : A) : (φ * ψ) x = φ (ψ x)

def Coalgebra.counitCoalgHom (R : Type u) (A : Type v) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] : A →ₗc[R] R

The counit of a coalgebra as a CoalgHom.

Equations

• Coalgebra.counitCoalgHom R A = let __src := Coalgebra.counit; { toLinearMap := __src, counit_comp := ⋯, map_comp_comul := ⋯ }

@[simp]

theorem Coalgebra.counitCoalgHom_apply (R : Type u) (A : Type v) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (x : A) : (Coalgebra.counitCoalgHom R A) x = Coalgebra.counit x

@[simp]

theorem Coalgebra.counitCoalgHom_toLinearMap (R : Type u) (A : Type v) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] : ↑(Coalgebra.counitCoalgHom R A) = Coalgebra.counit

instance Coalgebra.subsingleton_to_ring {R : Type u} (A : Type v) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] : Subsingleton (A →ₗc[R] R)

Equations

• ⋯ = ⋯

theorem Coalgebra.ext_to_ring {R : Type u} (A : Type v) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (f : A →ₗc[R] R) (g : A →ₗc[R] R) : f = g