Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
fpvandoorn committed Jan 6, 2025
1 parent 14c4fac commit 8946bf5
Show file tree
Hide file tree
Showing 2 changed files with 41 additions and 55 deletions.
35 changes: 14 additions & 21 deletions Mathlib/RingTheory/Bialgebra/Equiv.lean
Original file line number Diff line number Diff line change
Expand Up @@ -145,14 +145,6 @@ variable [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B]

variable (e e' : A ≃ₐc[R] B)

/-- See Note [custom simps projection] -/
def Simps.apply {R : Type u} [CommSemiring R] {α : Type v} {β : Type w}
[Semiring α] [Semiring β] [Algebra R α]
[Algebra R β] [CoalgebraStruct R α] [CoalgebraStruct R β]
(f : α ≃ₐc[R] β) : α → β := f

initialize_simps_projections BialgEquiv (toFun → apply)

@[simp, norm_cast]
theorem coe_coe : ⇑(e : A →ₐc[R] B) = e :=
rfl
Expand Down Expand Up @@ -202,17 +194,27 @@ protected theorem congr_fun (h : e = e') (x : A) : e x = e' x :=

end

section
/-- See Note [custom simps projection] -/
def Simps.apply {R : Type u} [CommSemiring R] {α : Type v} {β : Type w}
[Semiring α] [Semiring β] [Algebra R α]
[Algebra R β] [CoalgebraStruct R α] [CoalgebraStruct R β]
(f : α ≃ₐc[R] β) : α → β := f

/-- See Note [custom simps projection] -/
def Simps.symm_apply {R : Type*} [CommSemiring R]
{A : Type*} {B : Type*} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
[CoalgebraStruct R A] [CoalgebraStruct R B]
(e : A ≃ₐc[R] B) : B → A :=
e.symm

variable (A R)
initialize_simps_projections BialgEquiv (toFun → apply, invFun → symm_apply)

variable (A R) in
/-- The identity map is a bialgebra equivalence. -/
@[refl, simps!]
def refl : A ≃ₐc[R] A :=
{ CoalgEquiv.refl R A, BialgHom.id R A with }

end

@[simp]
theorem refl_toCoalgEquiv : refl R A = CoalgEquiv.refl R A := rfl

Expand All @@ -229,15 +231,6 @@ def symm (e : A ≃ₐc[R] B) : B ≃ₐc[R] A :=
theorem symm_toCoalgEquiv (e : A ≃ₐc[R] B) :
e.symm = (e : A ≃ₗc[R] B).symm := rfl

/-- See Note [custom simps projection] -/
def Simps.symm_apply {R : Type*} [CommSemiring R]
{A : Type*} {B : Type*} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
[CoalgebraStruct R A] [CoalgebraStruct R B]
(e : A ≃ₐc[R] B) : B → A :=
e.symm

initialize_simps_projections BialgEquiv (invFun → symm_apply)

theorem invFun_eq_symm : e.invFun = e.symm :=
rfl

Expand Down
61 changes: 27 additions & 34 deletions Mathlib/RingTheory/Coalgebra/Equiv.lean
Original file line number Diff line number Diff line change
Expand Up @@ -118,14 +118,6 @@ variable [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [Module R A] [Mod

variable (e e' : A ≃ₗc[R] B)

/-- See Note [custom simps projection] -/
def Simps.apply {R : Type*} [CommSemiring R] {α β : Type*}
[AddCommMonoid α] [AddCommMonoid β] [Module R α]
[Module R β] [CoalgebraStruct R α] [CoalgebraStruct R β]
(f : α ≃ₗc[R] β) : α → β := f

initialize_simps_projections CoalgEquiv (toFun → apply)

@[simp, norm_cast]
theorem coe_coe : ⇑(e : A →ₗc[R] B) = e :=
rfl
Expand Down Expand Up @@ -165,37 +157,47 @@ protected theorem congr_fun (h : e = e') (x : A) : e x = e' x :=

end

section
/-- Coalgebra equivalences are symmetric. -/
@[symm]
def symm (e : A ≃ₗc[R] B) : B ≃ₗc[R] A :=
{ (e : A ≃ₗ[R] B).symm with
counit_comp := (LinearEquiv.comp_toLinearMap_symm_eq _ _).2 e.counit_comp.symm
map_comp_comul := by
show (TensorProduct.congr (e : A ≃ₗ[R] B) (e : A ≃ₗ[R] B)).symm.toLinearMap ∘ₗ comul
= comul ∘ₗ (e : A ≃ₗ[R] B).symm
rw [LinearEquiv.toLinearMap_symm_comp_eq]
simp only [TensorProduct.congr, toLinearEquiv_toLinearMap,
LinearEquiv.ofLinear_toLinearMap, ← LinearMap.comp_assoc, CoalgHomClass.map_comp_comul,
LinearEquiv.eq_comp_toLinearMap_symm] }

/-- See Note [custom simps projection] -/
def Simps.apply {R : Type*} [CommSemiring R] {α β : Type*}
[AddCommMonoid α] [AddCommMonoid β] [Module R α]
[Module R β] [CoalgebraStruct R α] [CoalgebraStruct R β]
(f : α ≃ₗc[R] β) : α → β := f

/-- See Note [custom simps projection] -/
def Simps.symm_apply {R : Type*} [CommSemiring R]
{A : Type*} {B : Type*} [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B]
[CoalgebraStruct R A] [CoalgebraStruct R B]
(e : A ≃ₗc[R] B) : B → A :=
e.symm

variable (A R)
initialize_simps_projections CoalgEquiv (toFun → apply, invFun → symm_apply)

variable (A R) in
/-- The identity map is a coalgebra equivalence. -/
@[refl, simps!]
def refl : A ≃ₗc[R] A :=
{ CoalgHom.id R A, LinearEquiv.refl R A with }

end

@[simp]
theorem refl_toLinearEquiv : refl R A = LinearEquiv.refl R A := rfl

@[simp]
theorem refl_toCoalgHom : refl R A = CoalgHom.id R A :=
rfl

/-- Coalgebra equivalences are symmetric. -/
@[symm]
def symm (e : A ≃ₗc[R] B) : B ≃ₗc[R] A :=
{ (e : A ≃ₗ[R] B).symm with
counit_comp := (LinearEquiv.comp_toLinearMap_symm_eq _ _).2 e.counit_comp.symm
map_comp_comul := by
show (TensorProduct.congr (e : A ≃ₗ[R] B) (e : A ≃ₗ[R] B)).symm.toLinearMap ∘ₗ comul
= comul ∘ₗ (e : A ≃ₗ[R] B).symm
rw [LinearEquiv.toLinearMap_symm_comp_eq]
simp only [TensorProduct.congr, toLinearEquiv_toLinearMap,
LinearEquiv.ofLinear_toLinearMap, ← LinearMap.comp_assoc, CoalgHomClass.map_comp_comul,
LinearEquiv.eq_comp_toLinearMap_symm] }

@[simp]
theorem symm_toLinearEquiv (e : A ≃ₗc[R] B) :
e.symm = (e : A ≃ₗ[R] B).symm := rfl
Expand All @@ -217,15 +219,6 @@ theorem apply_symm_apply (e : A ≃ₗc[R] B) (x) :
e (e.symm x) = x :=
LinearEquiv.apply_symm_apply (e : A ≃ₗ[R] B) x

/-- See Note [custom simps projection] -/
def Simps.symm_apply {R : Type*} [CommSemiring R]
{A : Type*} {B : Type*} [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B]
[CoalgebraStruct R A] [CoalgebraStruct R B]
(e : A ≃ₗc[R] B) : B → A :=
e.symm

initialize_simps_projections CoalgEquiv (invFun → symm_apply)

@[simp]
theorem invFun_eq_symm : e.invFun = e.symm :=
rfl
Expand Down

0 comments on commit 8946bf5

Please sign in to comment.