Built with Alectryon. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+πŸ–±οΈ to focus. On Mac, use ⌘ instead of Ctrl.
Hover-Settings: Show types: Show goals:
import Mathlib.GroupTheory.GroupAction.ConjAct
import Mathlib.Algebra.Star.Unitary
import Mathlib.LinearAlgebra.CliffordAlgebra.Star
import Mathlib.Tactic

variable {
R: Type u_1
R : 
Type*: Type (u_1 + 1)
Type*} [
CommRing: Type u_1 β†’ Type u_1
CommRing 
R: Type u_1
R]

variable {
M: Type u_2
M : 
Type*: Type (u_2 + 1)
Type*} [
AddCommGroup: Type u_2 β†’ Type u_2
AddCommGroup 
M: Type u_2
M] [
Module: (R : Type u_1) β†’ (M : Type u_2) β†’ [inst : Semiring R] β†’ [inst : AddCommMonoid M] β†’ Type (max u_1 u_2)
Module 
R: Type u_1
R 
M: Type u_2
M]

variable {
Q: QuadraticForm R M
Q : 
QuadraticForm: (R : Type u_1) β†’
  (M : Type u_2) β†’ [inst : CommSemiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [inst : Module R M] β†’ Type (max u_1 u_2)
QuadraticForm 
R: Type u_1
R 
M: Type u_2
M}

section Pin

open CliffordAlgebra MulAction

open scoped Pointwise

def 
lipschitz: (Q : QuadraticForm R M) β†’ Subgroup (CliffordAlgebra Q)Λ£
lipschitz (
Q: QuadraticForm R M
Q : 
QuadraticForm: (R : Type u_1) β†’
  (M : Type u_2) β†’ [inst : CommSemiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [inst : Module R M] β†’ Type (max u_1 u_2)
QuadraticForm 
R: Type u_1
R 
M: Type u_2
M) :=
  
Subgroup.closure: {G : Type (max u_1 u_2)} β†’ [inst : Group G] β†’ Set G β†’ Subgroup G
Subgroup.closure (
Units.val: {Ξ± : Type (max u_1 u_2)} β†’ [inst : Monoid Ξ±] β†’ Ξ±Λ£ β†’ Ξ±
Units.val ⁻¹' 
Set.range: {Ξ± : Type (max u_1 u_2)} β†’ {ΞΉ : Type u_2} β†’ (ΞΉ β†’ Ξ±) β†’ Set Ξ±
Set.range (
ΞΉ: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ (Q : QuadraticForm R M) β†’ M β†’β‚—[R] CliffordAlgebra Q
ΞΉ 
Q: QuadraticForm R M
Q) : 
Set: Type (max u_2 u_1) β†’ Type (max u_2 u_1)
Set (
CliffordAlgebra: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’ [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ QuadraticForm R M β†’ Type (max u_2 u_1)
CliffordAlgebra 
Q: QuadraticForm R M
Q)Λ£)

def 
pinGroup: (Q : QuadraticForm R M) β†’ Submonoid (CliffordAlgebra Q)
pinGroup (
Q: QuadraticForm R M
Q : 
QuadraticForm: (R : Type u_1) β†’
  (M : Type u_2) β†’ [inst : CommSemiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [inst : Module R M] β†’ Type (max u_1 u_2)
QuadraticForm 
R: Type u_1
R 
M: Type u_2
M) : 
Submonoid: (M : Type (max u_2 u_1)) β†’ [inst : MulOneClass M] β†’ Type (max u_2 u_1)
Submonoid (
CliffordAlgebra: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’ [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ QuadraticForm R M β†’ Type (max u_2 u_1)
CliffordAlgebra 
Q: QuadraticForm R M
Q) :=
  (
lipschitz: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ (Q : QuadraticForm R M) β†’ Subgroup (CliffordAlgebra Q)Λ£
lipschitz 
Q: QuadraticForm R M
Q).
toSubmonoid: {G : Type (max u_1 u_2)} β†’ [inst : Group G] β†’ Subgroup G β†’ Submonoid G
toSubmonoid.
map: {M N : Type (max u_1 u_2)} β†’
  [inst : MulOneClass M] β†’
    [inst_1 : MulOneClass N] β†’
      {F : Type (max u_1 u_2)} β†’ [inst_2 : FunLike F M N] β†’ [mc : MonoidHomClass F M N] β†’ F β†’ Submonoid M β†’ Submonoid N
map (
Units.coeHom: (M : Type (max u_2 u_1)) β†’ [inst : Monoid M] β†’ MΛ£ β†’* M
Units.coeHom <| 
CliffordAlgebra: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’ [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ QuadraticForm R M β†’ Type (max u_2 u_1)
CliffordAlgebra 
Q: QuadraticForm R M
Q) βŠ“ 
unitary: (R : Type (max u_1 u_2)) β†’ [inst : Monoid R] β†’ [inst_1 : StarMul R] β†’ Submonoid R
unitary 
_: Type (max u_1 u_2)
_

namespace pinGroup

theorem 
Warning: declaration uses 'sorry'
 {
x: CliffordAlgebra Q
x : 
CliffordAlgebra: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’ [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ QuadraticForm R M β†’ Type (max u_2 u_1)
CliffordAlgebra 
Q: QuadraticForm R M
Q} (
hx: x ∈ pinGroup Q
hx : 
x: CliffordAlgebra Q
x ∈ 
pinGroup: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ (Q : QuadraticForm R M) β†’ Submonoid (CliffordAlgebra Q)
pinGroup 
Q: QuadraticForm R M
Q) : 
star: {R : Type (max u_1 u_2)} β†’ [self : Star R] β†’ R β†’ R
star 
x: CliffordAlgebra Q
x ∈ 
pinGroup: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ (Q : QuadraticForm R M) β†’ Submonoid (CliffordAlgebra Q)
pinGroup 
Q: QuadraticForm R M
Q := 
sorry: star x ∈ pinGroup Q
sorry


instance: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’ [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ {Q : QuadraticForm R M} β†’ Star β†₯(pinGroup Q)
instance : 
Star: Type (max u_1 u_2) β†’ Type (max u_1 u_2)
Star (
pinGroup: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ (Q : QuadraticForm R M) β†’ Submonoid (CliffordAlgebra Q)
pinGroup 
Q: QuadraticForm R M
Q) :=
  ⟨fun 
x: β†₯(pinGroup Q)
x => ⟨
star: {R : Type (max u_1 u_2)} β†’ [self : Star R] β†’ R β†’ R
star 
x: β†₯(pinGroup Q)
x, 
star_mem: βˆ€ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, x ∈ pinGroup Q β†’ star x ∈ pinGroup Q
star_mem 
x: β†₯(pinGroup Q)
x.
prop: βˆ€ {Ξ± : Type (max u_1 u_2)} {p : Ξ± β†’ Prop} (x : Subtype p), p ↑x
prop⟩⟩

@[simp, norm_cast]
theorem 
coe_star: βˆ€ {x : β†₯(pinGroup Q)}, ↑(star x) = star ↑x
coe_star {
x: β†₯(pinGroup Q)
x : 
pinGroup: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ (Q : QuadraticForm R M) β†’ Submonoid (CliffordAlgebra Q)
pinGroup 
Q: QuadraticForm R M
Q} : ↑(
star: {R : Type (max u_1 u_2)} β†’ [self : Star R] β†’ R β†’ R
star 
x: β†₯(pinGroup Q)
x) = (
star: {R : Type (max u_1 u_2)} β†’ [self : Star R] β†’ R β†’ R
star 
x: β†₯(pinGroup Q)
x : 
CliffordAlgebra: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’ [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ QuadraticForm R M β†’ Type (max u_2 u_1)
CliffordAlgebra 
Q: QuadraticForm R M
Q) :=
  
rfl: βˆ€ {Ξ± : Type (max u_1 u_2)} {a : Ξ±}, a = a
rfl

set_option synthInstance.maxHeartbeats 20038 in

instance: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ {Q : QuadraticForm R M} β†’ InvolutiveStar β†₯(pinGroup Q)
instance : 
InvolutiveStar: Type (max u_1 u_2) β†’ Type (max u_1 u_2)
InvolutiveStar (
pinGroup: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ (Q : QuadraticForm R M) β†’ Submonoid (CliffordAlgebra Q)
pinGroup 
Q: QuadraticForm R M
Q) :=
  ⟨fun 
_: β†₯(pinGroup Q)
_ => 
Goals accomplished! πŸ™

    /-
    failed to synthesize

    (deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
    -/
    
R: Type u_1
inst✝²: CommRing R
M: Type u_2
inst✝¹: AddCommGroup M
inst✝: Module R M
Q: QuadraticForm R M
x✝: β†₯(pinGroup Q)
a
↑(star (star x✝)) = ↑x✝
; 
Goals accomplished! πŸ™

  ⟩

end pinGroup

end Pin