Documentation

AdeleRingLocallyCompact.Algebra.Ring.Equiv

Ring equivs #

In this file we extend some standard results from Equiv to RingEquiv.

source
@[simp]
theorem RingEquiv.piEquivPiSubtypeProd_symm_apply {ι : Type u_3} (p : ι → Prop) [DecidablePred p] (Y : ι → Type u_4) [(i : ι) → Add (Y i)] [(i : ι) → Mul (Y i)] (f : ((i : { x : ι // p x }) → Y ↑i) × ((i : { x : ι // ¬p x }) → Y ↑i)) (x : ι) :
(RingEquiv.piEquivPiSubtypeProd p Y).symm f x = if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩
source
@[simp]
theorem RingEquiv.piEquivPiSubtypeProd_apply {ι : Type u_3} (p : ι → Prop) [DecidablePred p] (Y : ι → Type u_4) [(i : ι) → Add (Y i)] [(i : ι) → Mul (Y i)] (f : (i : ι) → Y i) :
(RingEquiv.piEquivPiSubtypeProd p Y) f = (fun (x : { x : ι // p x }) => f ↑x, fun (x : { x : ι // ¬p x }) => f ↑x)
source
def RingEquiv.piEquivPiSubtypeProd {ι : Type u_3} (p : ι → Prop) [DecidablePred p] (Y : ι → Type u_4) [(i : ι) → Add (Y i)] [(i : ι) → Mul (Y i)] :
((i : ι) → Y i) ≃+* ((i : { x : ι // p x }) → Y ↑i) × ((i : { x : ι // ¬p x }) → Y ↑i)
Equations
Instances For
    source
    @[simp]
    theorem RingEquiv.prodMap_symm_apply {R : Type u_4} {R' : Type u_5} {S : Type u_6} {S' : Type u_7} [Add R] [Add R'] [Mul R] [Mul R'] [Add S] [Add S'] [Mul S] [Mul S'] (f : R ≃+* R') (g : S ≃+* S') :
    ∀ (a : R' × S'), (f.prodMap g).symm a = Prod.map (⇑(↑f).symm) (⇑(↑g).symm) a
    source
    @[simp]
    theorem RingEquiv.prodMap_apply {R : Type u_4} {R' : Type u_5} {S : Type u_6} {S' : Type u_7} [Add R] [Add R'] [Mul R] [Mul R'] [Add S] [Add S'] [Mul S] [Mul S'] (f : R ≃+* R') (g : S ≃+* S') :
    ∀ (a : R × S), (f.prodMap g) a = Prod.map (⇑f) (⇑g) a
    source
    def RingEquiv.prodMap {R : Type u_4} {R' : Type u_5} {S : Type u_6} {S' : Type u_7} [Add R] [Add R'] [Mul R] [Mul R'] [Add S] [Add S'] [Mul S] [Mul S'] (f : R ≃+* R') (g : S ≃+* S') :
    R × S ≃+* R' × S'
    Equations
    • f.prodMap g = { toEquiv := (↑f).prodCongr ↑g, map_mul' := ⋯, map_add' := ⋯ }
    Instances For
      source
      @[simp]
      theorem RingEquiv.coe_prodMap {R : Type u_4} {R' : Type u_5} {S : Type u_6} {S' : Type u_7} [Add R] [Add R'] [Mul R] [Mul R'] [Add S] [Add S'] [Mul S] [Mul S'] (f : R ≃+* R') (g : S ≃+* S') :
      ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
      source
      @[simp]
      theorem RingEquiv.piCongrLeft'_apply {α : Type u_1} {β : Type u_2} (A : α → Type u_4) (e : α ≃ β) [(a : α) → Add (A a)] [(a : α) → Mul (A a)] (f : (a : α) → A a) (x : β) :
      (RingEquiv.piCongrLeft' A e) f x = f (e.symm x)
      source
      @[simp]
      theorem RingEquiv.piCongrLeft'_symm_apply {α : Type u_1} {β : Type u_2} (A : α → Type u_4) (e : α ≃ β) [(a : α) → Add (A a)] [(a : α) → Mul (A a)] (f : (b : β) → A (e.symm b)) (x : α) :
      (RingEquiv.piCongrLeft' A e).symm f x = ⋯ ▸ f (e x)
      source
      def RingEquiv.piCongrLeft' {α : Type u_1} {β : Type u_2} (A : α → Type u_4) (e : α ≃ β) [(a : α) → Add (A a)] [(a : α) → Mul (A a)] :
      ((a : α) → A a) ≃+* ((b : β) → A (e.symm b))
      Equations
      Instances For
        source
        @[simp]
        theorem RingEquiv.piCongrLeft'_symm {α : Type u_1} {β : Type u_2} {R : Type u_4} [Add R] [Mul R] (e : α ≃ β) :
        (RingEquiv.piCongrLeft' (fun (x : α) => R) e).symm = RingEquiv.piCongrLeft' (fun (a : β) => R) e.symm
        source
        @[simp]
        theorem RingEquiv.piCongrLeft_apply {α : Type u_1} {β : Type u_2} (B : β → Type u_4) (e : α ≃ β) [(b : β) → Add (B b)] [(b : β) → Mul (B b)] :
        ∀ (a : (b : α) → B (e.symm.symm b)) (a_1 : β), (RingEquiv.piCongrLeft B e) a a_1 = (↑(RingEquiv.piCongrLeft' B e.symm)).symm a a_1
        source
        @[simp]
        theorem RingEquiv.piCongrLeft_symm_apply {α : Type u_1} {β : Type u_2} (B : β → Type u_4) (e : α ≃ β) [(b : β) → Add (B b)] [(b : β) → Mul (B b)] :
        ∀ (a : (a : β) → B a) (b : α), (RingEquiv.piCongrLeft B e).symm a b = (RingEquiv.piCongrLeft' B e.symm) a b
        source
        def RingEquiv.piCongrLeft {α : Type u_1} {β : Type u_2} (B : β → Type u_4) (e : α ≃ β) [(b : β) → Add (B b)] [(b : β) → Mul (B b)] :
        ((a : α) → B (e a)) ≃+* ((b : β) → B b)
        Equations
        Instances For