Results #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
derivation_to_square_zero_equiv_lift: TheR-derivations fromAinto a square-zero idealIofBcorresponds to the liftsA →ₐ[R] Bof the mapA →ₐ[R] B ⧸ I.
def
diff_to_ideal_of_quotient_comp_eq
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[comm_semiring A]
[comm_ring B]
[algebra R A]
[algebra R B]
(I : ideal B)
(f₁ f₂ : A →ₐ[R] B)
(e : (ideal.quotient.mkₐ R I).comp f₁ = (ideal.quotient.mkₐ R I).comp f₂) :
If f₁ f₂ : A →ₐ[R] B are two lifts of the same A →ₐ[R] B ⧸ I,
we may define a map f₁ - f₂ : A →ₗ[R] I.
Equations
- diff_to_ideal_of_quotient_comp_eq I f₁ f₂ e = linear_map.cod_restrict (submodule.restrict_scalars R I) (f₁.to_linear_map - f₂.to_linear_map) _
@[simp]
theorem
diff_to_ideal_of_quotient_comp_eq_apply
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[comm_semiring A]
[comm_ring B]
[algebra R A]
[algebra R B]
(I : ideal B)
(f₁ f₂ : A →ₐ[R] B)
(e : (ideal.quotient.mkₐ R I).comp f₁ = (ideal.quotient.mkₐ R I).comp f₂)
(x : A) :
def
derivation_to_square_zero_of_lift
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[comm_semiring A]
[comm_ring B]
[algebra R A]
[algebra R B]
(I : ideal B)
(hI : I ^ 2 = ⊥)
[algebra A B]
[is_scalar_tower R A B]
(f : A →ₐ[R] B)
(e : (ideal.quotient.mkₐ R I).comp f = is_scalar_tower.to_alg_hom R A (B ⧸ I)) :
derivation R A ↥I
Given a tower of algebras R → A → B, and a square-zero I : ideal B, each lift A →ₐ[R] B
of the canonical map A →ₐ[R] B ⧸ I corresponds to a R-derivation from A to I.
Equations
- derivation_to_square_zero_of_lift I hI f e = {to_linear_map := {to_fun := (diff_to_ideal_of_quotient_comp_eq I f (is_scalar_tower.to_alg_hom R A B) _).to_fun, map_add' := _, map_smul' := _}, map_one_eq_zero' := _, leibniz' := _}
theorem
derivation_to_square_zero_of_lift_apply
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[comm_semiring A]
[comm_ring B]
[algebra R A]
[algebra R B]
(I : ideal B)
(hI : I ^ 2 = ⊥)
[algebra A B]
[is_scalar_tower R A B]
(f : A →ₐ[R] B)
(e : (ideal.quotient.mkₐ R I).comp f = is_scalar_tower.to_alg_hom R A (B ⧸ I))
(x : A) :
↑(⇑(derivation_to_square_zero_of_lift I hI f e) x) = ⇑f x - ⇑(algebra_map A B) x
theorem
lift_of_derivation_to_square_zero_apply
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[comm_semiring A]
[comm_ring B]
[algebra R A]
[algebra R B]
(I : ideal B)
(hI : I ^ 2 = ⊥)
[algebra A B]
[is_scalar_tower R A B]
(f : derivation R A ↥I)
(x : A) :
⇑(lift_of_derivation_to_square_zero I hI f) x = ↑(⇑f x) + ⇑(algebra_map A B) x
def
lift_of_derivation_to_square_zero
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[comm_semiring A]
[comm_ring B]
[algebra R A]
[algebra R B]
(I : ideal B)
(hI : I ^ 2 = ⊥)
[algebra A B]
[is_scalar_tower R A B]
(f : derivation R A ↥I) :
Given a tower of algebras R → A → B, and a square-zero I : ideal B, each R-derivation
from A to I corresponds to a lift A →ₐ[R] B of the canonical map A →ₐ[R] B ⧸ I.
@[simp]
theorem
lift_of_derivation_to_square_zero_mk_apply
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[comm_semiring A]
[comm_ring B]
[algebra R A]
[algebra R B]
(I : ideal B)
(hI : I ^ 2 = ⊥)
[algebra A B]
[is_scalar_tower R A B]
(d : derivation R A ↥I)
(x : A) :
⇑(ideal.quotient.mk I) (⇑(lift_of_derivation_to_square_zero I hI d) x) = ⇑(algebra_map A (B ⧸ I)) x
def
derivation_to_square_zero_equiv_lift
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[comm_semiring A]
[comm_ring B]
[algebra R A]
[algebra R B]
(I : ideal B)
(hI : I ^ 2 = ⊥)
[algebra A B]
[is_scalar_tower R A B] :
derivation R A ↥I ≃ {f // (ideal.quotient.mkₐ R I).comp f = is_scalar_tower.to_alg_hom R A (B ⧸ I)}
Given a tower of algebras R → A → B, and a square-zero I : ideal B,
there is a 1-1 correspondance between R-derivations from A to I and
lifts A →ₐ[R] B of the canonical map A →ₐ[R] B ⧸ I.
Equations
- derivation_to_square_zero_equiv_lift I hI = {to_fun := λ (d : derivation R A ↥I), ⟨lift_of_derivation_to_square_zero I hI d, _⟩, inv_fun := λ (f : {f // (ideal.quotient.mkₐ R I).comp f = is_scalar_tower.to_alg_hom R A (B ⧸ I)}), derivation_to_square_zero_of_lift I hI f.val _, left_inv := _, right_inv := _}
@[simp]
theorem
derivation_to_square_zero_equiv_lift_symm_apply
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[comm_semiring A]
[comm_ring B]
[algebra R A]
[algebra R B]
(I : ideal B)
(hI : I ^ 2 = ⊥)
[algebra A B]
[is_scalar_tower R A B]
(f : {f // (ideal.quotient.mkₐ R I).comp f = is_scalar_tower.to_alg_hom R A (B ⧸ I)}) :
⇑((derivation_to_square_zero_equiv_lift I hI).symm) f = derivation_to_square_zero_of_lift I hI f.val _
@[simp]
theorem
derivation_to_square_zero_equiv_lift_apply_coe
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[comm_semiring A]
[comm_ring B]
[algebra R A]
[algebra R B]
(I : ideal B)
(hI : I ^ 2 = ⊥)
[algebra A B]
[is_scalar_tower R A B]
(d : derivation R A ↥I) :
↑(⇑(derivation_to_square_zero_equiv_lift I hI) d) = lift_of_derivation_to_square_zero I hI d